lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫* U2 →
∃∃V2,T2. L ⊢ V1 [d, e] ≫* V2 &
L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫* T2 &
U2 = 𝕓{I} V2. T2.
lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫* U2 →
∃∃V2,T2. L ⊢ V1 [d, e] ≫* V2 &
L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫* T2 &
U2 = 𝕓{I} V2. T2.