]
qed.
lemma ltps_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
∀L1,d1,e1. L1 [d1, e1] ≫ L0 → d1 + e1 ≤ d2 →
L1 ⊢ T2 [d2, e2] ≫ U2.
]
qed.
lemma ltps_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
∀L1,d1,e1. L1 [d1, e1] ≫ L0 → d1 + e1 ≤ d2 →
L1 ⊢ T2 [d2, e2] ≫ U2.