-lemma ltpss_tpss_conf: â\88\80L1,T1,T2,d,e. L1 â\8a¢ T1 [d, e] â\89«* T2 →
- â\88\80L2,ds,es. L1 [ds, es] â\89«* L2 →
- â\88\83â\88\83T. L2 â\8a¢ T1 [d, e] â\89«* T & L1 â\8a¢ T2 [ds, es] â\89«* T.
+lemma ltpss_tpss_conf: â\88\80L1,T1,T2,d,e. L1 â\8a¢ T1 [d, e] â\96¶* T2 →
+ â\88\80L2,ds,es. L1 [ds, es] â\96¶* L2 →
+ â\88\83â\88\83T. L2 â\8a¢ T1 [d, e] â\96¶* T & L1 â\8a¢ T2 [ds, es] â\96¶* T.