milestone update in ground_2 and basic_2A

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

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 a50714b20506c40b3311e6027865025ae971439b..c897a93331922ebf8558e4fd0e75ee36d0e5b78c 100644 (file)
--- 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 â\8a¢ â¬\8a*[h, g, T, ⫯l] L.ⓑ{I}V.
+                       G â\8a¢ â¬\8a*[h, g, T, â\86\91l] 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 â\8a¢ â¬\8a*[h, g, V, l] L â\88§ G â\8a¢ â¬\8a*[h, g, T, ⫯l] L.ⓑ{I}V.
+                    G â\8a¢ â¬\8a*[h, g, V, l] L â\88§ G â\8a¢ â¬\8a*[h, g, T, â\86\91l] L.ⓑ{I}V.
 /3 width=4 by lsx_fwd_bind_sn, lsx_fwd_bind_dx, conj/ qed-.