- ∀l,l1. l1 ≤ l → ⦃G, L⦄ ⊢ T ▪[h, g] l → ∀T1. ⦃G, L⦄ ⊢ T •*[h, l1] T1 →
- ∀T2,l2. ⦃G, L⦄ ⊢ T •*➡*[h, g, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l2-l1, l1-l2] T2.
-#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T #H0 #HT #l #l1 #Hl1 #HTl #T1 #HT1 #T2 #l2 * #X #l0 #Hl20 #H #HTX #HXT2
-lapply (da_mono … H … HTl) -H #H destruct
-lapply (lstas_da_conf … HT1 … HTl) #HTl1
-lapply (lstas_da_conf … HTX … HTl) #HXl
-lapply (da_cprs_lpr_aux … IH3 IH2 … HXl … HXT2 L ?)
-[1,2,3: /3 width=8 by fpbg_fpbs_trans, lstas_fpbs/ ] #HTl2
-elim (le_or_ge l1 l2) #Hl12 >(eq_minus_O … Hl12)
-[ elim (da_lstas … HTl2 0) #X2 #HTX2 #_ -IH4 -IH3 -IH2 -IH1 -H0 -HT -HTl -HXl
+ ∀d,d1. d1 ≤ d → ⦃G, L⦄ ⊢ T ▪[h, g] d → ∀T1. ⦃G, L⦄ ⊢ T •*[h, d1] T1 →
+ ∀T2,d2. ⦃G, L⦄ ⊢ T •*➡*[h, g, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, d2-d1, d1-d2] T2.
+#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T #H0 #HT #d #d1 #Hd1 #HTd #T1 #HT1 #T2 #d2 * #X #d0 #Hd20 #H #HTX #HXT2
+lapply (da_mono … H … HTd) -H #H destruct
+lapply (lstas_da_conf … HT1 … HTd) #HTd1
+lapply (lstas_da_conf … HTX … HTd) #HXd
+lapply (da_cprs_lpr_aux … IH3 IH2 … HXd … HXT2 L ?)
+[1,2,3: /3 width=8 by fpbg_fpbs_trans, lstas_fpbs/ ] #HTd2
+elim (le_or_ge d1 d2) #Hd12 >(eq_minus_O … Hd12)
+[ elim (da_lstas … HTd2 0) #X2 #HTX2 #_ -IH4 -IH3 -IH2 -IH1 -H0 -HT -HTd -HXd