(* Basic inversion lemmas ***************************************************)
-lemma tnf_inv_abst: โV,T. ๐[โV.T] โ ๐[V] โง ๐[T].
+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 //
]
qed-.
-lemma tnf_inv_appl: โV,T. ๐[โV.T] โ โงโง ๐[V] & ๐[T] & ๐[T].
+lemma tnf_inv_appl: โV,T. ๐โฆโV.Tโฆ โ โงโง ๐โฆVโฆ & ๐โฆTโฆ & ๐โฆTโฆ.
#V1 #T1 #HVT1 @and3_intro
[ #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 //
]
qed-.
-lemma tnf_inv_abbr: โV,T. ๐[โV.T] โ โฅ.
+lemma tnf_inv_abbr: โV,T. ๐โฆโV.Tโฆ โ โฅ.
#V #T #H elim (is_lift_dec T 0 1)
[ * #U #HTU
lapply (H U ?) -H /2 width=3/ #H destruct
]
qed.
-lemma tnf_inv_cast: โV,T. ๐[โฃV.T] โ โฅ.
+lemma tnf_inv_cast: โV,T. ๐โฆโV.Tโฆ โ โฅ.
#V #T #H lapply (H T ?) -H /2 width=1/ #H
@discr_tpair_xy_y //
qed-.