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=d1b944b638846d98dfeb21fa6757e89c609be82a;hp=c244b9caed637c9567846f7515f054511f3a57f4;hpb=ab0d181f9a89f461a9c280f42a949a2dc2abe44c;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.