- ldrop is now drop as in basic_1

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_fqus.ma
index 87fd1e7f8161a58056181a6ad3eb0df901fbd800..eea2d3486a062949ab44c946758c3bc9a81a7c8a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_fqus.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/multiple/fqus_alt.ma".
-include "basic_2/multiple/lleq_ldrop.ma".
+include "basic_2/multiple/lleq_drop.ma".
 
 (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
 
@@ -24,7 +24,7 @@ lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐ ⦃G2, K2, U⦄ 
                       ∃∃K1. ⦃G1, L1, T⦄ ⊐ ⦃G2, K1, U⦄ & K1 ≡[U, 0] K2.
 #G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U
 [ #I #G #L2 #V #L1 #H elim (lleq_inv_lref_ge_dx … H … I L2 V) -H //
-  #K1 #H1 #H2 lapply (ldrop_inv_O2 … H1) -H1
+  #K1 #H1 #H2 lapply (drop_inv_O2 … H1) -H1
   #H destruct /2 width=3 by fqu_lref_O, ex2_intro/
 | * [ #a ] #I #G #L2 #V #T #L1 #H
   [ elim (lleq_inv_bind … H)
@@ -36,9 +36,9 @@ lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐ ⦃G2, K2, U⦄ 
 | #I #G #L2 #V #T #L1 #H elim (lleq_inv_flat … H) -H
   /2 width=3 by fqu_flat_dx, ex2_intro/
 | #G #L2 #K2 #T #U #e #HLK2 #HTU #L1 #HL12
-  elim (ldrop_O1_le (Ⓕ) (e+1) L1)
+  elim (drop_O1_le (Ⓕ) (e+1) L1)
   [ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/
-  | lapply (ldrop_fwd_length_le2 … HLK2) -K2
+  | lapply (drop_fwd_length_le2 … HLK2) -K2
     lapply (lleq_fwd_length … HL12) -T -U //
   ]
 ]