-lemma cnx_inv_sort: ∀h,o,G,L,s. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃⋆s⦄ → deg h o s 0.
-#h #o #G #L #s #H elim (deg_total h o s)
-#d @(nat_ind_plus … d) -d // #d #_ #Hkd
-lapply (H (⋆(next h s)) ?) -H /2 width=2 by cpx_st/ -L -d #H
-lapply (destruct_tatom_tatom_aux … H) -H #H (**) (* destruct lemma needed *)
-lapply (destruct_sort_sort_aux … H) -H #H (**) (* destruct lemma needed *)
-lapply (next_lt h s) >H -H #H elim (lt_refl_false … H)
-qed-.
-
-lemma cnx_inv_delta: ∀h,o,I,G,L,K,V,i. ⬇[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃#i⦄ → ⊥.
-#h #o #I #G #L #K #V #i #HLK #H
-elim (lift_total V 0 (i+1)) #W #HVW
-lapply (H W ?) -H [ /3 width=7 by cpx_delta/ ] -HLK #H destruct
-elim (lift_inv_lref2_be … HVW) -HVW /2 width=1 by ylt_inj/
-qed-.
-
-lemma cnx_inv_abst: ∀h,o,a,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃ⓛ{a}V.T⦄ →
- ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ ➡[h, o] 𝐍⦃T⦄.
-#h #o #a #G #L #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 #H destruct //
-]
-qed-.
-
-lemma cnx_inv_abbr: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃-ⓓV.T⦄ →
- ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ ➡[h, o] 𝐍⦃T⦄.
-#h #o #G #L #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 #H destruct //
-]
-qed-.
-