-lemma csx_sort: ∀h,o,G,L,s. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃⋆s⦄.
-#h #o #G #L #s elim (deg_total h o s)
-#d generalize in match s; -s elim d -d
-[ /3 width=3 by cnx_csx, cnx_sort/
-| #d #IH #s #Hsd lapply (deg_next_SO … Hsd) -Hsd
- #Hsd @csx_intro #X #H #HX
- elim (cpx_inv_sort1 … H) -H #H destruct /2 width=1 by/
- elim HX -HX //
-]
-qed.
+lemma csx_sort: ∀h,G,L,s. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃⋆s⦄.
+/3 width=4 by cnx_csx, cnx_sort/ qed.