]
qed.
lemma tpss_inv_lift1_eq: ∀L,U1,U2,d,e.
L ⊢ U1 [d, e] ≫* U2 → ∀T1. ↑[d, e] T1 ≡ U1 → U1 = U2.
#L #U1 #U2 #d #e #H #T1 #HTU1 @(tpss_ind … H) -U2 //
]
qed.
lemma tpss_inv_lift1_eq: ∀L,U1,U2,d,e.
L ⊢ U1 [d, e] ≫* U2 → ∀T1. ↑[d, e] T1 ≡ U1 → U1 = U2.
#L #U1 #U2 #d #e #H #T1 #HTU1 @(tpss_ind … H) -U2 //