-fact tps_inv_bind1_aux: â\88\80d,e,L,U1,U2. L â\8a¢ U1 [d, e] â\89« U2 →
- ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
- â\88\83â\88\83V2,T2. L â\8a¢ V1 [d, e] â\89« V2 &
- L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫ T2 &
- U2 = 𝕓{I} V2. T2.
+fact tps_inv_bind1_aux: â\88\80d,e,L,U1,U2. L â\8a¢ U1 [d, e] â\96¶ U2 →
+ ∀I,V1,T1. U1 = ⓑ{I} V1. T1 →
+ â\88\83â\88\83V2,T2. L â\8a¢ V1 [d, e] â\96¶ V2 &
+ L. ⓑ{I} V2 ⊢ T1 [d + 1, e] ▶ T2 &
+ U2 = ⓑ{I} V2. T2.