X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fldrop_leq.ma;h=179bb5f050d541cb0a5dc26fbb6e1f8792b7cd0e;hb=4e761a2c61e9c69f045ca6fc82838beaf31894a4;hp=47ac4653d5d59282ff18525491f247fbfc3d840c;hpb=32bdf7f107be22a121fab8225c5fae4eb6b33633;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma
index 47ac4653d..179bb5f05 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma
@@ -55,7 +55,7 @@ lemma ldrop_leq_conf_be: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
 [ #d #e #J1 #K1 #W1 #i #H elim (ldrop_inv_atom1 … H) -H
   #H destruct
 | #I #L1 #L2 #V #HL12 #IHL12 #J1 #K1 #W1 #i #_ #_ #H elim (ylt_yle_false … H) //
-| #I1 #I2 #L1 #L2 #V1 #V2 #e #HL12 >yplus_O_sn >yplus_O_sn
+| #I1 #I2 #L1 #L2 #V1 #V2 #e #HL12 >yplus_O1 >yplus_O1
   #IHL12 #J1 #K1 #W1 #i #H #_ elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ]
   [ #_ lapply (ldrop_inv_O2 … H) -H
     #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_3_intro/