-lemma ltpss_ldrop_trans_be: â\88\80L1,L0,d1,e1. L1 [d1, e1] â\89«* L0 →
- â\88\80L2,e2. â\87\93[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
- â\88\83â\88\83L. L [0, d1 + e1 - e2] â\89«* L2 & â\87\93[0, e2] L1 ≡ L.
+lemma ltpss_ldrop_trans_be: â\88\80L1,L0,d1,e1. L1 [d1, e1] â\96¶* L0 →
+ â\88\80L2,e2. â\87©[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+ â\88\83â\88\83L. L [0, d1 + e1 - e2] â\96¶* L2 & â\87©[0, e2] L1 ≡ L.