-lemma sstas_cpds_trans: ∀h,g,G,L,T1,T,T2.
- ⦃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 #HT1 * #T0 #HT0 #HT02
-lapply (sstas_trans … HT1 … HT0) -T /2 width=3/
+lemma lsstas_cpds_trans: ∀h,g,G,L,T1,T,T2,l1,l2.
+ l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 →
+ ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T → ⦃G, L⦄ ⊢ T •*➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
+#h #g #G #L #T1 #T #T2 #l1 #l2 #Hl21 #Hl1 #HT1 * #T0 #l3 #l4 #Hl43 #Hl3 #HT0 #HT02
+lapply (lsstas_da_conf … HT1 … Hl1) #H0T
+lapply (da_mono … H0T … Hl3) -H0T -Hl3 #H destruct
+lapply (le_minus_to_plus_r … Hl21 Hl43) -Hl21 -Hl43
+lapply (lsstas_trans … HT1 … HT0) -T /2 width=7/