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 0f5f065dffdb8647d11f7408858b2d526092f4e3..9e2eb7d8e65fb3c25903e38302f734bc4f33109d 100644 (file)
--- 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))))