- new definition of lazy equivalence for local environments,

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / ldrop_leq.ma

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 47ac4653d5d59282ff18525491f247fbfc3d840c..179bb5f050d541cb0a5dc26fbb6e1f8792b7cd0e 100644 (file)
--- 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/