X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fcpys_cpys.ma;h=c571d9991b8263cd618cfae19c97faf43e2cf93c;hb=c671743a83bbc7fff114e3e3694f628c0ec6685b;hp=52759ca7f3f0d123609af0c23f063b507e639e3b;hpb=1555848a5546d0154964286d3400114481d78962;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma
index 52759ca7f..c571d9991 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/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 (ldrop_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 //