#h #g #G #L #T1 #T2 #H @(cprs_ind … H) -T2 /3 width=3 by cpxs_strap1, cpr_cpx/
qed.
+lemma cpxs_sort: ∀h,g,G,L,k,l1. deg h g k l1 →
+ ∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ ⋆k ➡*[h, g] ⋆((next h)^l2 k).
+#h #g #G #L #k #l1 #Hkl1 #l2 @(nat_ind_plus … l2) -l2 /2 width=1 by cpx_cpxs/
+#l2 #IHl2 #Hl21 >iter_SO
+@(cpxs_strap1 … (⋆(iter l2 ℕ (next h) k)))
+[ /3 width=3 by lt_to_le/
+| @(cpx_st … (l1-l2-1)) <plus_minus_m_m
+ /2 width=1 by deg_iter, monotonic_le_minus_r/
+]
+qed.
+
lemma cpxs_bind_dx: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →
∀I,T1,T2. ⦃G, L. ⓑ{I}V1⦄ ⊢ T1 ➡*[h, g] T2 →
∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2.
/3 width=3 by cpxs_strap2, cpx_cpxs, cpx_bind, cpx_zeta/
qed.
-lemma cpxs_tau: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 →
+lemma cpxs_eps: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 →
∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ➡*[h, g] T2.
#h #g #G #L #T1 #T2 #H @(cpxs_ind … H) -T2
-/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_tau/
+/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_eps/
qed.
-lemma cpxs_ti: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
+lemma cpxs_ct: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
∀T. ⦃G, L⦄ ⊢ ⓝV1.T ➡*[h, g] V2.
#h #g #G #L #V1 #V2 #H @(cpxs_ind … H) -V2
-/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_ti/
+/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_ct/
qed.
lemma cpxs_beta_dx: ∀h,g,a,G,L,V1,V2,W1,W2,T1,T2.
lapply (cpxs_strap1 … HT1 … HT2) -T /3 width=5 by or3_intro0, ex3_2_intro/
qed-.
-lemma cpxs_inv_cnx1: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → T = U.
+lemma cpxs_inv_cnx1: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → T = U.
#h #g #G #L #T #U #H @(cpxs_ind_dx … H) -T //
#T0 #T #H1T0 #_ #IHT #H2T0
lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/