1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs".
19 include "ext/preamble.ma".
21 inductive and3 (P0:Prop) (P1:Prop) (P2:Prop): Prop \def
22 | and3_intro: P0 \to (P1 \to (P2 \to (and3 P0 P1 P2))).
24 inductive or3 (P0:Prop) (P1:Prop) (P2:Prop): Prop \def
25 | or3_intro0: P0 \to (or3 P0 P1 P2)
26 | or3_intro1: P1 \to (or3 P0 P1 P2)
27 | or3_intro2: P2 \to (or3 P0 P1 P2).
29 inductive or4 (P0:Prop) (P1:Prop) (P2:Prop) (P3:Prop): Prop \def
30 | or4_intro0: P0 \to (or4 P0 P1 P2 P3)
31 | or4_intro1: P1 \to (or4 P0 P1 P2 P3)
32 | or4_intro2: P2 \to (or4 P0 P1 P2 P3)
33 | or4_intro3: P3 \to (or4 P0 P1 P2 P3).
35 inductive ex3 (A0:Set) (P0:A0 \to Prop) (P1:A0 \to Prop) (P2:A0 \to Prop):
37 | ex3_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to (ex3 A0
40 inductive ex4 (A0:Set) (P0:A0 \to Prop) (P1:A0 \to Prop) (P2:A0 \to Prop)
41 (P3:A0 \to Prop): Prop \def
42 | ex4_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to ((P3 x0)
43 \to (ex4 A0 P0 P1 P2 P3))))).
45 inductive ex_2 (A0:Set) (A1:Set) (P0:A0 \to (A1 \to Prop)): Prop \def
46 | ex_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to (ex_2 A0 A1
49 inductive ex2_2 (A0:Set) (A1:Set) (P0:A0 \to (A1 \to Prop)) (P1:A0 \to (A1
51 | ex2_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1)
52 \to (ex2_2 A0 A1 P0 P1)))).
54 inductive ex3_2 (A0:Set) (A1:Set) (P0:A0 \to (A1 \to Prop)) (P1:A0 \to (A1
55 \to Prop)) (P2:A0 \to (A1 \to Prop)): Prop \def
56 | ex3_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1)
57 \to ((P2 x0 x1) \to (ex3_2 A0 A1 P0 P1 P2))))).
59 inductive ex4_2 (A0:Set) (A1:Set) (P0:A0 \to (A1 \to Prop)) (P1:A0 \to (A1
60 \to Prop)) (P2:A0 \to (A1 \to Prop)) (P3:A0 \to (A1 \to Prop)): Prop \def
61 | ex4_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1)
62 \to ((P2 x0 x1) \to ((P3 x0 x1) \to (ex4_2 A0 A1 P0 P1 P2 P3)))))).
64 inductive ex_3 (A0:Set) (A1:Set) (A2:Set) (P0:A0 \to (A1 \to (A2 \to Prop))):
66 | ex_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1
67 x2) \to (ex_3 A0 A1 A2 P0)))).
69 inductive ex2_3 (A0:Set) (A1:Set) (A2:Set) (P0:A0 \to (A1 \to (A2 \to Prop)))
70 (P1:A0 \to (A1 \to (A2 \to Prop))): Prop \def
71 | ex2_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0
72 x1 x2) \to ((P1 x0 x1 x2) \to (ex2_3 A0 A1 A2 P0 P1))))).
74 inductive ex3_3 (A0:Set) (A1:Set) (A2:Set) (P0:A0 \to (A1 \to (A2 \to Prop)))
75 (P1:A0 \to (A1 \to (A2 \to Prop))) (P2:A0 \to (A1 \to (A2 \to Prop))): Prop
77 | ex3_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0
78 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to (ex3_3 A0 A1 A2 P0 P1
81 inductive ex4_3 (A0:Set) (A1:Set) (A2:Set) (P0:A0 \to (A1 \to (A2 \to Prop)))
82 (P1:A0 \to (A1 \to (A2 \to Prop))) (P2:A0 \to (A1 \to (A2 \to Prop))) (P3:A0
83 \to (A1 \to (A2 \to Prop))): Prop \def
84 | ex4_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0
85 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to (ex4_3 A0
86 A1 A2 P0 P1 P2 P3))))))).
88 inductive ex3_4 (A0:Set) (A1:Set) (A2:Set) (A3:Set) (P0:A0 \to (A1 \to (A2
89 \to (A3 \to Prop)))) (P1:A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2:A0 \to
90 (A1 \to (A2 \to (A3 \to Prop)))): Prop \def
91 | ex3_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
92 (x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to
93 (ex3_4 A0 A1 A2 A3 P0 P1 P2))))))).
95 inductive ex4_4 (A0:Set) (A1:Set) (A2:Set) (A3:Set) (P0:A0 \to (A1 \to (A2
96 \to (A3 \to Prop)))) (P1:A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2:A0 \to
97 (A1 \to (A2 \to (A3 \to Prop)))) (P3:A0 \to (A1 \to (A2 \to (A3 \to Prop)))):
99 | ex4_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
100 (x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to
101 ((P3 x0 x1 x2 x3) \to (ex4_4 A0 A1 A2 A3 P0 P1 P2 P3)))))))).
103 inductive ex4_5 (A0:Set) (A1:Set) (A2:Set) (A3:Set) (A4:Set) (P0:A0 \to (A1
104 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1:A0 \to (A1 \to (A2 \to (A3 \to (A4
105 \to Prop))))) (P2:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P3:A0 \to
106 (A1 \to (A2 \to (A3 \to (A4 \to Prop))))): Prop \def
107 | ex4_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
108 (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to
109 ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to (ex4_5 A0 A1 A2 A3 A4 P0 P1
112 inductive ex5_5 (A0:Set) (A1:Set) (A2:Set) (A3:Set) (A4:Set) (P0:A0 \to (A1
113 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1:A0 \to (A1 \to (A2 \to (A3 \to (A4
114 \to Prop))))) (P2:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P3:A0 \to
115 (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P4:A0 \to (A1 \to (A2 \to (A3 \to
116 (A4 \to Prop))))): Prop \def
117 | ex5_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
118 (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to
119 ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to ((P4 x0 x1 x2 x3 x4) \to
120 (ex5_5 A0 A1 A2 A3 A4 P0 P1 P2 P3 P4)))))))))).
122 inductive ex6_6 (A0:Set) (A1:Set) (A2:Set) (A3:Set) (A4:Set) (A5:Set) (P0:A0
123 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P1:A0 \to (A1 \to (A2
124 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P2:A0 \to (A1 \to (A2 \to (A3 \to (A4
125 \to (A5 \to Prop)))))) (P3:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to
126 Prop)))))) (P4:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop))))))
127 (P5:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))): Prop \def
128 | ex6_6_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
129 (x3: A3).(\forall (x4: A4).(\forall (x5: A5).((P0 x0 x1 x2 x3 x4 x5) \to ((P1
130 x0 x1 x2 x3 x4 x5) \to ((P2 x0 x1 x2 x3 x4 x5) \to ((P3 x0 x1 x2 x3 x4 x5)
131 \to ((P4 x0 x1 x2 x3 x4 x5) \to ((P5 x0 x1 x2 x3 x4 x5) \to (ex6_6 A0 A1 A2
132 A3 A4 A5 P0 P1 P2 P3 P4 P5)))))))))))).
134 inductive ex6_7 (A0:Set) (A1:Set) (A2:Set) (A3:Set) (A4:Set) (A5:Set)
135 (A6:Set) (P0:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
136 Prop))))))) (P1:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
137 Prop))))))) (P2:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
138 Prop))))))) (P3:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
139 Prop))))))) (P4:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
140 Prop))))))) (P5:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
141 Prop))))))): Prop \def
142 | ex6_7_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
143 (x3: A3).(\forall (x4: A4).(\forall (x5: A5).(\forall (x6: A6).((P0 x0 x1 x2
144 x3 x4 x5 x6) \to ((P1 x0 x1 x2 x3 x4 x5 x6) \to ((P2 x0 x1 x2 x3 x4 x5 x6)
145 \to ((P3 x0 x1 x2 x3 x4 x5 x6) \to ((P4 x0 x1 x2 x3 x4 x5 x6) \to ((P5 x0 x1
146 x2 x3 x4 x5 x6) \to (ex6_7 A0 A1 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4