-lemma csx_cpx_trans: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, o] T1 →
- ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 → ⦃G, L⦄ ⊢ ⬊*[h, o] T2.
-#h #o #G #L #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IHT1 #T2 #HLT12
-elim (eq_term_dec T1 T2) #HT12 destruct /3 width=4 by/
-qed-.
-
-(* Basic_1: was just: sn3_nf2 *)
-lemma cnx_csx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ⬊*[h, o] T.
-/2 width=1 by NF_to_SN/ qed.
-
-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 @(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/
-]
-qed.
-