-lemma cprs_strap2: ∀G,L,T1,T,T2.
- ⦃G, L⦄ ⊢ T1 ➡ T → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
-normalize /2 width=3 by TC_strap/ qed-.
-
-lemma lsubr_cprs_trans: ∀G. lsub_trans … (cprs G) lsubr.
-/3 width=5 by lsubr_cpr_trans, CTC_lsub_trans/
-qed-.
-
-(* Basic_1: was: pr3_pr1 *)
-lemma tprs_cprs: ∀G,L,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
-/2 width=3 by lsubr_cprs_trans/ qed.
-
-lemma cprs_bind_dx: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡* T2 →
- ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
-#G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cprs_ind_dx … HT12) -T1
-/3 width=3 by cprs_strap2, cpr_cprs, cpr_pair_sn, cpr_bind/ qed.
+(* Basic_2A1: was: cprs_strap2 *)
+lemma cprs_step_sn (h) (G) (L):
+ ∀T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T →
+ ∀T2. ⦃G, L⦄ ⊢ T ➡*[h] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h] T2.
+/2 width=3 by cpms_step_sn/ qed-.
+
+(* Basic_2A1: was: cprs_strap1 *)
+lemma cprs_step_dx (h) (G) (L):
+ ∀T1,T. ⦃G, L⦄ ⊢ T1 ➡*[h] T →
+ ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h] T2.
+/2 width=3 by cpms_step_dx/ qed-.