-lemma ltpss_ldrop_trans_ge: â\88\80L1,L0,d1,e1. L1 [d1, e1] â\89«* L0 →
- ∀L2,e2. ↓[0, e2] L0 ≡ L2 →
- d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
-#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 /3 width=6/
+lemma ltpss_ldrop_trans_ge: â\88\80L1,L0,d1,e1. L1 [d1, e1] â\96¶* L0 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
+ d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
+#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 // /3 width=6/