notational update in ground_2 and basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma
index b836706ddd3fd72c6d197fbb58377eb237f43b3d..34ccf92d06ea9753af6c65e92e8daa123afe5234 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma
@@ -69,7 +69,7 @@ qed.
 lemma csx_inv_lref_pair: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≘ K.ⓑ{I}V →
                          ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄ → ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄.
 #h #o #I #G #L #K #V #i #HLK #Hi
-elim (lifts_total V (ð\9d\90\94â\9d´â«¯i❵))
+elim (lifts_total V (ð\9d\90\94â\9d´â\86\91i❵))
 /4 width=9 by csx_inv_lifts, csx_cpx_trans, cpx_delta_drops, drops_isuni_fwd_drop2/
 qed-.