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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_cpys.ma
index 1af1c2db0..dc646a4ca 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_cpys.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_cpys.ma
@@ -103,7 +103,7 @@ theorem cpys_antisym_eq: ∀G,L1,T1,T2,d,e. ⦃G, L1⦄ ⊢ T1 ▶*[d, e] T2 →
     lapply (cpys_weak … HW2 0 (i+1) ? ?) -HW2 //
     [ >yplus_O1 >yplus_O1 /3 width=1 by ylt_fwd_le, ylt_inj/ ] -Hi
     #HW2 >(cpys_inv_lift1_eq … HW2) -HW2 //
-  | elim (ldrop_O1_le (Ⓕ) … Hi) -Hi #K2 #HLK2
+  | elim (drop_O1_le (Ⓕ) … Hi) -Hi #K2 #HLK2
     elim (cpys_inv_lift1_ge_up … HW2 … HLK2 … HVW2 ? ? ?) -HW2 -HLK2 -HVW2
     /2 width=1 by ylt_fwd_le_succ, yle_succ_dx/ -Hdi -Hide
     #X #_ #H elim (lift_inv_lref2_be … H) -H //