milestone update in ground_2 and basic_2A

[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / computation / lsx_lpxs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/computation/lsx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2A/computation/lsx_lpxs.ma
index d77771eec7e46983adb0c29d907bca0328c2ab27..74f255161e79b9ad7bbc60a39e5c59628e8b2508 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2A/computation/lsx_lpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/computation/lsx_lpxs.ma
@@ -20,7 +20,7 @@ include "basic_2A/computation/lsx_alt.ma".
 (* Advanced properties ******************************************************)
 
 fact lsx_bind_lpxs_aux: ∀h,g,a,I,G,L1,V,l. G ⊢ ⬊*[h, g, V, l] L1 →
-                        â\88\80Y,T. G â\8a¢ â¬\8a*[h, g, T, ⫯l] Y →
+                        â\88\80Y,T. G â\8a¢ â¬\8a*[h, g, T, â\86\91l] Y →
                         ∀L2. Y = L2.ⓑ{I}V → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
                         G ⊢ ⬊*[h, g, ⓑ{a,I}V.T, l] L2.
 #h #g #a #I #G #L1 #V #l #H @(lsx_ind_alt … H) -L1
@@ -37,7 +37,7 @@ fact lsx_bind_lpxs_aux: ∀h,g,a,I,G,L1,V,l. G ⊢ ⬊*[h, g, V, l] L1 →
 qed-.
 
 lemma lsx_bind: ∀h,g,a,I,G,L,V,l. G ⊢ ⬊*[h, g, V, l] L →
-                â\88\80T. G â\8a¢ â¬\8a*[h, g, T, ⫯l] L.ⓑ{I}V →
+                â\88\80T. G â\8a¢ â¬\8a*[h, g, T, â\86\91l] L.ⓑ{I}V →
                 G ⊢ ⬊*[h, g, ⓑ{a,I}V.T, l] L.
 /2 width=3 by lsx_bind_lpxs_aux/ qed.