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 include "ground_1/types/defs.ma".
20 \forall (P0: Prop).(\forall (P1: Prop).(\forall (P2: Prop).(\forall (P:
21 Type[0]).(((P0 \to (P1 \to (P2 \to P)))) \to ((and3 P0 P1 P2) \to P)))))
23 \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (P:
24 Type[0]).(\lambda (f: ((P0 \to (P1 \to (P2 \to P))))).(\lambda (a: (and3 P0
25 P1 P2)).(match a with [(and3_intro x x0 x1) \Rightarrow (f x x0 x1)])))))).
28 \forall (P0: Prop).(\forall (P1: Prop).(\forall (P2: Prop).(\forall (P:
29 Prop).(((P0 \to (P1 \to (P2 \to P)))) \to ((and3 P0 P1 P2) \to P)))))
31 \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (P:
32 Prop).(and3_rect P0 P1 P2 P)))).
35 \forall (P0: Prop).(\forall (P1: Prop).(\forall (P2: Prop).(\forall (P3:
36 Prop).(\forall (P: Type[0]).(((P0 \to (P1 \to (P2 \to (P3 \to P))))) \to
37 ((and4 P0 P1 P2 P3) \to P))))))
39 \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (P3:
40 Prop).(\lambda (P: Type[0]).(\lambda (f: ((P0 \to (P1 \to (P2 \to (P3 \to
41 P)))))).(\lambda (a: (and4 P0 P1 P2 P3)).(match a with [(and4_intro x x0 x1
42 x2) \Rightarrow (f x x0 x1 x2)]))))))).
45 \forall (P0: Prop).(\forall (P1: Prop).(\forall (P2: Prop).(\forall (P3:
46 Prop).(\forall (P: Prop).(((P0 \to (P1 \to (P2 \to (P3 \to P))))) \to ((and4
47 P0 P1 P2 P3) \to P))))))
49 \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (P3:
50 Prop).(\lambda (P: Prop).(and4_rect P0 P1 P2 P3 P))))).
53 \forall (P0: Prop).(\forall (P1: Prop).(\forall (P2: Prop).(\forall (P3:
54 Prop).(\forall (P4: Prop).(\forall (P: Type[0]).(((P0 \to (P1 \to (P2 \to (P3
55 \to (P4 \to P)))))) \to ((and5 P0 P1 P2 P3 P4) \to P)))))))
57 \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (P3:
58 Prop).(\lambda (P4: Prop).(\lambda (P: Type[0]).(\lambda (f: ((P0 \to (P1 \to
59 (P2 \to (P3 \to (P4 \to P))))))).(\lambda (a: (and5 P0 P1 P2 P3 P4)).(match a
60 with [(and5_intro x x0 x1 x2 x3) \Rightarrow (f x x0 x1 x2 x3)])))))))).
63 \forall (P0: Prop).(\forall (P1: Prop).(\forall (P2: Prop).(\forall (P3:
64 Prop).(\forall (P4: Prop).(\forall (P: Prop).(((P0 \to (P1 \to (P2 \to (P3
65 \to (P4 \to P)))))) \to ((and5 P0 P1 P2 P3 P4) \to P)))))))
67 \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (P3:
68 Prop).(\lambda (P4: Prop).(\lambda (P: Prop).(and5_rect P0 P1 P2 P3 P4
72 \forall (P0: Prop).(\forall (P1: Prop).(\forall (P2: Prop).(\forall (P:
73 Prop).(((P0 \to P)) \to (((P1 \to P)) \to (((P2 \to P)) \to ((or3 P0 P1 P2)
76 \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (P:
77 Prop).(\lambda (f: ((P0 \to P))).(\lambda (f0: ((P1 \to P))).(\lambda (f1:
78 ((P2 \to P))).(\lambda (o: (or3 P0 P1 P2)).(match o with [(or3_intro0 x)
79 \Rightarrow (f x) | (or3_intro1 x) \Rightarrow (f0 x) | (or3_intro2 x)
80 \Rightarrow (f1 x)])))))))).
83 \forall (P0: Prop).(\forall (P1: Prop).(\forall (P2: Prop).(\forall (P3:
84 Prop).(\forall (P: Prop).(((P0 \to P)) \to (((P1 \to P)) \to (((P2 \to P))
85 \to (((P3 \to P)) \to ((or4 P0 P1 P2 P3) \to P)))))))))
87 \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (P3:
88 Prop).(\lambda (P: Prop).(\lambda (f: ((P0 \to P))).(\lambda (f0: ((P1 \to
89 P))).(\lambda (f1: ((P2 \to P))).(\lambda (f2: ((P3 \to P))).(\lambda (o:
90 (or4 P0 P1 P2 P3)).(match o with [(or4_intro0 x) \Rightarrow (f x) |
91 (or4_intro1 x) \Rightarrow (f0 x) | (or4_intro2 x) \Rightarrow (f1 x) |
92 (or4_intro3 x) \Rightarrow (f2 x)])))))))))).
95 \forall (P0: Prop).(\forall (P1: Prop).(\forall (P2: Prop).(\forall (P3:
96 Prop).(\forall (P4: Prop).(\forall (P: Prop).(((P0 \to P)) \to (((P1 \to P))
97 \to (((P2 \to P)) \to (((P3 \to P)) \to (((P4 \to P)) \to ((or5 P0 P1 P2 P3
100 \lambda (P0: Prop).(\lambda (P1: Prop).(\lambda (P2: Prop).(\lambda (P3:
101 Prop).(\lambda (P4: Prop).(\lambda (P: Prop).(\lambda (f: ((P0 \to
102 P))).(\lambda (f0: ((P1 \to P))).(\lambda (f1: ((P2 \to P))).(\lambda (f2:
103 ((P3 \to P))).(\lambda (f3: ((P4 \to P))).(\lambda (o: (or5 P0 P1 P2 P3
104 P4)).(match o with [(or5_intro0 x) \Rightarrow (f x) | (or5_intro1 x)
105 \Rightarrow (f0 x) | (or5_intro2 x) \Rightarrow (f1 x) | (or5_intro3 x)
106 \Rightarrow (f2 x) | (or5_intro4 x) \Rightarrow (f3 x)])))))))))))).
109 \forall (A0: Type[0]).(\forall (P0: ((A0 \to Prop))).(\forall (P1: ((A0 \to
110 Prop))).(\forall (P2: ((A0 \to Prop))).(\forall (P: Prop).(((\forall (x0:
111 A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to P))))) \to ((ex3 A0 P0 P1 P2) \to
114 \lambda (A0: Type[0]).(\lambda (P0: ((A0 \to Prop))).(\lambda (P1: ((A0 \to
115 Prop))).(\lambda (P2: ((A0 \to Prop))).(\lambda (P: Prop).(\lambda (f:
116 ((\forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to P)))))).(\lambda
117 (e: (ex3 A0 P0 P1 P2)).(match e with [(ex3_intro x x0 x1 x2) \Rightarrow (f x
121 \forall (A0: Type[0]).(\forall (P0: ((A0 \to Prop))).(\forall (P1: ((A0 \to
122 Prop))).(\forall (P2: ((A0 \to Prop))).(\forall (P3: ((A0 \to
123 Prop))).(\forall (P: Prop).(((\forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2
124 x0) \to ((P3 x0) \to P)))))) \to ((ex4 A0 P0 P1 P2 P3) \to P)))))))
126 \lambda (A0: Type[0]).(\lambda (P0: ((A0 \to Prop))).(\lambda (P1: ((A0 \to
127 Prop))).(\lambda (P2: ((A0 \to Prop))).(\lambda (P3: ((A0 \to
128 Prop))).(\lambda (P: Prop).(\lambda (f: ((\forall (x0: A0).((P0 x0) \to ((P1
129 x0) \to ((P2 x0) \to ((P3 x0) \to P))))))).(\lambda (e: (ex4 A0 P0 P1 P2
130 P3)).(match e with [(ex4_intro x x0 x1 x2 x3) \Rightarrow (f x x0 x1 x2
134 \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (P0: ((A0 \to (A1 \to
135 Prop)))).(\forall (P: Prop).(((\forall (x0: A0).(\forall (x1: A1).((P0 x0 x1)
136 \to P)))) \to ((ex_2 A0 A1 P0) \to P)))))
138 \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (P0: ((A0 \to (A1 \to
139 Prop)))).(\lambda (P: Prop).(\lambda (f: ((\forall (x0: A0).(\forall (x1:
140 A1).((P0 x0 x1) \to P))))).(\lambda (e: (ex_2 A0 A1 P0)).(match e with
141 [(ex_2_intro x x0 x1) \Rightarrow (f x x0 x1)])))))).
144 \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (P0: ((A0 \to (A1 \to
145 Prop)))).(\forall (P1: ((A0 \to (A1 \to Prop)))).(\forall (P:
146 Prop).(((\forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) \to
147 P))))) \to ((ex2_2 A0 A1 P0 P1) \to P))))))
149 \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (P0: ((A0 \to (A1 \to
150 Prop)))).(\lambda (P1: ((A0 \to (A1 \to Prop)))).(\lambda (P: Prop).(\lambda
151 (f: ((\forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) \to
152 P)))))).(\lambda (e: (ex2_2 A0 A1 P0 P1)).(match e with [(ex2_2_intro x x0 x1
153 x2) \Rightarrow (f x x0 x1 x2)]))))))).
156 \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (P0: ((A0 \to (A1 \to
157 Prop)))).(\forall (P1: ((A0 \to (A1 \to Prop)))).(\forall (P2: ((A0 \to (A1
158 \to Prop)))).(\forall (P: Prop).(((\forall (x0: A0).(\forall (x1: A1).((P0 x0
159 x1) \to ((P1 x0 x1) \to ((P2 x0 x1) \to P)))))) \to ((ex3_2 A0 A1 P0 P1 P2)
162 \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (P0: ((A0 \to (A1 \to
163 Prop)))).(\lambda (P1: ((A0 \to (A1 \to Prop)))).(\lambda (P2: ((A0 \to (A1
164 \to Prop)))).(\lambda (P: Prop).(\lambda (f: ((\forall (x0: A0).(\forall (x1:
165 A1).((P0 x0 x1) \to ((P1 x0 x1) \to ((P2 x0 x1) \to P))))))).(\lambda (e:
166 (ex3_2 A0 A1 P0 P1 P2)).(match e with [(ex3_2_intro x x0 x1 x2 x3)
167 \Rightarrow (f x x0 x1 x2 x3)])))))))).
170 \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (P0: ((A0 \to (A1 \to
171 Prop)))).(\forall (P1: ((A0 \to (A1 \to Prop)))).(\forall (P2: ((A0 \to (A1
172 \to Prop)))).(\forall (P3: ((A0 \to (A1 \to Prop)))).(\forall (P:
173 Prop).(((\forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) \to
174 ((P2 x0 x1) \to ((P3 x0 x1) \to P))))))) \to ((ex4_2 A0 A1 P0 P1 P2 P3) \to
177 \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (P0: ((A0 \to (A1 \to
178 Prop)))).(\lambda (P1: ((A0 \to (A1 \to Prop)))).(\lambda (P2: ((A0 \to (A1
179 \to Prop)))).(\lambda (P3: ((A0 \to (A1 \to Prop)))).(\lambda (P:
180 Prop).(\lambda (f: ((\forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1
181 x0 x1) \to ((P2 x0 x1) \to ((P3 x0 x1) \to P)))))))).(\lambda (e: (ex4_2 A0
182 A1 P0 P1 P2 P3)).(match e with [(ex4_2_intro x x0 x1 x2 x3 x4) \Rightarrow (f
183 x x0 x1 x2 x3 x4)]))))))))).
186 \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall
187 (P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P: Prop).(((\forall (x0:
188 A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) \to P))))) \to ((ex_3
189 A0 A1 A2 P0) \to P))))))
191 \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda
192 (P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P: Prop).(\lambda (f:
193 ((\forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) \to
194 P)))))).(\lambda (e: (ex_3 A0 A1 A2 P0)).(match e with [(ex_3_intro x x0 x1
195 x2) \Rightarrow (f x x0 x1 x2)]))))))).
198 \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall
199 (P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P1: ((A0 \to (A1 \to (A2
200 \to Prop))))).(\forall (P: Prop).(((\forall (x0: A0).(\forall (x1:
201 A1).(\forall (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to P)))))) \to
202 ((ex2_3 A0 A1 A2 P0 P1) \to P)))))))
204 \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda
205 (P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P1: ((A0 \to (A1 \to (A2
206 \to Prop))))).(\lambda (P: Prop).(\lambda (f: ((\forall (x0: A0).(\forall
207 (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to
208 P))))))).(\lambda (e: (ex2_3 A0 A1 A2 P0 P1)).(match e with [(ex2_3_intro x
209 x0 x1 x2 x3) \Rightarrow (f x x0 x1 x2 x3)])))))))).
212 \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall
213 (P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P1: ((A0 \to (A1 \to (A2
214 \to Prop))))).(\forall (P2: ((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P:
215 Prop).(((\forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2)
216 \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to P))))))) \to ((ex3_3 A0 A1 A2 P0 P1
219 \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda
220 (P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P1: ((A0 \to (A1 \to (A2
221 \to Prop))))).(\lambda (P2: ((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P:
222 Prop).(\lambda (f: ((\forall (x0: A0).(\forall (x1: A1).(\forall (x2:
223 A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to
224 P)))))))).(\lambda (e: (ex3_3 A0 A1 A2 P0 P1 P2)).(match e with [(ex3_3_intro
225 x x0 x1 x2 x3 x4) \Rightarrow (f x x0 x1 x2 x3 x4)]))))))))).
228 \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall
229 (P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P1: ((A0 \to (A1 \to (A2
230 \to Prop))))).(\forall (P2: ((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P3:
231 ((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P: Prop).(((\forall (x0:
232 A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to
233 ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to P)))))))) \to ((ex4_3 A0 A1 A2 P0 P1 P2
236 \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda
237 (P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P1: ((A0 \to (A1 \to (A2
238 \to Prop))))).(\lambda (P2: ((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P3:
239 ((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P: Prop).(\lambda (f: ((\forall
240 (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1
241 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to P))))))))).(\lambda (e: (ex4_3
242 A0 A1 A2 P0 P1 P2 P3)).(match e with [(ex4_3_intro x x0 x1 x2 x3 x4 x5)
243 \Rightarrow (f x x0 x1 x2 x3 x4 x5)])))))))))).
246 \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall
247 (P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P1: ((A0 \to (A1 \to (A2
248 \to Prop))))).(\forall (P2: ((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P3:
249 ((A0 \to (A1 \to (A2 \to Prop))))).(\forall (P4: ((A0 \to (A1 \to (A2 \to
250 Prop))))).(\forall (P: Prop).(((\forall (x0: A0).(\forall (x1: A1).(\forall
251 (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1
252 x2) \to ((P4 x0 x1 x2) \to P))))))))) \to ((ex5_3 A0 A1 A2 P0 P1 P2 P3 P4)
255 \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda
256 (P0: ((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P1: ((A0 \to (A1 \to (A2
257 \to Prop))))).(\lambda (P2: ((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P3:
258 ((A0 \to (A1 \to (A2 \to Prop))))).(\lambda (P4: ((A0 \to (A1 \to (A2 \to
259 Prop))))).(\lambda (P: Prop).(\lambda (f: ((\forall (x0: A0).(\forall (x1:
260 A1).(\forall (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2)
261 \to ((P3 x0 x1 x2) \to ((P4 x0 x1 x2) \to P)))))))))).(\lambda (e: (ex5_3 A0
262 A1 A2 P0 P1 P2 P3 P4)).(match e with [(ex5_3_intro x x0 x1 x2 x3 x4 x5 x6)
263 \Rightarrow (f x x0 x1 x2 x3 x4 x5 x6)]))))))))))).
266 \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall
267 (A3: Type[0]).(\forall (P0: ((A0 \to (A1 \to (A2 \to (A3 \to
268 Prop)))))).(\forall (P1: ((A0 \to (A1 \to (A2 \to (A3 \to Prop)))))).(\forall
269 (P2: ((A0 \to (A1 \to (A2 \to (A3 \to Prop)))))).(\forall (P:
270 Prop).(((\forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3:
271 A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to
272 P)))))))) \to ((ex3_4 A0 A1 A2 A3 P0 P1 P2) \to P)))))))))
274 \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda
275 (A3: Type[0]).(\lambda (P0: ((A0 \to (A1 \to (A2 \to (A3 \to
276 Prop)))))).(\lambda (P1: ((A0 \to (A1 \to (A2 \to (A3 \to Prop)))))).(\lambda
277 (P2: ((A0 \to (A1 \to (A2 \to (A3 \to Prop)))))).(\lambda (P: Prop).(\lambda
278 (f: ((\forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3:
279 A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to
280 P))))))))).(\lambda (e: (ex3_4 A0 A1 A2 A3 P0 P1 P2)).(match e with
281 [(ex3_4_intro x x0 x1 x2 x3 x4 x5) \Rightarrow (f x x0 x1 x2 x3 x4
285 \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall
286 (A3: Type[0]).(\forall (P0: ((A0 \to (A1 \to (A2 \to (A3 \to
287 Prop)))))).(\forall (P1: ((A0 \to (A1 \to (A2 \to (A3 \to Prop)))))).(\forall
288 (P2: ((A0 \to (A1 \to (A2 \to (A3 \to Prop)))))).(\forall (P3: ((A0 \to (A1
289 \to (A2 \to (A3 \to Prop)))))).(\forall (P: Prop).(((\forall (x0:
290 A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: A3).((P0 x0 x1 x2 x3)
291 \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to ((P3 x0 x1 x2 x3) \to
292 P))))))))) \to ((ex4_4 A0 A1 A2 A3 P0 P1 P2 P3) \to P))))))))))
294 \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda
295 (A3: Type[0]).(\lambda (P0: ((A0 \to (A1 \to (A2 \to (A3 \to
296 Prop)))))).(\lambda (P1: ((A0 \to (A1 \to (A2 \to (A3 \to Prop)))))).(\lambda
297 (P2: ((A0 \to (A1 \to (A2 \to (A3 \to Prop)))))).(\lambda (P3: ((A0 \to (A1
298 \to (A2 \to (A3 \to Prop)))))).(\lambda (P: Prop).(\lambda (f: ((\forall (x0:
299 A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: A3).((P0 x0 x1 x2 x3)
300 \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to ((P3 x0 x1 x2 x3) \to
301 P)))))))))).(\lambda (e: (ex4_4 A0 A1 A2 A3 P0 P1 P2 P3)).(match e with
302 [(ex4_4_intro x x0 x1 x2 x3 x4 x5 x6) \Rightarrow (f x x0 x1 x2 x3 x4 x5
306 \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall
307 (A3: Type[0]).(\forall (A4: Type[0]).(\forall (P0: ((A0 \to (A1 \to (A2 \to
308 (A3 \to (A4 \to Prop))))))).(\forall (P1: ((A0 \to (A1 \to (A2 \to (A3 \to
309 (A4 \to Prop))))))).(\forall (P2: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to
310 Prop))))))).(\forall (P3: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to
311 Prop))))))).(\forall (P: Prop).(((\forall (x0: A0).(\forall (x1: A1).(\forall
312 (x2: A2).(\forall (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0
313 x1 x2 x3 x4) \to ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to
314 P)))))))))) \to ((ex4_5 A0 A1 A2 A3 A4 P0 P1 P2 P3) \to P)))))))))))
316 \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda
317 (A3: Type[0]).(\lambda (A4: Type[0]).(\lambda (P0: ((A0 \to (A1 \to (A2 \to
318 (A3 \to (A4 \to Prop))))))).(\lambda (P1: ((A0 \to (A1 \to (A2 \to (A3 \to
319 (A4 \to Prop))))))).(\lambda (P2: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to
320 Prop))))))).(\lambda (P3: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to
321 Prop))))))).(\lambda (P: Prop).(\lambda (f: ((\forall (x0: A0).(\forall (x1:
322 A1).(\forall (x2: A2).(\forall (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3
323 x4) \to ((P1 x0 x1 x2 x3 x4) \to ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3
324 x4) \to P))))))))))).(\lambda (e: (ex4_5 A0 A1 A2 A3 A4 P0 P1 P2 P3)).(match
325 e with [(ex4_5_intro x x0 x1 x2 x3 x4 x5 x6 x7) \Rightarrow (f x x0 x1 x2 x3
326 x4 x5 x6 x7)])))))))))))).
329 \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall
330 (A3: Type[0]).(\forall (A4: Type[0]).(\forall (P0: ((A0 \to (A1 \to (A2 \to
331 (A3 \to (A4 \to Prop))))))).(\forall (P1: ((A0 \to (A1 \to (A2 \to (A3 \to
332 (A4 \to Prop))))))).(\forall (P2: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to
333 Prop))))))).(\forall (P3: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to
334 Prop))))))).(\forall (P4: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to
335 Prop))))))).(\forall (P: Prop).(((\forall (x0: A0).(\forall (x1: A1).(\forall
336 (x2: A2).(\forall (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0
337 x1 x2 x3 x4) \to ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to ((P4 x0 x1
338 x2 x3 x4) \to P))))))))))) \to ((ex5_5 A0 A1 A2 A3 A4 P0 P1 P2 P3 P4) \to
341 \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda
342 (A3: Type[0]).(\lambda (A4: Type[0]).(\lambda (P0: ((A0 \to (A1 \to (A2 \to
343 (A3 \to (A4 \to Prop))))))).(\lambda (P1: ((A0 \to (A1 \to (A2 \to (A3 \to
344 (A4 \to Prop))))))).(\lambda (P2: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to
345 Prop))))))).(\lambda (P3: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to
346 Prop))))))).(\lambda (P4: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to
347 Prop))))))).(\lambda (P: Prop).(\lambda (f: ((\forall (x0: A0).(\forall (x1:
348 A1).(\forall (x2: A2).(\forall (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3
349 x4) \to ((P1 x0 x1 x2 x3 x4) \to ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3
350 x4) \to ((P4 x0 x1 x2 x3 x4) \to P)))))))))))).(\lambda (e: (ex5_5 A0 A1 A2
351 A3 A4 P0 P1 P2 P3 P4)).(match e with [(ex5_5_intro x x0 x1 x2 x3 x4 x5 x6 x7
352 x8) \Rightarrow (f x x0 x1 x2 x3 x4 x5 x6 x7 x8)]))))))))))))).
355 \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall
356 (A3: Type[0]).(\forall (A4: Type[0]).(\forall (A5: Type[0]).(\forall (P0:
357 ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\forall (P1:
358 ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\forall (P2:
359 ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\forall (P3:
360 ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\forall (P4:
361 ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\forall (P5:
362 ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\forall (P:
363 Prop).(((\forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3:
364 A3).(\forall (x4: A4).(\forall (x5: A5).((P0 x0 x1 x2 x3 x4 x5) \to ((P1 x0
365 x1 x2 x3 x4 x5) \to ((P2 x0 x1 x2 x3 x4 x5) \to ((P3 x0 x1 x2 x3 x4 x5) \to
366 ((P4 x0 x1 x2 x3 x4 x5) \to ((P5 x0 x1 x2 x3 x4 x5) \to P))))))))))))) \to
367 ((ex6_6 A0 A1 A2 A3 A4 A5 P0 P1 P2 P3 P4 P5) \to P))))))))))))))
369 \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda
370 (A3: Type[0]).(\lambda (A4: Type[0]).(\lambda (A5: Type[0]).(\lambda (P0:
371 ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\lambda (P1:
372 ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\lambda (P2:
373 ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\lambda (P3:
374 ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\lambda (P4:
375 ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\lambda (P5:
376 ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))))).(\lambda (P:
377 Prop).(\lambda (f: ((\forall (x0: A0).(\forall (x1: A1).(\forall (x2:
378 A2).(\forall (x3: A3).(\forall (x4: A4).(\forall (x5: A5).((P0 x0 x1 x2 x3 x4
379 x5) \to ((P1 x0 x1 x2 x3 x4 x5) \to ((P2 x0 x1 x2 x3 x4 x5) \to ((P3 x0 x1 x2
380 x3 x4 x5) \to ((P4 x0 x1 x2 x3 x4 x5) \to ((P5 x0 x1 x2 x3 x4 x5) \to
381 P)))))))))))))).(\lambda (e: (ex6_6 A0 A1 A2 A3 A4 A5 P0 P1 P2 P3 P4
382 P5)).(match e with [(ex6_6_intro x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
383 \Rightarrow (f x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)]))))))))))))))).
386 \forall (A0: Type[0]).(\forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall
387 (A3: Type[0]).(\forall (A4: Type[0]).(\forall (A5: Type[0]).(\forall (A6:
388 Type[0]).(\forall (P0: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6
389 \to Prop))))))))).(\forall (P1: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5
390 \to (A6 \to Prop))))))))).(\forall (P2: ((A0 \to (A1 \to (A2 \to (A3 \to (A4
391 \to (A5 \to (A6 \to Prop))))))))).(\forall (P3: ((A0 \to (A1 \to (A2 \to (A3
392 \to (A4 \to (A5 \to (A6 \to Prop))))))))).(\forall (P4: ((A0 \to (A1 \to (A2
393 \to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))))).(\forall (P5: ((A0 \to (A1
394 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))))).(\forall (P:
395 Prop).(((\forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3:
396 A3).(\forall (x4: A4).(\forall (x5: A5).(\forall (x6: A6).((P0 x0 x1 x2 x3 x4
397 x5 x6) \to ((P1 x0 x1 x2 x3 x4 x5 x6) \to ((P2 x0 x1 x2 x3 x4 x5 x6) \to ((P3
398 x0 x1 x2 x3 x4 x5 x6) \to ((P4 x0 x1 x2 x3 x4 x5 x6) \to ((P5 x0 x1 x2 x3 x4
399 x5 x6) \to P)))))))))))))) \to ((ex6_7 A0 A1 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4
400 P5) \to P)))))))))))))))
402 \lambda (A0: Type[0]).(\lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda
403 (A3: Type[0]).(\lambda (A4: Type[0]).(\lambda (A5: Type[0]).(\lambda (A6:
404 Type[0]).(\lambda (P0: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6
405 \to Prop))))))))).(\lambda (P1: ((A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5
406 \to (A6 \to Prop))))))))).(\lambda (P2: ((A0 \to (A1 \to (A2 \to (A3 \to (A4
407 \to (A5 \to (A6 \to Prop))))))))).(\lambda (P3: ((A0 \to (A1 \to (A2 \to (A3
408 \to (A4 \to (A5 \to (A6 \to Prop))))))))).(\lambda (P4: ((A0 \to (A1 \to (A2
409 \to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))))).(\lambda (P5: ((A0 \to (A1
410 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))))).(\lambda (P:
411 Prop).(\lambda (f: ((\forall (x0: A0).(\forall (x1: A1).(\forall (x2:
412 A2).(\forall (x3: A3).(\forall (x4: A4).(\forall (x5: A5).(\forall (x6:
413 A6).((P0 x0 x1 x2 x3 x4 x5 x6) \to ((P1 x0 x1 x2 x3 x4 x5 x6) \to ((P2 x0 x1
414 x2 x3 x4 x5 x6) \to ((P3 x0 x1 x2 x3 x4 x5 x6) \to ((P4 x0 x1 x2 x3 x4 x5 x6)
415 \to ((P5 x0 x1 x2 x3 x4 x5 x6) \to P))))))))))))))).(\lambda (e: (ex6_7 A0 A1
416 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4 P5)).(match e with [(ex6_7_intro x x0 x1 x2 x3
417 x4 x5 x6 x7 x8 x9 x10 x11) \Rightarrow (f x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10
418 x11)])))))))))))))))).