X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Ffrees_lift.ma;h=1b66bd0b74d911d9a158ae103f04ee127deb7d19;hb=52e675f555f559c047d5449db7fc89a51b977d35;hp=8b295524d7a89777e29dcfe98f62dfda2ca42866;hpb=75fac6d60f67a4dfa38ea6c2cc45a18eda5d8996;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma
index 8b295524d..1b66bd0b7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ldrop_ldrop.ma".
+include "basic_2/substitution/drop_drop.ma".
 include "basic_2/multiple/frees.ma".
 
 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
@@ -31,10 +31,10 @@ lemma frees_dec: ∀L,U,d,i. Decidable (frees d L U i).
     [ -n @or_intror #H elim (lt_refl_false i)
       lapply (frees_inv_lref_skip … H ?) -L //
     | elim (lt_or_ge j (|L|)) #Hj
-      [ elim (ldrop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct
-        elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, ldrop_fwd_rfw, or_introl/ ] #HnW
+      [ elim (drop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct
+        elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, drop_fwd_rfw, or_introl/ ] #HnW
         @or_intror #H elim (frees_inv_lref_lt … H) // #Z #Y #X #_ #HLY -d
-        lapply (ldrop_mono … HLY … HLK) -L #H destruct /2 width=1 by/  
+        lapply (drop_mono … HLY … HLK) -L #H destruct /2 width=1 by/  
       | -n @or_intror #H elim (lt_refl_false i)
         lapply (frees_inv_lref_free … H ?) -d //
       ]
@@ -60,7 +60,7 @@ lapply (yle_inv_inj … Hdj) -Hdj #Hdj
 elim (le_to_or_lt_eq … Hdj) -Hdj
 [ -I0 -K0 -W0 /3 width=9 by frees_be, yle_inj/
 | -Hji -HnU #H destruct
-  lapply (ldrop_mono … HLK0 … HLK) #H destruct -I
+  lapply (drop_mono … HLK0 … HLK) #H destruct -I
   elim HnW0 -L -U -HnW0 //
 ]
 qed.
@@ -83,7 +83,7 @@ lemma frees_lift_ge: ∀K,T,d,i. K ⊢ i ϵ𝐅*[d]⦃T⦄ →
   @frees_eq #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
 | #I #K #K0 #T #V #d #i #j #Hdj #Hji #HnT #HK0 #HV #IHV #L #s #d0 #e0 #HLK #U #HTU #Hd0i
   elim (lt_or_ge j d0) #H1
-  [ elim (ldrop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 #HLK0 #HVW
+  [ elim (drop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 #HLK0 #HVW
     @(frees_be … HL0) -HL0 -HV
     /3 width=3 by lt_plus_to_minus_r, lt_to_le_to_lt/
     [ #X #HXU >(plus_minus_m_m d0 1) in HTU; /2 width=2 by ltn_to_ltO/ #HTU
@@ -91,8 +91,8 @@ lemma frees_lift_ge: ∀K,T,d,i. K ⊢ i ϵ𝐅*[d]⦃T⦄ →
     | >minus_plus <plus_minus // <minus_plus
       /3 width=5 by monotonic_le_minus_l2/
     ]
-  | lapply (ldrop_trans_ge … HLK … HK0 ?) // -K #HLK0
-    lapply (ldrop_inv_gen … HLK0) >commutative_plus -HLK0 #HLK0
+  | lapply (drop_trans_ge … HLK … HK0 ?) // -K #HLK0
+    lapply (drop_inv_gen … HLK0) >commutative_plus -HLK0 #HLK0
     @(frees_be … HLK0) -HLK0 -IHV
     /2 width=1 by yle_plus_dx1_trans, lt_minus_to_plus/
     #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
@@ -110,7 +110,7 @@ lemma frees_inv_lift_be: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ →
   elim (lift_split … HTU i e0) -HTU /2 width=2 by/
 | #I #L #K0 #U #W #d #i #j #Hdi #Hij #HnU #HLK0 #_ #IHW #K #s #d0 #e0 #HLK #T #HTU #Hd0i #Hide0
   elim (lt_or_ge j d0) #H1
-  [ elim (ldrop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
+  [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
     @(IHW … HKL0 … HVW)
     [ /2 width=1 by monotonic_le_minus_l2/
     | >minus_plus >minus_plus >plus_minus /2 width=1 by monotonic_le_minus_l/
@@ -130,7 +130,7 @@ lemma frees_inv_lift_ge: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ →
   elim (lift_trans_le … HXT … HTU) -T // <plus_minus_m_m /2 width=2 by/
 | #I #L #K0 #U #W #d #i #j #Hdi #Hij #HnU #HLK0 #_ #IHW #K #s #d0 #e0 #HLK #T #HTU #Hde0i
   elim (lt_or_ge j d0) #H1
-  [ elim (ldrop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
+  [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
     elim (le_inv_plus_l … Hde0i) #H0 #He0i
     @(frees_be … H) -H
     [ /3 width=1 by yle_plus_dx1_trans, monotonic_yle_minus_dx/
@@ -146,7 +146,7 @@ lemma frees_inv_lift_ge: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ →
         #X #_ #H elim (HnU … H)
       | >commutative_plus /3 width=1 by le_minus_to_plus, monotonic_pred/
       ]
-    | lapply (ldrop_conf_ge … HLK … HLK0 ?) // -L #HK0
+    | lapply (drop_conf_ge … HLK … HLK0 ?) // -L #HK0
       elim (le_inv_plus_l … H2) -H2 #H2 #He0j
       @(frees_be … HK0)
       [ /2 width=1 by monotonic_yle_minus_dx/