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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
index f76cbc115..f002081e4 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
@@ -19,7 +19,7 @@ include "ground/arith/ynat_succ.ma".
 (* ADDITION FOR NON-NEGATIVE INTEGERS WITH INFINITY *************************)
 
 definition yplus_aux (x) (n): ynat ≝
-           ysucc^n x.
+           (ysucc^n) x.
 
 (*** yplus *)
 definition yplus (x): ynat → ynat ≝
@@ -32,7 +32,7 @@ interpretation
 (* Basic constructions ******************************************************)
 
 lemma yplus_inj_dx (x) (n):
-      ysucc^n x = x + yinj_nat n.
+      (ysucc^n) x = x + yinj_nat n.
 #x @(ynat_bind_nat_inj (yplus_aux x))
 qed.
 
@@ -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 *)