-#d generalize in match s; -s @(nat_ind_plus … d) -d /3 width=6 by cnx_csx, cnx_sort/
-#d #IHd #s #Hkd lapply (deg_next_SO … Hkd) -Hkd
-#Hkd @csx_intro #X #H #HX elim (cpx_inv_sort1 … H) -H
-[ #H destruct elim HX //
-| -HX * #d0 #_ #H destruct -d0 /2 width=1 by/
-]
-qed.
-
-(* Basic_1: was just: sn3_cast *)
-lemma csx_cast: ∀h,o,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, o] W →
- ∀T. ⦃G, L⦄ ⊢ ⬊*[h, o] T → ⦃G, L⦄ ⊢ ⬊*[h, o] ⓝW.T.
-#h #o #G #L #W #HW @(csx_ind … HW) -W #W #HW #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT
-@csx_intro #X #H1 #H2
-elim (cpx_inv_cast1 … H1) -H1
-[ * #W0 #T0 #HLW0 #HLT0 #H destruct
- elim (eq_false_inv_tpair_sn … H2) -H2
- [ /3 width=3 by csx_cpx_trans/
- | -HLW0 * #H destruct /3 width=1 by/
- ]
-|2,3: /3 width=3 by csx_cpx_trans/
+#d generalize in match s; -s elim d -d
+[ #s1 #Hs1 @csx_intro #X #H #HX elim HX -HX
+ elim (cpx_inv_sort1 … H) -H #H destruct //
+ /3 width=3 by tdeq_sort, deg_next/
+| #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 //