-lemma tnf_inv_abst: โV,T. ๐โฆโV.Tโฆ โ ๐โฆVโฆ โง ๐โฆTโฆ.
-#V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (โV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (โV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
+lemma tnf_inv_abst: โa,V,T. ๐โฆโ{a}V.Tโฆ โ ๐โฆVโฆ โง ๐โฆTโฆ.
+#a #V1 #T1 #HVT1 @conj
+[ #V2 #HV2 lapply (HVT1 (โ{a}V2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (โ{a}V1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //