notational update in ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / csx_csx_vector.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma
index 6872763e0c756078889f8f75dfe35d43f3e3ad23..e1166a0fd127622a1319dfd8125516b58367b251 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma
@@ -38,7 +38,7 @@ elim (cpxs_fwd_beta_vector … o … H) -H #H
 qed.
 
 lemma csx_applv_delta: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 →
-                       â\88\80V2. â¬\86*[⫯i] V1 ≘ V2 →
+                       â\88\80V2. â¬\86*[â\86\91i] V1 ≘ V2 →
                        ∀Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.V2⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.#i⦄.
 #h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
 [ /4 width=11 by csx_inv_lifts, csx_lref_pair, drops_isuni_fwd_drop2/