+qed-.
+
+lemma tnf_inv_abbr: ∀V,T. ℕ[𝕔{Abbr}V.T] → False.
+#V #T #H elim (is_lift_dec T 0 1)
+[ * #U #HTU
+ lapply (H U ?) -H /2 width=3/ #H destruct -U;
+ elim (lift_inv_pair_xy_y … HTU)
+| #HT
+ elim (tps_full (⋆) V T (⋆. 𝕓{Abbr} V) 0 ?) // #T2 #T1 #HT2 #HT12
+ lapply (H (𝕓{Abbr}V.T2) ?) -H /2/ -HT2 #H destruct -T /3 width=2/
+]