-lemma cpds_cprs_trans: ∀h,g,L,T1,T,T2.
- ⦃h, L⦄ ⊢ T1 •*➡*[g] T → L ⊢ T ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
-#h #g #L #T1 #T #T2 * #T0 #HT10 #HT0 #HT2
-lapply (cprs_trans … HT0 … HT2) -T /2 width=3/
+lemma cpds_strap2: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 →
+ ⦃G, L⦄ ⊢ T1 •[h, g] T → ⦃G, L⦄ ⊢ T •*➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
+#h #g #G #L #T1 #T #T2 #l #Hl #HT1 *
+#T0 #l0 #l1 #Hl10 #HT #HT0 #HT02
+lapply (ssta_da_conf … HT1 … Hl) <minus_plus_m_m #H0T
+lapply (da_mono … H0T … HT) -HT -H0T #H destruct /3 width=7/
+qed.
+
+lemma cpds_cprs_trans: ∀h,g,G,L,T1,T,T2.
+ ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
+#h #g #G #L #T1 #T #T2 * #T0 #l1 #l2 #Hl12 #Hl1 #HT10 #HT0 #HT2
+lapply (cprs_trans … HT0 … HT2) -T /2 width=7/