notational change of lift, drop, and gget

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / lsx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma
index 0f47fe0567f69a3b5725c48bbc6e25fa3ad80500..3c2b01edd1a0f5719d95645ca9b876953f2b02bb 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/sn_6.ma".
-include "basic_2/substitution/lleq.ma".
+include "basic_2/multiple/lleq.ma".
 include "basic_2/reduction/lpx.ma".
 
 (* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
@@ -63,7 +63,7 @@ lemma lsx_gref: ∀h,g,G,L,d,p. G ⊢ ⬊*[h, g, §p, d] L.
 qed.
 
 lemma lsx_ge_up: ∀h,g,G,L,T,U,dt,d,e. dt ≤ yinj d + yinj e →
-                 â\87§[d, e] T ≡ U → G ⊢ ⬊*[h, g, U, dt] L → G ⊢ ⬊*[h, g, U, d] L.
+                 â¬\86[d, e] T ≡ U → G ⊢ ⬊*[h, g, U, dt] L → G ⊢ ⬊*[h, g, U, d] L.
 #h #g #G #L #T #U #dt #d #e #Hdtde #HTU #H @(lsx_ind … H) -L
 /5 width=7 by lsx_intro, lleq_ge_up/
 qed-.