-lemma cpds_cprs_trans: ∀h,g,L,T1,T,T2.
+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 by lsstas_step_sn, le_S_S, ex4_3_intro/
+qed.
+
+lemma cpds_cprs_trans: ∀h,g,G,L,T1,T,T2.