X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fynat_plus.ma;h=f002081e4f1bc0cc2de4a6c9bb70b3a2c31db463;hp=bc75d92d11d8d6e5a90bc45d6dd51345a11e1e21;hb=0bcf2dc1a27e38cb6cd3d44eb838d652926841e0;hpb=7e120a2bf2e6c0882b4f4b376c5861e001945cf4

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
index bc75d92d1..f002081e4 100644
--- 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 *)