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

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/computation/lsx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2A/computation/lsx_lpx.ma
index a50714b20..c897a9333 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/computation/lsx_lpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/computation/lsx_lpx.ma
@@ -45,7 +45,7 @@ qed-.
 (* Advanced forward lemmas **************************************************)
 
 lemma lsx_fwd_bind_dx: ∀h,g,a,I,G,L,V,T,l. G ⊢ ⬊*[h, g, ⓑ{a,I}V.T, l] L →
-                       G ⊢ ⬊*[h, g, T, ⫯l] L.ⓑ{I}V.
+                       G ⊢ ⬊*[h, g, T, ↑l] L.ⓑ{I}V.
 #h #g #a #I #G #L #V1 #T #l #H @(lsx_ind … H) -L
 #L1 #_ #IHL1 @lsx_intro
 #Y #H #HT elim (lpx_inv_pair1 … H) -H
@@ -59,5 +59,5 @@ qed-.
 (* Advanced inversion lemmas ************************************************)
 
 lemma lsx_inv_bind: ∀h,g,a,I,G,L,V,T,l. G ⊢ ⬊*[h, g, ⓑ{a, I}V.T, l] L →
-                    G ⊢ ⬊*[h, g, V, l] L ∧ G ⊢ ⬊*[h, g, T, ⫯l] L.ⓑ{I}V.
+                    G ⊢ ⬊*[h, g, V, l] L ∧ G ⊢ ⬊*[h, g, T, ↑l] L.ⓑ{I}V.
 /3 width=4 by lsx_fwd_bind_sn, lsx_fwd_bind_dx, conj/ qed-.