-lemma tps_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.
-/2/ qed-.
-
-fact tps_inv_flat1_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 â\8a¢ T1 [d, e] â\89« T2 &
- U2 = 𝕗{I} V2. T2.
-#d #e #L #U1 #U2 * -d e L U1 U2
+lemma tps_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.
+/2 width=3/ qed-.
+
+fact tps_inv_flat1_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 â\8a¢ T1 [d, e] â\96¶ T2 &
+ U2 = ⓕ{I} V2. T2.
+#d #e #L #U1 #U2 * -d -e -L -U1 -U2