X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_1A%2Ftypes%2Ffwd.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_1A%2Ftypes%2Ffwd.ma;h=862e581af20af6f6ea7a96d3a9c7def5bd6515e7;hb=d2545ffd201b1aa49887313791386add78fa8603;hp=0000000000000000000000000000000000000000;hpb=57ae1762497a5f3ea75740e2908e04adb8642cc2;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground_1A/types/fwd.ma b/matita/matita/contribs/lambdadelta/ground_1A/types/fwd.ma new file mode 100644 index 000000000..862e581af --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_1A/types/fwd.ma @@ -0,0 +1,419 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +include "ground_1A/types/defs.ma". + +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 + \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (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)])))))). + +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)))). + +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)))))) +\def + \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (P3: +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)]))))))). + +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)))))) +\def + \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (P3: +Prop).(\lambda (P: Prop).(and4_rect P0 P1 P2 P3 P))))). + +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))))))) +\def + \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (P3: +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)])))))))). + +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))))))) +\def + \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (P3: +Prop).(\lambda (P4: Prop).(\lambda (P: Prop).(and5_rect P0 P1 P2 P3 P4 +P)))))). + +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))))))) +\def + \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (P: +Prop).(\lambda (f: ((P0 \to P))).(\lambda (f0: ((P1 \to P))).(\lambda (f1: +((P2 \to P))).(\lambda (o: (or3 P0 P1 P2)).(match o with [(or3_intro0 x) +\Rightarrow (f x) | (or3_intro1 x) \Rightarrow (f0 x) | (or3_intro2 x) +\Rightarrow (f1 x)])))))))). + +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))))))))) +\def + \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (P3: +Prop).(\lambda (P: Prop).(\lambda (f: ((P0 \to P))).(\lambda (f0: ((P1 \to +P))).(\lambda (f1: ((P2 \to P))).(\lambda (f2: ((P3 \to P))).(\lambda (o: +(or4 P0 P1 P2 P3)).(match o with [(or4_intro0 x) \Rightarrow (f x) | +(or4_intro1 x) \Rightarrow (f0 x) | (or4_intro2 x) \Rightarrow (f1 x) | +(or4_intro3 x) \Rightarrow (f2 x)])))))))))). + +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 +P4) \to P))))))))))) +\def + \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (P3: +Prop).(\lambda (P4: Prop).(\lambda (P: Prop).(\lambda (f: ((P0 \to +P))).(\lambda (f0: ((P1 \to P))).(\lambda (f1: ((P2 \to P))).(\lambda (f2: +((P3 \to P))).(\lambda (f3: ((P4 \to P))).(\lambda (o: (or5 P0 P1 P2 P3 +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)])))))))))))). + +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 +P)))))) +\def + \lambda (A0: Type[0]).(\lambda (P0: ((A0 \to Prop))).(\lambda (P1: ((A0 \to +Prop))).(\lambda (P2: ((A0 \to Prop))).(\lambda (P: Prop).(\lambda (f: +((\forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to P)))))).(\lambda +(e: (ex3 A0 P0 P1 P2)).(match e with [(ex3_intro x x0 x1 x2) \Rightarrow (f x +x0 x1 x2)]))))))). + +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 +x0) \to ((P3 x0) \to P)))))) \to ((ex4 A0 P0 P1 P2 P3) \to P))))))) +\def + \lambda (A0: Type[0]).(\lambda (P0: ((A0 \to Prop))).(\lambda (P1: ((A0 \to +Prop))).(\lambda (P2: ((A0 \to Prop))).(\lambda (P3: ((A0 \to +Prop))).(\lambda (P: Prop).(\lambda (f: ((\forall (x0: A0).((P0 x0) \to ((P1 +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)])))))))). + +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))))) +\def + \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (P0: ((A0 \to (A1 \to +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)])))))). + +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 +P))))) \to ((ex2_2 A0 A1 P0 P1) \to P)))))) +\def + \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (P0: ((A0 \to (A1 \to +Prop)))).(\lambda (P1: ((A0 \to (A1 \to Prop)))).(\lambda (P: Prop).(\lambda +(f: ((\forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) \to +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)]))))))). + +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 +x1) \to ((P1 x0 x1) \to ((P2 x0 x1) \to P)))))) \to ((ex3_2 A0 A1 P0 P1 P2) +\to P))))))) +\def + \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (P0: ((A0 \to (A1 \to +Prop)))).(\lambda (P1: ((A0 \to (A1 \to Prop)))).(\lambda (P2: ((A0 \to (A1 +\to Prop)))).(\lambda (P: Prop).(\lambda (f: ((\forall (x0: A0).(\forall (x1: +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)])))))))). + +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: +Prop).(((\forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) \to +((P2 x0 x1) \to ((P3 x0 x1) \to P))))))) \to ((ex4_2 A0 A1 P0 P1 P2 P3) \to +P)))))))) +\def + \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (P0: ((A0 \to (A1 \to +Prop)))).(\lambda (P1: ((A0 \to (A1 \to Prop)))).(\lambda (P2: ((A0 \to (A1 +\to Prop)))).(\lambda (P3: ((A0 \to (A1 \to Prop)))).(\lambda (P: +Prop).(\lambda (f: ((\forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 +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)]))))))))). + +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 +A0 A1 A2 P0) \to P)))))) +\def + \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda +(P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P: Prop).(\lambda (f: +((\forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) \to +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)]))))))). + +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: +A1).(\forall (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to P)))))) \to +((ex2_3 A0 A1 A2 P0 P1) \to P))))))) +\def + \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda +(P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P1: ((A0 \to (A1 \to (A2 +\to Prop))))).(\lambda (P: Prop).(\lambda (f: ((\forall (x0: A0).(\forall +(x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \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)])))))))). + +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: +Prop).(((\forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) +\to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to P))))))) \to ((ex3_3 A0 A1 A2 P0 P1 +P2) \to P)))))))) +\def + \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda +(P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P1: ((A0 \to (A1 \to (A2 +\to Prop))))).(\lambda (P2: ((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P: +Prop).(\lambda (f: ((\forall (x0: A0).(\forall (x1: A1).(\forall (x2: +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)]))))))))). + +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: +((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P: Prop).(((\forall (x0: +A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to +((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to P)))))))) \to ((ex4_3 A0 A1 A2 P0 P1 P2 +P3) \to P))))))))) +\def + \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda +(P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P1: ((A0 \to (A1 \to (A2 +\to Prop))))).(\lambda (P2: ((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P3: +((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P: Prop).(\lambda (f: ((\forall +(x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 +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)])))))))))). + +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: +((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P4: ((A0 \to (A1 \to (A2 \to +Prop))))).(\forall (P: Prop).(((\forall (x0: A0).(\forall (x1: A1).(\forall +(x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 +x2) \to ((P4 x0 x1 x2) \to P))))))))) \to ((ex5_3 A0 A1 A2 P0 P1 P2 P3 P4) +\to P)))))))))) +\def + \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda +(P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P1: ((A0 \to (A1 \to (A2 +\to Prop))))).(\lambda (P2: ((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P3: +((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P4: ((A0 \to (A1 \to (A2 \to +Prop))))).(\lambda (P: Prop).(\lambda (f: ((\forall (x0: A0).(\forall (x1: +A1).(\forall (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) +\to ((P3 x0 x1 x2) \to ((P4 x0 x1 x2) \to P)))))))))).(\lambda (e: (ex5_3 A0 +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)]))))))))))). + +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 +(P2: ((A0 \to (A1 \to (A2 \to (A3 \to Prop)))))).(\forall (P: +Prop).(((\forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: +A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to +P)))))))) \to ((ex3_4 A0 A1 A2 A3 P0 P1 P2) \to P))))))))) +\def + \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda +(A3: Type[0]).(\lambda (P0: ((A0 \to (A1 \to (A2 \to (A3 \to +Prop)))))).(\lambda (P1: ((A0 \to (A1 \to (A2 \to (A3 \to Prop)))))).(\lambda +(P2: ((A0 \to (A1 \to (A2 \to (A3 \to Prop)))))).(\lambda (P: Prop).(\lambda +(f: ((\forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: +A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to +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)])))))))))). + +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 +(P2: ((A0 \to (A1 \to (A2 \to (A3 \to Prop)))))).(\forall (P3: ((A0 \to (A1 +\to (A2 \to (A3 \to Prop)))))).(\forall (P: Prop).(((\forall (x0: +A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: A3).((P0 x0 x1 x2 x3) +\to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to ((P3 x0 x1 x2 x3) \to +P))))))))) \to ((ex4_4 A0 A1 A2 A3 P0 P1 P2 P3) \to P)))))))))) +\def + \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda +(A3: Type[0]).(\lambda (P0: ((A0 \to (A1 \to (A2 \to (A3 \to +Prop)))))).(\lambda (P1: ((A0 \to (A1 \to (A2 \to (A3 \to Prop)))))).(\lambda +(P2: ((A0 \to (A1 \to (A2 \to (A3 \to Prop)))))).(\lambda (P3: ((A0 \to (A1 +\to (A2 \to (A3 \to Prop)))))).(\lambda (P: Prop).(\lambda (f: ((\forall (x0: +A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: A3).((P0 x0 x1 x2 x3) +\to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to ((P3 x0 x1 x2 x3) \to +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)]))))))))))). + +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 +(A4 \to Prop))))))).(\forall (P2: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to +Prop))))))).(\forall (P3: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to +Prop))))))).(\forall (P: Prop).(((\forall (x0: A0).(\forall (x1: A1).(\forall +(x2: A2).(\forall (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 +x1 x2 x3 x4) \to ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to +P)))))))))) \to ((ex4_5 A0 A1 A2 A3 A4 P0 P1 P2 P3) \to P))))))))))) +\def + \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda +(A3: Type[0]).(\lambda (A4: Type[0]).(\lambda (P0: ((A0 \to (A1 \to (A2 \to +(A3 \to (A4 \to Prop))))))).(\lambda (P1: ((A0 \to (A1 \to (A2 \to (A3 \to +(A4 \to Prop))))))).(\lambda (P2: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to +Prop))))))).(\lambda (P3: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to +Prop))))))).(\lambda (P: Prop).(\lambda (f: ((\forall (x0: A0).(\forall (x1: +A1).(\forall (x2: A2).(\forall (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 +x4) \to ((P1 x0 x1 x2 x3 x4) \to ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 +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)])))))))))))). + +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 +(A4 \to Prop))))))).(\forall (P2: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to +Prop))))))).(\forall (P3: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to +Prop))))))).(\forall (P4: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to +Prop))))))).(\forall (P: Prop).(((\forall (x0: A0).(\forall (x1: A1).(\forall +(x2: A2).(\forall (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 +x1 x2 x3 x4) \to ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to ((P4 x0 x1 +x2 x3 x4) \to P))))))))))) \to ((ex5_5 A0 A1 A2 A3 A4 P0 P1 P2 P3 P4) \to +P)))))))))))) +\def + \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda +(A3: Type[0]).(\lambda (A4: Type[0]).(\lambda (P0: ((A0 \to (A1 \to (A2 \to +(A3 \to (A4 \to Prop))))))).(\lambda (P1: ((A0 \to (A1 \to (A2 \to (A3 \to +(A4 \to Prop))))))).(\lambda (P2: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to +Prop))))))).(\lambda (P3: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to +Prop))))))).(\lambda (P4: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to +Prop))))))).(\lambda (P: Prop).(\lambda (f: ((\forall (x0: A0).(\forall (x1: +A1).(\forall (x2: A2).(\forall (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 +x4) \to ((P1 x0 x1 x2 x3 x4) \to ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 +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)]))))))))))))). + +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: +((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\forall (P2: +((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\forall (P3: +((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\forall (P4: +((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\forall (P5: +((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\forall (P: +Prop).(((\forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: +A3).(\forall (x4: A4).(\forall (x5: A5).((P0 x0 x1 x2 x3 x4 x5) \to ((P1 x0 +x1 x2 x3 x4 x5) \to ((P2 x0 x1 x2 x3 x4 x5) \to ((P3 x0 x1 x2 x3 x4 x5) \to +((P4 x0 x1 x2 x3 x4 x5) \to ((P5 x0 x1 x2 x3 x4 x5) \to P))))))))))))) \to +((ex6_6 A0 A1 A2 A3 A4 A5 P0 P1 P2 P3 P4 P5) \to P)))))))))))))) +\def + \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda +(A3: Type[0]).(\lambda (A4: Type[0]).(\lambda (A5: Type[0]).(\lambda (P0: +((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\lambda (P1: +((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\lambda (P2: +((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\lambda (P3: +((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\lambda (P4: +((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\lambda (P5: +((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\lambda (P: +Prop).(\lambda (f: ((\forall (x0: A0).(\forall (x1: A1).(\forall (x2: +A2).(\forall (x3: A3).(\forall (x4: A4).(\forall (x5: A5).((P0 x0 x1 x2 x3 x4 +x5) \to ((P1 x0 x1 x2 x3 x4 x5) \to ((P2 x0 x1 x2 x3 x4 x5) \to ((P3 x0 x1 x2 +x3 x4 x5) \to ((P4 x0 x1 x2 x3 x4 x5) \to ((P5 x0 x1 x2 x3 x4 x5) \to +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)]))))))))))))))). + +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 +\to Prop))))))))).(\forall (P1: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 +\to (A6 \to Prop))))))))).(\forall (P2: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 +\to (A5 \to (A6 \to Prop))))))))).(\forall (P3: ((A0 \to (A1 \to (A2 \to (A3 +\to (A4 \to (A5 \to (A6 \to Prop))))))))).(\forall (P4: ((A0 \to (A1 \to (A2 +\to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))))).(\forall (P5: ((A0 \to (A1 +\to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))))).(\forall (P: +Prop).(((\forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: +A3).(\forall (x4: A4).(\forall (x5: A5).(\forall (x6: A6).((P0 x0 x1 x2 x3 x4 +x5 x6) \to ((P1 x0 x1 x2 x3 x4 x5 x6) \to ((P2 x0 x1 x2 x3 x4 x5 x6) \to ((P3 +x0 x1 x2 x3 x4 x5 x6) \to ((P4 x0 x1 x2 x3 x4 x5 x6) \to ((P5 x0 x1 x2 x3 x4 +x5 x6) \to P)))))))))))))) \to ((ex6_7 A0 A1 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4 +P5) \to P))))))))))))))) +\def + \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda +(A3: Type[0]).(\lambda (A4: Type[0]).(\lambda (A5: Type[0]).(\lambda (A6: +Type[0]).(\lambda (P0: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 +\to Prop))))))))).(\lambda (P1: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 +\to (A6 \to Prop))))))))).(\lambda (P2: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 +\to (A5 \to (A6 \to Prop))))))))).(\lambda (P3: ((A0 \to (A1 \to (A2 \to (A3 +\to (A4 \to (A5 \to (A6 \to Prop))))))))).(\lambda (P4: ((A0 \to (A1 \to (A2 +\to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))))).(\lambda (P5: ((A0 \to (A1 +\to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))))).(\lambda (P: +Prop).(\lambda (f: ((\forall (x0: A0).(\forall (x1: A1).(\forall (x2: +A2).(\forall (x3: A3).(\forall (x4: A4).(\forall (x5: A5).(\forall (x6: +A6).((P0 x0 x1 x2 x3 x4 x5 x6) \to ((P1 x0 x1 x2 x3 x4 x5 x6) \to ((P2 x0 x1 +x2 x3 x4 x5 x6) \to ((P3 x0 x1 x2 x3 x4 x5 x6) \to ((P4 x0 x1 x2 x3 x4 x5 x6) +\to ((P5 x0 x1 x2 x3 x4 x5 x6) \to P))))))))))))))).(\lambda (e: (ex6_7 A0 A1 +A2 A3 A4 A5 A6 P0 P1 P2 P3 P4 P5)).(match e with [(ex6_7_intro x x0 x1 x2 x3 +x4 x5 x6 x7 x8 x9 x10 x11) \Rightarrow (f x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 +x11)])))))))))))))))). +