X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flfxs.ma;h=f3f64b5ffe15c55941823c8a885e99c4c14bb15e;hb=990f97071a9939d47be16b36f6045d3b23f218e0;hp=0e7e900d544cb00861e6c26e5332234921c0cdd0;hpb=42705ef31dd3513a998533e02b5f20fb38dd4fb2;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
index 0e7e900d5..f3f64b5ff 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
@@ -12,10 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/relocation/rtmap_id.ma".
 include "basic_2/notation/relations/relationstar_4.ma".
 include "basic_2/syntax/cext2.ma".
 include "basic_2/relocation/lexs.ma".
-include "basic_2/static/fle.ma".
+include "basic_2/static/frees.ma".
 
 (* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
 
@@ -25,12 +26,6 @@ definition lfxs (R) (T): relation lenv ≝
 interpretation "generic extension on referred entries (local environment)"
    'RelationStar R T L1 L2 = (lfxs R T L1 L2).
 
-definition R_fle_compatible: predicate (relation3 …) ≝ λRN.
-                             ∀L,T1,T2. RN L T1 T2 → ⦃L, T2⦄ ⊆ ⦃L, T1⦄.
-
-definition lfxs_fle_compatible: predicate (relation3 …) ≝ λRN.
-                                ∀L1,L2,T. L1 ⪤*[RN, T] L2 → ⦃L2, T⦄ ⊆ ⦃L1, T⦄.
-
 definition R_confluent2_lfxs: relation4 (relation3 lenv term term)
                                         (relation3 lenv term term) … ≝
                               λR1,R2,RP1,RP2.