+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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_1/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)])))))))))))))))).
-
projects / helm.git / blobdiff