-lemma ltps_inv_tps22: â\88\80e,L1,K2,I,V2. L1 [0, e] â\89« K2. ð\9d\95\93{I} V2 → 0 < e →
- â\88\83â\88\83K1,V1. K1 [0, e - 1] â\89« K2 & K2 â\8a¢ V1 [0, e - 1] â\89« V2 &
- L1 = K1. 𝕓{I} V1.
-/2 width=5/ qed.
-
-fact ltps_inv_tps12_aux: â\88\80d,e,L1,L2. L1 [d, e] â\89« L2 → 0 < d →
- ∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
- â\88\83â\88\83K1,V1. K1 [d - 1, e] â\89« K2 &
- K2 â\8a¢ V1 [d - 1, e] â\89« V2 &
- L1 = K1. 𝕓{I} V1.
-#d #e #L1 #L2 * -d e L1 L2
+lemma ltps_inv_tps22: â\88\80e,L1,K2,I,V2. L1 [0, e] â\96¶ K2. â\93\91{I} V2 → 0 < e →
+ â\88\83â\88\83K1,V1. K1 [0, e - 1] â\96¶ K2 & K2 â\8a¢ V1 [0, e - 1] â\96¶ V2 &
+ L1 = K1. ⓑ{I} V1.
+/2 width=5/ qed-.
+
+fact ltps_inv_tps12_aux: â\88\80d,e,L1,L2. L1 [d, e] â\96¶ L2 → 0 < d →
+ ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
+ â\88\83â\88\83K1,V1. K1 [d - 1, e] â\96¶ K2 &
+ K2 â\8a¢ V1 [d - 1, e] â\96¶ V2 &
+ L1 = K1. ⓑ{I} V1.
+#d #e #L1 #L2 * -d -e -L1 -L2