-(* Basic_1: was: ldrop_trans_le *)
-theorem ldrop_trans_le: â\88\80d1,e1,L1,L. â\86\93[d1, e1] L1 ≡ L →
- â\88\80e2,L2. â\86\93[0, e2] L ≡ L2 → e2 ≤ d1 →
- â\88\83â\88\83L0. â\86\93[0, e2] L1 â\89¡ L0 & â\86\93[d1 - e2, e1] L0 ≡ L2.
+(* Basic_1: was: drop_trans_le *)
+theorem ldrop_trans_le: â\88\80d1,e1,L1,L. â\87©[d1, e1] L1 ≡ L →
+ â\88\80e2,L2. â\87©[0, e2] L ≡ L2 → e2 ≤ d1 →
+ â\88\83â\88\83L0. â\87©[0, e2] L1 â\89¡ L0 & â\87©[d1 - e2, e1] L0 ≡ L2.