-lemma tpss_lift_le: â\88\80K,T1,T2,dt,et. K â\8a¢ T1 [dt, et] â\89«* T2 →
- â\88\80L,U1,d,e. dt + et â\89¤ d â\86\92 â\87\93[d, e] L ≡ K →
- â\87\91[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â\87\91[d, e] T2 ≡ U2 →
- L â\8a¢ U1 [dt, et] â\89«* U2.
+lemma tpss_lift_le: â\88\80K,T1,T2,dt,et. K â\8a¢ T1 [dt, et] â\96¶* T2 →
+ â\88\80L,U1,d,e. dt + et â\89¤ d â\86\92 â\87©[d, e] L ≡ K →
+ â\87§[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â\87§[d, e] T2 ≡ U2 →
+ L â\8a¢ U1 [dt, et] â\96¶* U2.