-theorem lift_trans_ge: â\88\80d1,e1,T1,T. â\86\91[d1, e1] T1 ≡ T →
- â\88\80d2,e2,T2. â\86\91[d2, e2] T ≡ T2 → d1 + e1 ≤ d2 →
- â\88\83â\88\83T0. â\86\91[d2 - e1, e2] T1 â\89¡ T0 & â\86\91[d1, e1] T0 ≡ T2.
+theorem lift_trans_ge: â\88\80d1,e1,T1,T. â\87§[d1, e1] T1 ≡ T →
+ â\88\80d2,e2,T2. â\87§[d2, e2] T ≡ T2 → d1 + e1 ≤ d2 →
+ â\88\83â\88\83T0. â\87§[d2 - e1, e2] T1 â\89¡ T0 & â\87§[d1, e1] T0 ≡ T2.