X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_succ.ma;h=660d4147a4fbb9a0cd317617de3b82fea6bba6bd;hb=d54b569f6bf95945a851455c0a13b08c51ddce60;hp=742c6b25776f397bfddd57541f8a007ad5a0b4cc;hpb=e6482f7f499fbb88aff8a205d2a2c808158042c5;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
index 742c6b257..660d4147a 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
@@ -41,6 +41,9 @@ lemma npsucc_zero: (𝟏) = ↑𝟎.
 lemma npsucc_inj (p): (↑p) = ↑(ninj p).
 // qed.
 
+lemma nsucc_unfold (n): ninj (↑n) = ↑n.
+// qed-.
+
 lemma nsucc_zero: ninj (𝟏) = ↑𝟎.
 // qed.