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=0f5f065dffdb8647d11f7408858b2d526092f4e3;hpb=e8656c819b0b5e7bea7b4da244015b480af5f0f5;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 0f5f065df..9e2eb7d8e 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/A/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/A/fwd.ma
@@ -16,14 +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 (let TMP_1 \def ((A_rect 
-P f f0) a0) in (let TMP_2 \def ((A_rect P f f0) a1) in (f0 a0 TMP_1 a1 
-TMP_2)))].
+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))))