X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Flsx.ma;h=c842a9448fa67aa7ec6feffc2250fae4752c378d;hb=dca4170c5ce5f2cd6be8ae1dc0422bd6a680b43f;hp=61363bf9f76aa3cd05b7bad297d30d86838d397e;hpb=d1b944b638846d98dfeb21fa6757e89c609be82a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma
index 61363bf9f..c842a9448 100644
--- 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/lazysn_5.ma".
-include "basic_2/relocation/lleq.ma".
+include "basic_2/substitution/lleq.ma".
 include "basic_2/computation/lpxs.ma".
 
 (* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
@@ -29,7 +29,7 @@ interpretation
 
 lemma lsx_ind: ∀h,g,T,G. ∀R:predicate lenv.
                (∀L1. G ⊢ ⋕⬊*[h, g, T] L1 →
-                     (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[0, T] L2 → ⊥) → R L2) →
+                     (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, 0] L2 → ⊥) → R L2) →
                      R L1
                ) →
                ∀L. G ⊢ ⋕⬊*[h, g, T] L → R L.
@@ -40,7 +40,7 @@ qed-.
 (* Basic properties *********************************************************)
 
 lemma lsx_intro: ∀h,g,T,G,L1.
-                 (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[0, T] L2 → ⊥) → G ⊢ ⋕⬊*[h, g, T] L2) →
+                 (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, 0] L2 → ⊥) → G ⊢ ⋕⬊*[h, g, T] L2) →
                  G ⊢ ⋕⬊*[h, g, T] L1.
 /5 width=1 by lleq_sym, SN_intro/ qed.