]
qed-.
-lemma tnf_inv_abbr: โV,T. ๐[โV.T] โ False.
+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] โ False.
+lemma tnf_inv_cast: โV,T. ๐[โฃV.T] โ โฅ.
#V #T #H lapply (H T ?) -H /2 width=1/ #H
-@(discr_tpair_xy_y โฆ H)
+@discr_tpair_xy_y //
qed-.