-lemma ltpss_ldrop_trans_ge: â\88\80L1,L0,d1,e1. L1 [d1, e1] â\89«* L0 →
- â\88\80L2,e2. â\86\93[0, e2] L0 ≡ L2 →
- d1 + e1 â\89¤ e2 â\86\92 â\86\93[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 →
+ â\88\80L2,e2. â\87©[0, e2] L0 ≡ L2 →
+ d1 + e1 â\89¤ e2 â\86\92 â\87©[0, e2] L1 ≡ L2.
+#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 // /3 width=6/