X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Faplus%2Fdefs.ma;h=c26b3c28656754bb6898772e31b1c451ebf19620;hb=6c15dd2d7c372dc163c24e96bf56376c5bcb5a6c;hp=08c752cb8718616cf5308be1fa6f7e17f3acc888;hpb=e8656c819b0b5e7bea7b4da244015b480af5f0f5;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/aplus/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/aplus/defs.ma
index 08c752cb8..c26b3c286 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/aplus/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/aplus/defs.ma
@@ -17,5 +17,5 @@
 include "basic_1/asucc/defs.ma".
 
 let rec aplus (g: G) (a: A) (n: nat) on n: A \def match n with [O \Rightarrow 
-a | (S n0) \Rightarrow (let TMP_1 \def (aplus g a n0) in (asucc g TMP_1))].
+a | (S n0) \Rightarrow (asucc g (aplus g a n0))].