-lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫* U2 →
- â\88\83â\88\83V2,T2. L â\8a¢ V1 [d, e] â\89«* 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 →
+ â\88\83â\88\83V2,T2. L â\8a¢ V1 [d, e] â\96¶* V2 &
+ L. ⓑ{I} V2 ⊢ T1 [d + 1, e] ▶* T2 &
+ U2 = ⓑ{I} V2. T2.