update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / A / fwd.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/A/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/A/fwd.ma
index a0f6f0931217f9d175c2725dea94bbfc4ff2cb13..9e2eb7d8e65fb3c25903e38302f734bc4f33109d 100644 (file)
--- 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