-lemma ltps_tps_trans: â\88\80L0,T2,U2,d2,e2. L0 â\8a¢ T2 [d2, e2] â\89« U2 →
- â\88\80L1,d1,e1. L1 [d1, e1] â\89« L0 →
- â\88\83â\88\83T. L1 â\8a¢ T2 [d2, e2] â\89« T &
- L0 â\8a¢ T [d1, e1] â\89« U2.
+lemma ltps_tps_trans: â\88\80L0,T2,U2,d2,e2. L0 â\8a¢ T2 [d2, e2] â\96¶ U2 →
+ â\88\80L1,d1,e1. L1 [d1, e1] â\96¶ L0 →
+ â\88\83â\88\83T. L1 â\8a¢ T2 [d2, e2] â\96¶ T &
+ L0 â\8a¢ T [d1, e1] â\96¶ U2.