-theorem tpss_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ▶* T0 →
- ∀T2,d2,e2. L ⊢ T0 [d2, e2] ▶* T2 → d2 + e2 ≤ d1 →
- ∃∃T. L ⊢ T1 [d2, e2] ▶* T & L ⊢ T [d1, e1] ▶* T2.
+theorem tpss_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 ▶* [d1, e1] T0 →
+ ∀T2,d2,e2. L ⊢ T0 ▶* [d2, e2] T2 → d2 + e2 ≤ d1 →
+ ∃∃T. L ⊢ T1 ▶* [d2, e2] T & L ⊢ T ▶* [d1, e1] T2.