X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fcomputation%2Flsx_lpxs.ma;h=74f255161e79b9ad7bbc60a39e5c59628e8b2508;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=d77771eec7e46983adb0c29d907bca0328c2ab27;hpb=277fc8ff21ce3dbd6893b1994c55cf5c06a98355;p=helm.git

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 d77771eec..74f255161 100644
--- 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 →
-                        ∀Y,T. G ⊢ ⬊*[h, g, T, ⫯l] Y →
+                        ∀Y,T. G ⊢ ⬊*[h, g, T, ↑l] 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 →
-                ∀T. G ⊢ ⬊*[h, g, T, ⫯l] L.ⓑ{I}V →
+                ∀T. G ⊢ ⬊*[h, g, T, ↑l] L.ⓑ{I}V →
                 G ⊢ ⬊*[h, g, ⓑ{a,I}V.T, l] L.
 /2 width=3 by lsx_bind_lpxs_aux/ qed.