focus checkMetas: labEnd \{a}-><<HERE>>
\(a : V0~'X)->X