- some refactoring and minor additions

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / lpx_frees.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_frees.ma
index e303b8386604a6a1544856499e8dd18971cf347b..1458cf3fa69c898c40e48c902309baa2bc04a089 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_frees.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_frees.ma
@@ -12,18 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/fqup.ma".
-include "basic_2/substitution/frees_lift.ma".
+include "basic_2/multiple/fqup.ma".
+include "basic_2/multiple/frees_lift.ma".
 include "basic_2/reduction/lpx_ldrop.ma".
 
 (* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
 (*
-lemma yle_plus2_to_minus_inj2: ∀x,y:ynat. ∀z:nat. x ≤ y + z → x - z ≤ y.
-/2 width=1 by monotonic_yle_minus_dx/ qed-.
-
-lemma yle_plus2_to_minus_inj1: ∀x,y:ynat. ∀z:nat. x ≤ z + y → x - z ≤ y.
-/2 width=1 by yle_plus2_to_minus_inj2/ qed-.
-
 lemma cofrees_lsuby_conf: ∀L1,U,i. L1 ⊢ i ~ϵ 𝐅*⦃U⦄ →
                           ∀L2. lsuby L1 L2 → L2 ⊢ i ~ϵ 𝐅*⦃U⦄.
 /3 width=3 by lsuby_cpys_trans/ qed-.