X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fynat%2Fynat_min.ma;h=96b8f2a21082ee2103b48d4a402bfaf005397bee;hb=14a8276e6d877c2281a1fda452ed3e4c150f5d39;hp=7661dd4868f1acda89640eac5823cf94bfdeecd0;hpb=4b7a1d1c4258c10822823cb5ee1949bcdf81abcb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_min.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_min.ma
index 7661dd486..96b8f2a21 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_min.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_min.ma
@@ -20,7 +20,7 @@ fact ymin_pre_dx_aux: ∀x,y. y ≤ x → x - (x - y) ≤ y.
 #x #y * -x -y
 [ #x #y #Hxy >yminus_inj
  /3 width=4 by yle_inj, monotonic_le_minus_l/
-| * // #m >yminus_Y_inj //
+| * //
 ]
 qed-.