X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fynat_le.ma;h=1e1dad37f7f2bbe6f12c60f10ad40bbb0ca1e8ae;hp=66a47dd4a0b4f6bd30a7dc0d40c18ed8dd29e859;hb=6604a232815858a6c75dd25ac45abd68438077ff;hpb=888840f6b3a71d3d686b53b702d362ab90ab0038

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le.ma
index 66a47dd4a..1e1dad37f 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le.ma
@@ -71,7 +71,8 @@ qed-.
 lemma yle_antisym (x) (y):
       x ≤ y → y ≤ x → x = y.
 #x #y #H elim H -x -y
-[ /4 width=1 by yle_inv_inj_bi, nle_antisym, eq_f/
+[ #m #n #Hmn #Hnm
+  <(nle_antisym … Hmn) -Hmn /2 width=1 by yle_inv_inj_bi/
 | /2 width=1 by yle_inv_inf_sn/
 ] 
 qed-.