(* Basic inversion lemmas ***************************************************)
lemma cnx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃⋆k⦄ → deg h g k 0.
#h #g #G #L #k #H elim (deg_total h g k)
#l @(nat_ind_plus … l) -l // #l #_ #Hkl
(* Basic inversion lemmas ***************************************************)
lemma cnx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃⋆k⦄ → deg h g k 0.
#h #g #G #L #k #H elim (deg_total h g k)
#l @(nat_ind_plus … l) -l // #l #_ #Hkl