-lemma cnx_sort: ∀h,g,L,k. deg h g k 0 → ⦃h, L⦄ ⊢ 𝐍[g]⦃⋆k⦄.
-#h #g #L #k #Hk #X #H elim (cpx_inv_sort1 … H) -H // * #l #Hkl #_
-lapply (deg_mono … Hkl Hk) -h -L <plus_n_Sm #H destruct
+lemma cnx_sort: ∀h,g,G,L,k. deg h g k 0 → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃⋆k⦄.
+#h #g #G #L #k #Hk #X #H elim (cpx_inv_sort1 … H) -H // * #l #Hkl #_
+lapply (deg_mono … Hkl Hk) -h -L <plus_n_Sm #H destruct
+qed.
+
+lemma cnx_sort_iter: ∀h,g,G,L,k,l. deg h g k l → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃⋆((next h)^l k)⦄.
+#h #g #G #L #k #l #Hkl
+lapply (deg_iter … l Hkl) -Hkl <minus_n_n /2 width=6 by cnx_sort/
+qed.
+
+lemma cnx_lref_free: ∀h,g,G,L,i. |L| ≤ i → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃#i⦄.
+#h #g #G #L #i #Hi #X #H elim (cpx_inv_lref1 … H) -H // *
+#I #K #V1 #V2 #HLK lapply (ldrop_fwd_length_lt2 … HLK) -HLK
+#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/