X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fynat%2Fynat_pred.ma;h=b64e388773f454ea8e13fc3b7bf131625c323c3f;hp=b49dbda04a708baf00d037c358a331d0c8a1f352;hb=fb4c641d43be3d601104751363782553bea0fb6b;hpb=765848c4d9a3f5434fae623f3e623d1b73ac76a5

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma
index b49dbda04..b64e38877 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma
@@ -37,5 +37,5 @@ lemma ypred_Y: (↓∞) = ∞.
 
 lemma ypred_inv_refl: ∀m:ynat. ↓m = m → m = 0 ∨ m = ∞.
 * // #m #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *)
-/4 width=1 by pred_inv_refl, or_introl, eq_f/
+/4 width=1 by pred_inv_fix_sn, or_introl, eq_f/
 qed-.