X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fynat_plus.ma;h=bc75d92d11d8d6e5a90bc45d6dd51345a11e1e21;hb=55c768d7e45babb300b5010463ba3196a68f1bbe;hp=f76cbc115bb118588de873b61010498f0680be55;hpb=15212e44902f25536f6e2de4bec4cedcd9a9804d;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..bc75d92d1 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.