+(* Basic_1: was just: sn3_nf2 *)
+lemma cnx_csn: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → ⦃h, L⦄ ⊢ ⬊*[g] T.
+/2 width=1/ qed.
+
+lemma cnx_sort: ∀h,g,L,k. ⦃h, L⦄ ⊢ ⬊*[g] ⋆k.
+#h #g #L #k elim (deg_total h g k)
+#l generalize in match k; -k @(nat_ind_plus … l) -l /3 width=1/
+#l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl
+#Hkl @csn_intro #X #H #HX elim (cpx_inv_sort1 … H) -H
+[ #H destruct elim HX //
+| -HX * #l0 #_ #H destruct -l0 /2 width=1/
+]
+qed.
+