X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2FA%2Ffwd.ma;h=9e2eb7d8e65fb3c25903e38302f734bc4f33109d;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=a0f6f0931217f9d175c2725dea94bbfc4ff2cb13;hpb=8de8cf8adfa6fcda91047eb2c25535893ede046a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/A/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/A/fwd.ma
index a0f6f0931..9e2eb7d8e 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/A/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/A/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/A/defs.ma".
 
-implied let rec A_rect (P: (A \to Type[0])) (f: (\forall (n: nat).(\forall 
+implied rec lemma A_rect (P: (A \to Type[0])) (f: (\forall (n: nat).(\forall 
 (n0: nat).(P (ASort n n0))))) (f0: (\forall (a: A).((P a) \to (\forall (a0: 
 A).((P a0) \to (P (AHead a a0))))))) (a: A) on a: P a \def match a with 
 [(ASort n n0) \Rightarrow (f n n0) | (AHead a0 a1) \Rightarrow (f0 a0