focus checkMetas: labEnd \{a}-><<HERE>>
\(a : V0~'X)->X
------------ trace
'X :: Type
X :: 'X
'XCase :: (b : 'X->Type) -> b X -> d:'X -> b d
match'X :: (b : Type->Type) -> b 'X -> d:Type -> b d -> b d
!focus checkMetas: labEnd \{a}-><<HERE>>
\(a : V0~'X)->X
------------ tooltips
testdata/typesig.reject.lc 3:6-3:7  Type
testdata/typesig.reject.lc 3:6-3:11  Type
testdata/typesig.reject.lc 3:10-3:11  X
testdata/typesig.reject.lc 5:6-5:7  Type | V1
testdata/typesig.reject.lc 6:5-6:6  X