update in ground and delayed_updating

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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus_succ.ma
index 3c280acb0eea4baf0650164127b80d62350a84a8..d7dfaa1aa582441999c73a8275731c5c8e6c3964 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus_succ.ma
@@ -26,9 +26,6 @@ qed.
 lemma nrplus_succ_shift (p) (n): ↑p + n = p + ↑n.
 // qed.
 
-lemma nrplus_succ_sn (p) (n): ↑(p+n) = ↑p + n.
-// qed.
-
 lemma nrplus_unit_sn (n): ↑n = 𝟏 + n.
 #n @(nat_ind_succ … n) -n //
 qed.