update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_succ.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
index 742c6b25776f397bfddd57541f8a007ad5a0b4cc..660d4147a4fbb9a0cd317617de3b82fea6bba6bd 100644 (file)
--- 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.