- ldrop is now drop as in basic_1

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / multiple / frees_leq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_leq.ma
index bb387ad1065337a0eaaf85ec2d51fc0e13a34700..c8cf8f0c2f244719896f1a5e9de8a67587a06a49 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_leq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_leq.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ldrop_leq.ma".
+include "basic_2/substitution/drop_leq.ma".
 include "basic_2/multiple/frees.ma".
 
 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
@@ -20,13 +20,13 @@ include "basic_2/multiple/frees.ma".
 (* Properties on equivalence for local environments *************************)
 
 lemma leq_frees_trans: ∀L2,U,d,i. L2 ⊢ i ϵ 𝐅*[d]⦃U⦄ →
-                       â\88\80L1. L1 â\89\83[d, ∞] L2 → L1 ⊢ i ϵ 𝐅*[d]⦃U⦄.
+                       â\88\80L1. L1 ⩬[d, ∞] L2 → L1 ⊢ i ϵ 𝐅*[d]⦃U⦄.
 #L2 #U #d #i #H elim H -L2 -U -d -i /3 width=2 by frees_eq/
 #I2 #L2 #K2 #U #W2 #d #i #j #Hdj #Hji #HnU #HLK2 #_ #IHW2 #L1 #HL12
-elim (leq_ldrop_trans_be … HL12 … HLK2) -L2 // >yminus_Y_inj #K1 #HK12 #HLK1
+elim (leq_drop_trans_be … HL12 … HLK2) -L2 // >yminus_Y_inj #K1 #HK12 #HLK1
 lapply (leq_inv_O_Y … HK12) -HK12 #H destruct /3 width=9 by frees_be/
 qed-.
 
 lemma frees_leq_conf: ∀L1,U,d,i. L1 ⊢ i ϵ 𝐅*[d]⦃U⦄ →
-                      â\88\80L2. L1 â\89\83[d, ∞] L2 → L2 ⊢ i ϵ 𝐅*[d]⦃U⦄.
+                      â\88\80L2. L1 ⩬[d, ∞] L2 → L2 ⊢ i ϵ 𝐅*[d]⦃U⦄.
 /3 width=3 by leq_sym, leq_frees_trans/ qed-.