X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fynat%2Fynat_succ.ma;h=a8d1946bea235170f6405cdcc962f660c1e789ae;hb=b3f8b89278d193ed0aa0f39e7f8d74cf1de81d8d;hp=c244b9caed637c9567846f7515f054511f3a57f4;hpb=c9a1672c725945b47f9ea8af3c23b67cf9026f01;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma
index c244b9cae..a8d1946be 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma
@@ -38,6 +38,11 @@ lemma ynat_cases: ∀n:ynat. n = 0 ∨ ∃m. n = ⫯m.
 ]
 qed-.
 
+lemma ysucc_iter_Y: ∀m. ysucc^m (∞) = ∞.
+#m elim m -m //
+#m #IHm whd in ⊢ (??%?); >IHm //
+qed.
+
 (* Inversion lemmas *********************************************************)
 
 lemma ysucc_inj: ∀m,n. ⫯m = ⫯n → m = n.