update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / ground_1 / types / fwd.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_1/types/fwd.ma b/matita/matita/contribs/lambdadelta/ground_1/types/fwd.ma
index d1139518f29705dea03e882d9b7035eba08c8892..7cb7c3108debd85d9f679114ceb472cf21cc982d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_1/types/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/ground_1/types/fwd.ma
@@ -16,7 +16,7 @@
 
 include "ground_1/types/defs.ma".
 
-theorem and3_rect:
+implied lemma and3_rect:
  \forall (P0: Prop).(\forall (P1: Prop).(\forall (P2: Prop).(\forall (P: 
 Type[0]).(((P0 \to (P1 \to (P2 \to P)))) \to ((and3 P0 P1 P2) \to P)))))
 \def
@@ -24,14 +24,14 @@ Type[0]).(((P0 \to (P1 \to (P2 \to P)))) \to ((and3 P0 P1 P2) \to P)))))
 Type[0]).(\lambda (f: ((P0 \to (P1 \to (P2 \to P))))).(\lambda (a: (and3 P0 
 P1 P2)).(match a with [(and3_intro x x0 x1) \Rightarrow (f x x0 x1)])))))).
 
-theorem and3_ind:
+implied lemma and3_ind:
  \forall (P0: Prop).(\forall (P1: Prop).(\forall (P2: Prop).(\forall (P: 
 Prop).(((P0 \to (P1 \to (P2 \to P)))) \to ((and3 P0 P1 P2) \to P)))))
 \def
  \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (P: 
 Prop).(and3_rect P0 P1 P2 P)))).
 
-theorem and4_rect:
+implied lemma and4_rect:
  \forall (P0: Prop).(\forall (P1: Prop).(\forall (P2: Prop).(\forall (P3: 
 Prop).(\forall (P: Type[0]).(((P0 \to (P1 \to (P2 \to (P3 \to P))))) \to 
 ((and4 P0 P1 P2 P3) \to P))))))
@@ -41,7 +41,7 @@ Prop).(\lambda (P: Type[0]).(\lambda (f: ((P0 \to (P1 \to (P2 \to (P3 \to
 P)))))).(\lambda (a: (and4 P0 P1 P2 P3)).(match a with [(and4_intro x x0 x1 
 x2) \Rightarrow (f x x0 x1 x2)]))))))).
 
-theorem and4_ind:
+implied lemma and4_ind:
  \forall (P0: Prop).(\forall (P1: Prop).(\forall (P2: Prop).(\forall (P3: 
 Prop).(\forall (P: Prop).(((P0 \to (P1 \to (P2 \to (P3 \to P))))) \to ((and4 
 P0 P1 P2 P3) \to P))))))
@@ -49,7 +49,7 @@ P0 P1 P2 P3) \to P))))))
  \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (P3: 
 Prop).(\lambda (P: Prop).(and4_rect P0 P1 P2 P3 P))))).
 
-theorem and5_rect:
+implied lemma and5_rect:
  \forall (P0: Prop).(\forall (P1: Prop).(\forall (P2: Prop).(\forall (P3: 
 Prop).(\forall (P4: Prop).(\forall (P: Type[0]).(((P0 \to (P1 \to (P2 \to (P3 
 \to (P4 \to P)))))) \to ((and5 P0 P1 P2 P3 P4) \to P)))))))
@@ -59,7 +59,7 @@ Prop).(\lambda (P4: Prop).(\lambda (P: Type[0]).(\lambda (f: ((P0 \to (P1 \to
 (P2 \to (P3 \to (P4 \to P))))))).(\lambda (a: (and5 P0 P1 P2 P3 P4)).(match a 
 with [(and5_intro x x0 x1 x2 x3) \Rightarrow (f x x0 x1 x2 x3)])))))))).
 
-theorem and5_ind:
+implied lemma and5_ind:
  \forall (P0: Prop).(\forall (P1: Prop).(\forall (P2: Prop).(\forall (P3: 
 Prop).(\forall (P4: Prop).(\forall (P: Prop).(((P0 \to (P1 \to (P2 \to (P3 
 \to (P4 \to P)))))) \to ((and5 P0 P1 P2 P3 P4) \to P)))))))
@@ -68,7 +68,7 @@ Prop).(\forall (P4: Prop).(\forall (P: Prop).(((P0 \to (P1 \to (P2 \to (P3
 Prop).(\lambda (P4: Prop).(\lambda (P: Prop).(and5_rect P0 P1 P2 P3 P4 
 P)))))).
 
-theorem or3_ind:
+implied lemma or3_ind:
  \forall (P0: Prop).(\forall (P1: Prop).(\forall (P2: Prop).(\forall (P: 
 Prop).(((P0 \to P)) \to (((P1 \to P)) \to (((P2 \to P)) \to ((or3 P0 P1 P2) 
 \to P)))))))
@@ -79,7 +79,7 @@ Prop).(\lambda (f: ((P0 \to P))).(\lambda (f0: ((P1 \to P))).(\lambda (f1:
 \Rightarrow (f x) | (or3_intro1 x) \Rightarrow (f0 x) | (or3_intro2 x) 
 \Rightarrow (f1 x)])))))))).
 
-theorem or4_ind:
+implied lemma or4_ind:
  \forall (P0: Prop).(\forall (P1: Prop).(\forall (P2: Prop).(\forall (P3: 
 Prop).(\forall (P: Prop).(((P0 \to P)) \to (((P1 \to P)) \to (((P2 \to P)) 
 \to (((P3 \to P)) \to ((or4 P0 P1 P2 P3) \to P)))))))))
@@ -91,7 +91,7 @@ P))).(\lambda (f1: ((P2 \to P))).(\lambda (f2: ((P3 \to P))).(\lambda (o:
 (or4_intro1 x) \Rightarrow (f0 x) | (or4_intro2 x) \Rightarrow (f1 x) | 
 (or4_intro3 x) \Rightarrow (f2 x)])))))))))).
 
-theorem or5_ind:
+implied lemma or5_ind:
  \forall (P0: Prop).(\forall (P1: Prop).(\forall (P2: Prop).(\forall (P3: 
 Prop).(\forall (P4: Prop).(\forall (P: Prop).(((P0 \to P)) \to (((P1 \to P)) 
 \to (((P2 \to P)) \to (((P3 \to P)) \to (((P4 \to P)) \to ((or5 P0 P1 P2 P3 
@@ -105,7 +105,7 @@ P4)).(match o with [(or5_intro0 x) \Rightarrow (f x) | (or5_intro1 x)
 \Rightarrow (f0 x) | (or5_intro2 x) \Rightarrow (f1 x) | (or5_intro3 x) 
 \Rightarrow (f2 x) | (or5_intro4 x) \Rightarrow (f3 x)])))))))))))).
 
-theorem ex3_ind:
+implied lemma ex3_ind:
  \forall (A0: Type[0]).(\forall (P0: ((A0 \to Prop))).(\forall (P1: ((A0 \to 
 Prop))).(\forall (P2: ((A0 \to Prop))).(\forall (P: Prop).(((\forall (x0: 
 A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to P))))) \to ((ex3 A0 P0 P1 P2) \to 
@@ -117,7 +117,7 @@ Prop))).(\lambda (P2: ((A0 \to Prop))).(\lambda (P: Prop).(\lambda (f:
 (e: (ex3 A0 P0 P1 P2)).(match e with [(ex3_intro x x0 x1 x2) \Rightarrow (f x 
 x0 x1 x2)]))))))).
 
-theorem ex4_ind:
+implied lemma ex4_ind:
  \forall (A0: Type[0]).(\forall (P0: ((A0 \to Prop))).(\forall (P1: ((A0 \to 
 Prop))).(\forall (P2: ((A0 \to Prop))).(\forall (P3: ((A0 \to 
 Prop))).(\forall (P: Prop).(((\forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 
@@ -130,7 +130,7 @@ x0) \to ((P2 x0) \to ((P3 x0) \to P))))))).(\lambda (e: (ex4 A0 P0 P1 P2
 P3)).(match e with [(ex4_intro x x0 x1 x2 x3) \Rightarrow (f x x0 x1 x2 
 x3)])))))))).
 
-theorem ex_2_ind:
+implied lemma ex_2_ind:
  \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (P0: ((A0 \to (A1 \to 
 Prop)))).(\forall (P: Prop).(((\forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) 
 \to P)))) \to ((ex_2 A0 A1 P0) \to P)))))
@@ -140,7 +140,7 @@ Prop)))).(\lambda (P: Prop).(\lambda (f: ((\forall (x0: A0).(\forall (x1:
 A1).((P0 x0 x1) \to P))))).(\lambda (e: (ex_2 A0 A1 P0)).(match e with 
 [(ex_2_intro x x0 x1) \Rightarrow (f x x0 x1)])))))).
 
-theorem ex2_2_ind:
+implied lemma ex2_2_ind:
  \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (P0: ((A0 \to (A1 \to 
 Prop)))).(\forall (P1: ((A0 \to (A1 \to Prop)))).(\forall (P: 
 Prop).(((\forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) \to 
@@ -152,7 +152,7 @@ Prop)))).(\lambda (P1: ((A0 \to (A1 \to Prop)))).(\lambda (P: Prop).(\lambda
 P)))))).(\lambda (e: (ex2_2 A0 A1 P0 P1)).(match e with [(ex2_2_intro x x0 x1 
 x2) \Rightarrow (f x x0 x1 x2)]))))))).
 
-theorem ex3_2_ind:
+implied lemma ex3_2_ind:
  \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (P0: ((A0 \to (A1 \to 
 Prop)))).(\forall (P1: ((A0 \to (A1 \to Prop)))).(\forall (P2: ((A0 \to (A1 
 \to Prop)))).(\forall (P: Prop).(((\forall (x0: A0).(\forall (x1: A1).((P0 x0 
@@ -166,7 +166,7 @@ A1).((P0 x0 x1) \to ((P1 x0 x1) \to ((P2 x0 x1) \to P))))))).(\lambda (e:
 (ex3_2 A0 A1 P0 P1 P2)).(match e with [(ex3_2_intro x x0 x1 x2 x3) 
 \Rightarrow (f x x0 x1 x2 x3)])))))))).
 
-theorem ex4_2_ind:
+implied lemma ex4_2_ind:
  \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (P0: ((A0 \to (A1 \to 
 Prop)))).(\forall (P1: ((A0 \to (A1 \to Prop)))).(\forall (P2: ((A0 \to (A1 
 \to Prop)))).(\forall (P3: ((A0 \to (A1 \to Prop)))).(\forall (P: 
@@ -182,7 +182,7 @@ x0 x1) \to ((P2 x0 x1) \to ((P3 x0 x1) \to P)))))))).(\lambda (e: (ex4_2 A0
 A1 P0 P1 P2 P3)).(match e with [(ex4_2_intro x x0 x1 x2 x3 x4) \Rightarrow (f 
 x x0 x1 x2 x3 x4)]))))))))).
 
-theorem ex_3_ind:
+implied lemma ex_3_ind:
  \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall 
 (P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P: Prop).(((\forall (x0: 
 A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) \to P))))) \to ((ex_3 
@@ -194,7 +194,7 @@ A0 A1 A2 P0) \to P))))))
 P)))))).(\lambda (e: (ex_3 A0 A1 A2 P0)).(match e with [(ex_3_intro x x0 x1 
 x2) \Rightarrow (f x x0 x1 x2)]))))))).
 
-theorem ex2_3_ind:
+implied lemma ex2_3_ind:
  \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall 
 (P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P1: ((A0 \to (A1 \to (A2 
 \to Prop))))).(\forall (P: Prop).(((\forall (x0: A0).(\forall (x1: 
@@ -208,7 +208,7 @@ A1).(\forall (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to P)))))) \to
 P))))))).(\lambda (e: (ex2_3 A0 A1 A2 P0 P1)).(match e with [(ex2_3_intro x 
 x0 x1 x2 x3) \Rightarrow (f x x0 x1 x2 x3)])))))))).
 
-theorem ex3_3_ind:
+implied lemma ex3_3_ind:
  \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall 
 (P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P1: ((A0 \to (A1 \to (A2 
 \to Prop))))).(\forall (P2: ((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P: 
@@ -224,7 +224,7 @@ A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to
 P)))))))).(\lambda (e: (ex3_3 A0 A1 A2 P0 P1 P2)).(match e with [(ex3_3_intro 
 x x0 x1 x2 x3 x4) \Rightarrow (f x x0 x1 x2 x3 x4)]))))))))).
 
-theorem ex4_3_ind:
+implied lemma ex4_3_ind:
  \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall 
 (P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P1: ((A0 \to (A1 \to (A2 
 \to Prop))))).(\forall (P2: ((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P3: 
@@ -242,7 +242,7 @@ x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to P))))))))).(\lambda (e: (ex4_3
 A0 A1 A2 P0 P1 P2 P3)).(match e with [(ex4_3_intro x x0 x1 x2 x3 x4 x5) 
 \Rightarrow (f x x0 x1 x2 x3 x4 x5)])))))))))).
 
-theorem ex5_3_ind:
+implied lemma ex5_3_ind:
  \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall 
 (P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P1: ((A0 \to (A1 \to (A2 
 \to Prop))))).(\forall (P2: ((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P3: 
@@ -262,7 +262,7 @@ A1).(\forall (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2)
 A1 A2 P0 P1 P2 P3 P4)).(match e with [(ex5_3_intro x x0 x1 x2 x3 x4 x5 x6) 
 \Rightarrow (f x x0 x1 x2 x3 x4 x5 x6)]))))))))))).
 
-theorem ex3_4_ind:
+implied lemma ex3_4_ind:
  \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall 
 (A3: Type[0]).(\forall (P0: ((A0 \to (A1 \to (A2 \to (A3 \to 
 Prop)))))).(\forall (P1: ((A0 \to (A1 \to (A2 \to (A3 \to Prop)))))).(\forall 
@@ -281,7 +281,7 @@ P))))))))).(\lambda (e: (ex3_4 A0 A1 A2 A3 P0 P1 P2)).(match e with
 [(ex3_4_intro x x0 x1 x2 x3 x4 x5) \Rightarrow (f x x0 x1 x2 x3 x4 
 x5)])))))))))).
 
-theorem ex4_4_ind:
+implied lemma ex4_4_ind:
  \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall 
 (A3: Type[0]).(\forall (P0: ((A0 \to (A1 \to (A2 \to (A3 \to 
 Prop)))))).(\forall (P1: ((A0 \to (A1 \to (A2 \to (A3 \to Prop)))))).(\forall 
@@ -302,7 +302,7 @@ P)))))))))).(\lambda (e: (ex4_4 A0 A1 A2 A3 P0 P1 P2 P3)).(match e with
 [(ex4_4_intro x x0 x1 x2 x3 x4 x5 x6) \Rightarrow (f x x0 x1 x2 x3 x4 x5 
 x6)]))))))))))).
 
-theorem ex4_5_ind:
+implied lemma ex4_5_ind:
  \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall 
 (A3: Type[0]).(\forall (A4: Type[0]).(\forall (P0: ((A0 \to (A1 \to (A2 \to 
 (A3 \to (A4 \to Prop))))))).(\forall (P1: ((A0 \to (A1 \to (A2 \to (A3 \to 
@@ -325,7 +325,7 @@ x4) \to P))))))))))).(\lambda (e: (ex4_5 A0 A1 A2 A3 A4 P0 P1 P2 P3)).(match
 e with [(ex4_5_intro x x0 x1 x2 x3 x4 x5 x6 x7) \Rightarrow (f x x0 x1 x2 x3 
 x4 x5 x6 x7)])))))))))))).
 
-theorem ex5_5_ind:
+implied lemma ex5_5_ind:
  \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall 
 (A3: Type[0]).(\forall (A4: Type[0]).(\forall (P0: ((A0 \to (A1 \to (A2 \to 
 (A3 \to (A4 \to Prop))))))).(\forall (P1: ((A0 \to (A1 \to (A2 \to (A3 \to 
@@ -351,7 +351,7 @@ x4) \to ((P4 x0 x1 x2 x3 x4) \to P)))))))))))).(\lambda (e: (ex5_5 A0 A1 A2
 A3 A4 P0 P1 P2 P3 P4)).(match e with [(ex5_5_intro x x0 x1 x2 x3 x4 x5 x6 x7 
 x8) \Rightarrow (f x x0 x1 x2 x3 x4 x5 x6 x7 x8)]))))))))))))).
 
-theorem ex6_6_ind:
+implied lemma ex6_6_ind:
  \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall 
 (A3: Type[0]).(\forall (A4: Type[0]).(\forall (A5: Type[0]).(\forall (P0: 
 ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\forall (P1: 
@@ -382,7 +382,7 @@ P)))))))))))))).(\lambda (e: (ex6_6 A0 A1 A2 A3 A4 A5 P0 P1 P2 P3 P4
 P5)).(match e with [(ex6_6_intro x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) 
 \Rightarrow (f x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)]))))))))))))))).
 
-theorem ex6_7_ind:
+implied lemma ex6_7_ind:
  \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall 
 (A3: Type[0]).(\forall (A4: Type[0]).(\forall (A5: Type[0]).(\forall (A6: 
 Type[0]).(\forall (P0: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6