-lemma cprs_flat_dx: ∀I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 →
- ⦃G, L⦄ ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2.
-#I #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind … HT12) -T2
-/3 width=5 by cprs_strap1, cpr_flat, cpr_cprs, cpr_pair_sn/
-qed.
-
-lemma cprs_flat_sn: ∀I,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡* V2 →
- ⦃G, L⦄ ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2.
-#I #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cprs_ind … H) -V2
-/3 width=3 by cprs_strap1, cpr_cprs, cpr_pair_sn, cpr_flat/
-qed.
-
-lemma cprs_zeta: ∀G,L,V,T1,T,T2. ⬆[0, 1] T2 ≘ T →
- ⦃G, L.ⓓV⦄ ⊢ T1 ➡* T → ⦃G, L⦄ ⊢ +ⓓV.T1 ➡* T2.
-#G #L #V #T1 #T #T2 #HT2 #H @(cprs_ind_dx … H) -T1
-/3 width=3 by cprs_strap2, cpr_cprs, cpr_bind, cpr_zeta/
-qed.
-
-lemma cprs_eps: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ➡* T2.
-#G #L #T1 #T2 #H @(cprs_ind … H) -T2
-/3 width=3 by cprs_strap1, cpr_cprs, cpr_eps/
+lemma cprs_flat_dx (h) (I) (G) (L):
+ ∀V1,V2. ❪G,L❫ ⊢ V1 ➡[h] V2 →
+ ∀T1,T2. ❪G,L❫ ⊢ T1 ➡*[h] T2 →
+ ❪G,L❫ ⊢ ⓕ[I]V1.T1 ➡*[h] ⓕ[I]V2.T2.
+#h #I #G #L #V1 #V2 #HV12 #T1 #T2 #H @(cprs_ind_sn … H) -T1
+/3 width=3 by cprs_step_sn, cpm_cpms, cpr_flat/