update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
index bc75d92d11d8d6e5a90bc45d6dd51345a11e1e21..f002081e4f1bc0cc2de4a6c9bb70b3a2c31db463 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
@@ -47,7 +47,7 @@ lemma yplus_zero_dx (x): x = x + 𝟎.
 (* Constructions with ysucc *************************************************)
 
 (*** yplus_SO2 *)
-lemma yplus_one_dx (x): ↑x = x + 𝟏.
+lemma yplus_unit_dx (x): ↑x = x + 𝟏.
 // qed.
 
 (*** yplus_S2 yplus_succ2 *)