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=c08af2080ede3a3be05aa74ab59591658493c654;hpb=639e798161afea770f41d78673c0fe3be4125beb;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 c08af2080..9e2eb7d8e 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/A/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/A/fwd.ma
@@ -16,13 +16,13 @@
 
 include "basic_1/A/defs.ma".
 
-let rec 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 ((A_rect P f f0) 
-a0) a1 ((A_rect P f f0) a1))].
+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 
+((A_rect P f f0) a0) a1 ((A_rect P f f0) a1))].
 
-theorem A_ind:
+implied lemma A_ind:
  \forall (P: ((A \to Prop))).(((\forall (n: nat).(\forall (n0: nat).(P (ASort 
 n n0))))) \to (((\forall (a: A).((P a) \to (\forall (a0: A).((P a0) \to (P 
 (AHead a a0))))))) \to (\forall (a: A).(P a))))