-lemma cpxs_strap1: ∀h,o,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T →
- ∀T2. ⦃G, L⦄ ⊢ T ⬈[h, o] T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2.
-normalize /2 width=3 by step/ qed.
-
-lemma cpxs_strap2: ∀h,o,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬈[h, o] T →
- ∀T2. ⦃G, L⦄ ⊢ T ⬈*[h, o] T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2.
-normalize /2 width=3 by TC_strap/ qed.
-
-lemma lsubr_cpxs_trans: ∀h,o,G. lsub_trans … (cpxs h o G) lsubr.
-/3 width=5 by lsubr_cpx_trans, LTC_lsub_trans/
-qed-.
-
-lemma cprs_cpxs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈* T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2.
-#h #o #G #L #T1 #T2 #H @(cprs_ind … H) -T2 /3 width=3 by cpxs_strap1, cpr_cpx/
-qed.
-
-lemma cpxs_sort: ∀h,o,G,L,s,d1. deg h o s d1 →
- ∀d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ ⋆s ⬈*[h, o] ⋆((next h)^d2 s).
-#h #o #G #L #s #d1 #Hkd1 #d2 @(nat_ind_plus … d2) -d2 /2 width=1 by cpx_cpxs/
-#d2 #IHd2 #Hd21 >iter_SO
-@(cpxs_strap1 … (⋆(iter d2 ℕ (next h) s)))
-[ /3 width=3 by lt_to_le/
-| @(cpx_st … (d1-d2-1)) <plus_minus_k_k
- /2 width=1 by deg_iter, monotonic_le_minus_c/
-]
-qed.
-
-lemma cpxs_bind_dx: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 →
- ∀I,T1,T2. ⦃G, L. ⓑ{I}V1⦄ ⊢ T1 ⬈*[h, o] T2 →
- ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ⬈*[h, o] ⓑ{a,I}V2.T2.
-#h #o #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cpxs_ind_dx … HT12) -T1
+lemma cpxs_strap1 (G) (L):
+ ∀T1,T. ❪G,L❫ ⊢ T1 ⬈* T →
+ ∀T2. ❪G,L❫ ⊢ T ⬈ T2 → ❪G,L❫ ⊢ T1 ⬈* T2.
+normalize /2 width=3 by step/ qed-.
+
+lemma cpxs_strap2 (G) (L):
+ ∀T1,T. ❪G,L❫ ⊢ T1 ⬈ T →
+ ∀T2. ❪G,L❫ ⊢ T ⬈* T2 → ❪G,L❫ ⊢ T1 ⬈* T2.
+normalize /2 width=3 by TC_strap/ qed-.
+
+(* Basic_2A1: was just: cpxs_sort *)
+lemma cpxs_qu (G) (L):
+ ∀s1,s2. ❪G,L❫ ⊢ ⋆s1 ⬈* ⋆s2.
+/2 width=1 by cpx_cpxs/ qed.
+
+lemma cpxs_bind_dx (G) (L):
+ ∀V1,V2. ❪G,L❫ ⊢ V1 ⬈ V2 →
+ ∀I,T1,T2. ❪G,L. ⓑ[I]V1❫ ⊢ T1 ⬈* T2 →
+ ∀p. ❪G,L❫ ⊢ ⓑ[p,I]V1.T1 ⬈* ⓑ[p,I]V2.T2.
+#G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cpxs_ind_dx … HT12) -T1