X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_rplus.ma;h=a919727559b6981967a44fc231c964b074f76818;hb=2e4a7c54ef77c10cb1cef4b59518c473245ea935;hp=694ac940729130980af50518a63e1e9a7f40ab4b;hpb=8fdf1af656038d0245eba64ff2531bbe94ce0e9e;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus.ma
index 694ac9407..a91972755 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus.ma
@@ -17,7 +17,7 @@ include "ground/arith/nat_iter.ma".
 (* RIGHT ADDITION FOR NON-NEGATIVE INTEGERS *********************************)
 
 definition nrplus: pnat → nat → pnat ≝
-           λp,n. psucc^n p.
+           λp,n. (psucc^n) p.
 
 interpretation
   "right plus (non-negative integers)"