-
Notifications
You must be signed in to change notification settings - Fork 1
/
terms.v
555 lines (555 loc) · 115 KB
/
terms.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
Require Import HOLLight_Real.HOLLight_Real HOLLight Rdefinitions Rbasic_fun Raxioms.
Require Import HOLLight.theory_hol.
Definition _FALSITY_ : Prop := False.
Lemma _FALSITY__def : _FALSITY_ = False.
Proof. exact (eq_refl _FALSITY_). Qed.
Lemma COND_def {A : Type'} : (@COND A) = (fun t : Prop => fun t1 : A => fun t2 : A => @ε A (fun x : A => ((t = True) -> x = t1) /\ ((t = False) -> x = t2))).
Proof. exact (eq_refl (@COND A)). Qed.
Definition o {A B C : Type'} : (B -> C) -> (A -> B) -> A -> C := fun f : B -> C => fun g : A -> B => fun x : A => f (g x).
Lemma o_def {A B C : Type'} : (@o A B C) = (fun f : B -> C => fun g : A -> B => fun x : A => f (g x)).
Proof. exact (eq_refl (@o A B C)). Qed.
Definition I {A : Type'} : A -> A := fun x : A => x.
Lemma I_def {A : Type'} : (@I A) = (fun x : A => x).
Proof. exact (eq_refl (@I A)). Qed.
Definition hashek : Prop := True.
Lemma hashek_def : hashek = True.
Proof. exact (eq_refl hashek). Qed.
Definition LET {A B : Type'} : (A -> B) -> A -> B := fun f : A -> B => fun x : A => f x.
Lemma LET_def {A B : Type'} : (@LET A B) = (fun f : A -> B => fun x : A => f x).
Proof. exact (eq_refl (@LET A B)). Qed.
Definition LET_END {A : Type'} : A -> A := fun t : A => t.
Lemma LET_END_def {A : Type'} : (@LET_END A) = (fun t : A => t).
Proof. exact (eq_refl (@LET_END A)). Qed.
Definition GABS {A : Type'} : (A -> Prop) -> A := fun P : A -> Prop => @ε A P.
Lemma GABS_def {A : Type'} : (@GABS A) = (fun P : A -> Prop => @ε A P).
Proof. exact (eq_refl (@GABS A)). Qed.
Definition GEQ {A : Type'} : A -> A -> Prop := fun a : A => fun b : A => a = b.
Lemma GEQ_def {A : Type'} : (@GEQ A) = (fun a : A => fun b : A => a = b).
Proof. exact (eq_refl (@GEQ A)). Qed.
Definition _SEQPATTERN {A B : Type'} : (A -> B -> Prop) -> (A -> B -> Prop) -> A -> B -> Prop := fun r : A -> B -> Prop => fun s : A -> B -> Prop => fun x : A => @COND (B -> Prop) (exists y : B, r x y) (r x) (s x).
Lemma _SEQPATTERN_def {A B : Type'} : (@_SEQPATTERN A B) = (fun r : A -> B -> Prop => fun s : A -> B -> Prop => fun x : A => @COND (B -> Prop) (exists y : B, r x y) (r x) (s x)).
Proof. exact (eq_refl (@_SEQPATTERN A B)). Qed.
Definition _UNGUARDED_PATTERN : Prop -> Prop -> Prop := fun p : Prop => fun r : Prop => p /\ r.
Lemma _UNGUARDED_PATTERN_def : _UNGUARDED_PATTERN = (fun p : Prop => fun r : Prop => p /\ r).
Proof. exact (eq_refl _UNGUARDED_PATTERN). Qed.
Definition _GUARDED_PATTERN : Prop -> Prop -> Prop -> Prop := fun p : Prop => fun g : Prop => fun r : Prop => p /\ (g /\ r).
Lemma _GUARDED_PATTERN_def : _GUARDED_PATTERN = (fun p : Prop => fun g : Prop => fun r : Prop => p /\ (g /\ r)).
Proof. exact (eq_refl _GUARDED_PATTERN). Qed.
Definition _MATCH {A B : Type'} : A -> (A -> B -> Prop) -> B := fun e : A => fun r : A -> B -> Prop => @COND B (@ex1 B (r e)) (@ε B (r e)) (@ε B (fun z : B => False)).
Lemma _MATCH_def {A B : Type'} : (@_MATCH A B) = (fun e : A => fun r : A -> B -> Prop => @COND B (@ex1 B (r e)) (@ε B (r e)) (@ε B (fun z : B => False))).
Proof. exact (eq_refl (@_MATCH A B)). Qed.
Definition _FUNCTION {A B : Type'} : (A -> B -> Prop) -> A -> B := fun r : A -> B -> Prop => fun x : A => @COND B (@ex1 B (r x)) (@ε B (r x)) (@ε B (fun z : B => False)).
Lemma _FUNCTION_def {A B : Type'} : (@_FUNCTION A B) = (fun r : A -> B -> Prop => fun x : A => @COND B (@ex1 B (r x)) (@ε B (r x)) (@ε B (fun z : B => False))).
Proof. exact (eq_refl (@_FUNCTION A B)). Qed.
Lemma mk_pair_def {A B : Type'} : (@mk_pair A B) = (fun x : A => fun y : B => fun a : A => fun b : B => (a = x) /\ (b = y)).
Proof. exact (eq_refl (@mk_pair A B)). Qed.
Definition CURRY {A B C : Type'} : ((prod A B) -> C) -> A -> B -> C := fun _1283 : (prod A B) -> C => fun _1284 : A => fun _1285 : B => _1283 (@pair A B _1284 _1285).
Lemma CURRY_def {A B C : Type'} : (@CURRY A B C) = (fun _1283 : (prod A B) -> C => fun _1284 : A => fun _1285 : B => _1283 (@pair A B _1284 _1285)).
Proof. exact (eq_refl (@CURRY A B C)). Qed.
Definition UNCURRY {A B C : Type'} : (A -> B -> C) -> (prod A B) -> C := fun _1304 : A -> B -> C => fun _1305 : prod A B => _1304 (@fst A B _1305) (@snd A B _1305).
Lemma UNCURRY_def {A B C : Type'} : (@UNCURRY A B C) = (fun _1304 : A -> B -> C => fun _1305 : prod A B => _1304 (@fst A B _1305) (@snd A B _1305)).
Proof. exact (eq_refl (@UNCURRY A B C)). Qed.
Definition PASSOC {A B C D : Type'} : ((prod (prod A B) C) -> D) -> (prod A (prod B C)) -> D := fun _1321 : (prod (prod A B) C) -> D => fun _1322 : prod A (prod B C) => _1321 (@pair (prod A B) C (@pair A B (@fst A (prod B C) _1322) (@fst B C (@snd A (prod B C) _1322))) (@snd B C (@snd A (prod B C) _1322))).
Lemma PASSOC_def {A B C D : Type'} : (@PASSOC A B C D) = (fun _1321 : (prod (prod A B) C) -> D => fun _1322 : prod A (prod B C) => _1321 (@pair (prod A B) C (@pair A B (@fst A (prod B C) _1322) (@fst B C (@snd A (prod B C) _1322))) (@snd B C (@snd A (prod B C) _1322)))).
Proof. exact (eq_refl (@PASSOC A B C D)). Qed.
Lemma ONE_ONE_def {A B : Type'} : (@ONE_ONE A B) = (fun _2064 : A -> B => forall x1 : A, forall x2 : A, ((_2064 x1) = (_2064 x2)) -> x1 = x2).
Proof. exact (eq_refl (@ONE_ONE A B)). Qed.
Lemma ONTO_def {A B : Type'} : (@ONTO A B) = (fun _2069 : A -> B => forall y : B, exists x : A, y = (_2069 x)).
Proof. exact (eq_refl (@ONTO A B)). Qed.
Lemma IND_SUC_def : IND_SUC = (@ε (ind -> ind) (fun f : ind -> ind => exists z : ind, (forall x1 : ind, forall x2 : ind, ((f x1) = (f x2)) = (x1 = x2)) /\ (forall x : ind, ~ ((f x) = z)))).
Proof. exact (eq_refl IND_SUC). Qed.
Lemma IND_0_def : IND_0 = (@ε ind (fun z : ind => (forall x1 : ind, forall x2 : ind, ((IND_SUC x1) = (IND_SUC x2)) = (x1 = x2)) /\ (forall x : ind, ~ ((IND_SUC x) = z)))).
Proof. exact (eq_refl IND_0). Qed.
Lemma NUM_REP_def : NUM_REP = (fun a : ind => forall NUM_REP' : ind -> Prop, (forall a' : ind, ((a' = IND_0) \/ (exists i : ind, (a' = (IND_SUC i)) /\ (NUM_REP' i))) -> NUM_REP' a') -> NUM_REP' a).
Proof. exact (eq_refl NUM_REP). Qed.
Definition NUMERAL : nat -> nat := fun _2128 : nat => _2128.
Lemma NUMERAL_def : NUMERAL = (fun _2128 : nat => _2128).
Proof. exact (eq_refl NUMERAL). Qed.
Lemma BIT1_def : BIT1 = (fun _2143 : nat => S (BIT0 _2143)).
Proof. exact (eq_refl BIT1). Qed.
Definition minimal : (nat -> Prop) -> nat := fun _6536 : nat -> Prop => @ε nat (fun n : nat => (_6536 n) /\ (forall m : nat, (Peano.lt m n) -> ~ (_6536 m))).
Lemma minimal_def : minimal = (fun _6536 : nat -> Prop => @ε nat (fun n : nat => (_6536 n) /\ (forall m : nat, (Peano.lt m n) -> ~ (_6536 m)))).
Proof. exact (eq_refl minimal). Qed.
Definition WF {A : Type'} : (A -> A -> Prop) -> Prop := fun _6923 : A -> A -> Prop => forall P : A -> Prop, (exists x : A, P x) -> exists x : A, (P x) /\ (forall y : A, (_6923 y x) -> ~ (P y)).
Lemma WF_def {A : Type'} : (@WF A) = (fun _6923 : A -> A -> Prop => forall P : A -> Prop, (exists x : A, P x) -> exists x : A, (P x) /\ (forall y : A, (_6923 y x) -> ~ (P y))).
Proof. exact (eq_refl (@WF A)). Qed.
Definition MEASURE {A : Type'} : (A -> nat) -> A -> A -> Prop := fun _8094 : A -> nat => fun x : A => fun y : A => Peano.lt (_8094 x) (_8094 y).
Lemma MEASURE_def {A : Type'} : (@MEASURE A) = (fun _8094 : A -> nat => fun x : A => fun y : A => Peano.lt (_8094 x) (_8094 y)).
Proof. exact (eq_refl (@MEASURE A)). Qed.
Definition NUMPAIR : nat -> nat -> nat := fun _17487 : nat => fun _17488 : nat => Nat.mul (Nat.pow (NUMERAL (BIT0 (BIT1 0))) _17487) (Nat.add (Nat.mul (NUMERAL (BIT0 (BIT1 0))) _17488) (NUMERAL (BIT1 0))).
Lemma NUMPAIR_def : NUMPAIR = (fun _17487 : nat => fun _17488 : nat => Nat.mul (Nat.pow (NUMERAL (BIT0 (BIT1 0))) _17487) (Nat.add (Nat.mul (NUMERAL (BIT0 (BIT1 0))) _17488) (NUMERAL (BIT1 0)))).
Proof. exact (eq_refl NUMPAIR). Qed.
Definition NUMFST : nat -> nat := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> nat -> nat) (fun X : (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> nat -> nat => forall _17503 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), exists Y : nat -> nat, forall x : nat, forall y : nat, ((X _17503 (NUMPAIR x y)) = x) /\ ((Y (NUMPAIR x y)) = y)) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0))))))))))))).
Lemma NUMFST_def : NUMFST = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> nat -> nat) (fun X : (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> nat -> nat => forall _17503 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), exists Y : nat -> nat, forall x : nat, forall y : nat, ((X _17503 (NUMPAIR x y)) = x) /\ ((Y (NUMPAIR x y)) = y)) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))))))))).
Proof. exact (eq_refl NUMFST). Qed.
Definition NUMSND : nat -> nat := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> nat -> nat) (fun Y : (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> nat -> nat => forall _17504 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), forall x : nat, forall y : nat, ((NUMFST (NUMPAIR x y)) = x) /\ ((Y _17504 (NUMPAIR x y)) = y)) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0))))))))))))).
Lemma NUMSND_def : NUMSND = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> nat -> nat) (fun Y : (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> nat -> nat => forall _17504 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), forall x : nat, forall y : nat, ((NUMFST (NUMPAIR x y)) = x) /\ ((Y _17504 (NUMPAIR x y)) = y)) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))))))))).
Proof. exact (eq_refl NUMSND). Qed.
Definition NUMSUM : Prop -> nat -> nat := fun _17505 : Prop => fun _17506 : nat => @COND nat _17505 (S (Nat.mul (NUMERAL (BIT0 (BIT1 0))) _17506)) (Nat.mul (NUMERAL (BIT0 (BIT1 0))) _17506).
Lemma NUMSUM_def : NUMSUM = (fun _17505 : Prop => fun _17506 : nat => @COND nat _17505 (S (Nat.mul (NUMERAL (BIT0 (BIT1 0))) _17506)) (Nat.mul (NUMERAL (BIT0 (BIT1 0))) _17506)).
Proof. exact (eq_refl NUMSUM). Qed.
Definition INJN {A : Type'} : nat -> nat -> A -> Prop := fun _17537 : nat => fun n : nat => fun a : A => n = _17537.
Lemma INJN_def {A : Type'} : (@INJN A) = (fun _17537 : nat => fun n : nat => fun a : A => n = _17537).
Proof. exact (eq_refl (@INJN A)). Qed.
Definition INJA {A : Type'} : A -> nat -> A -> Prop := fun _17542 : A => fun n : nat => fun b : A => b = _17542.
Lemma INJA_def {A : Type'} : (@INJA A) = (fun _17542 : A => fun n : nat => fun b : A => b = _17542).
Proof. exact (eq_refl (@INJA A)). Qed.
Definition INJF {A : Type'} : (nat -> nat -> A -> Prop) -> nat -> A -> Prop := fun _17549 : nat -> nat -> A -> Prop => fun n : nat => _17549 (NUMFST n) (NUMSND n).
Lemma INJF_def {A : Type'} : (@INJF A) = (fun _17549 : nat -> nat -> A -> Prop => fun n : nat => _17549 (NUMFST n) (NUMSND n)).
Proof. exact (eq_refl (@INJF A)). Qed.
Definition INJP {A : Type'} : (nat -> A -> Prop) -> (nat -> A -> Prop) -> nat -> A -> Prop := fun _17554 : nat -> A -> Prop => fun _17555 : nat -> A -> Prop => fun n : nat => fun a : A => @COND Prop (NUMLEFT n) (_17554 (NUMRIGHT n) a) (_17555 (NUMRIGHT n) a).
Lemma INJP_def {A : Type'} : (@INJP A) = (fun _17554 : nat -> A -> Prop => fun _17555 : nat -> A -> Prop => fun n : nat => fun a : A => @COND Prop (NUMLEFT n) (_17554 (NUMRIGHT n) a) (_17555 (NUMRIGHT n) a)).
Proof. exact (eq_refl (@INJP A)). Qed.
Definition ZCONSTR {A : Type'} : nat -> A -> (nat -> nat -> A -> Prop) -> nat -> A -> Prop := fun _17566 : nat => fun _17567 : A => fun _17568 : nat -> nat -> A -> Prop => @INJP A (@INJN A (S _17566)) (@INJP A (@INJA A _17567) (@INJF A _17568)).
Lemma ZCONSTR_def {A : Type'} : (@ZCONSTR A) = (fun _17566 : nat => fun _17567 : A => fun _17568 : nat -> nat -> A -> Prop => @INJP A (@INJN A (S _17566)) (@INJP A (@INJA A _17567) (@INJF A _17568))).
Proof. exact (eq_refl (@ZCONSTR A)). Qed.
Definition ZBOT {A : Type'} : nat -> A -> Prop := @INJP A (@INJN A (NUMERAL 0)) (@ε (nat -> A -> Prop) (fun z : nat -> A -> Prop => True)).
Lemma ZBOT_def {A : Type'} : (@ZBOT A) = (@INJP A (@INJN A (NUMERAL 0)) (@ε (nat -> A -> Prop) (fun z : nat -> A -> Prop => True))).
Proof. exact (eq_refl (@ZBOT A)). Qed.
Definition BOTTOM {A : Type'} : recspace A := @_mk_rec A (@ZBOT A).
Lemma BOTTOM_def {A : Type'} : (@BOTTOM A) = (@_mk_rec A (@ZBOT A)).
Proof. exact (eq_refl (@BOTTOM A)). Qed.
Definition CONSTR {A : Type'} : nat -> A -> (nat -> recspace A) -> recspace A := fun _17591 : nat => fun _17592 : A => fun _17593 : nat -> recspace A => @_mk_rec A (@ZCONSTR A _17591 _17592 (fun n : nat => @_dest_rec A (_17593 n))).
Lemma CONSTR_def {A : Type'} : (@CONSTR A) = (fun _17591 : nat => fun _17592 : A => fun _17593 : nat -> recspace A => @_mk_rec A (@ZCONSTR A _17591 _17592 (fun n : nat => @_dest_rec A (_17593 n)))).
Proof. exact (eq_refl (@CONSTR A)). Qed.
Definition FNIL {A : Type'} : nat -> A := fun _17624 : nat => @ε A (fun x : A => True).
Lemma FNIL_def {A : Type'} : (@FNIL A) = (fun _17624 : nat => @ε A (fun x : A => True)).
Proof. exact (eq_refl (@FNIL A)). Qed.
Definition OUTL {A B : Type'} : (Datatypes.sum A B) -> A := @ε ((prod nat (prod nat (prod nat nat))) -> (Datatypes.sum A B) -> A) (fun OUTL' : (prod nat (prod nat (prod nat nat))) -> (Datatypes.sum A B) -> A => forall _17649 : prod nat (prod nat (prod nat nat)), forall x : A, (OUTL' _17649 (@inl A B x)) = x) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0))))))))))).
Lemma OUTL_def {A B : Type'} : (@OUTL A B) = (@ε ((prod nat (prod nat (prod nat nat))) -> (Datatypes.sum A B) -> A) (fun OUTL' : (prod nat (prod nat (prod nat nat))) -> (Datatypes.sum A B) -> A => forall _17649 : prod nat (prod nat (prod nat nat)), forall x : A, (OUTL' _17649 (@inl A B x)) = x) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))))))).
Proof. exact (eq_refl (@OUTL A B)). Qed.
Definition OUTR {A B : Type'} : (Datatypes.sum A B) -> B := @ε ((prod nat (prod nat (prod nat nat))) -> (Datatypes.sum A B) -> B) (fun OUTR' : (prod nat (prod nat (prod nat nat))) -> (Datatypes.sum A B) -> B => forall _17651 : prod nat (prod nat (prod nat nat)), forall y : B, (OUTR' _17651 (@inr A B y)) = y) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0))))))))))).
Lemma OUTR_def {A B : Type'} : (@OUTR A B) = (@ε ((prod nat (prod nat (prod nat nat))) -> (Datatypes.sum A B) -> B) (fun OUTR' : (prod nat (prod nat (prod nat nat))) -> (Datatypes.sum A B) -> B => forall _17651 : prod nat (prod nat (prod nat nat)), forall y : B, (OUTR' _17651 (@inr A B y)) = y) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))))))).
Proof. exact (eq_refl (@OUTR A B)). Qed.
Definition LAST {A : Type'} : (list A) -> A := @ε ((prod nat (prod nat (prod nat nat))) -> (list A) -> A) (fun LAST' : (prod nat (prod nat (prod nat nat))) -> (list A) -> A => forall _18117 : prod nat (prod nat (prod nat nat)), forall h : A, forall t : list A, (LAST' _18117 (@cons A h t)) = (@COND A (t = (@nil A)) h (LAST' _18117 t))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0))))))))))).
Lemma LAST_def {A : Type'} : (@LAST A) = (@ε ((prod nat (prod nat (prod nat nat))) -> (list A) -> A) (fun LAST' : (prod nat (prod nat (prod nat nat))) -> (list A) -> A => forall _18117 : prod nat (prod nat (prod nat nat)), forall h : A, forall t : list A, (LAST' _18117 (@cons A h t)) = (@COND A (t = (@nil A)) h (LAST' _18117 t))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))))))).
Proof. exact (eq_refl (@LAST A)). Qed.
Definition NULL {A : Type'} : (list A) -> Prop := @ε ((prod nat (prod nat (prod nat nat))) -> (list A) -> Prop) (fun NULL' : (prod nat (prod nat (prod nat nat))) -> (list A) -> Prop => forall _18129 : prod nat (prod nat (prod nat nat)), ((NULL' _18129 (@nil A)) = True) /\ (forall h : A, forall t : list A, (NULL' _18129 (@cons A h t)) = False)) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0))))))))))).
Lemma NULL_def {A : Type'} : (@NULL A) = (@ε ((prod nat (prod nat (prod nat nat))) -> (list A) -> Prop) (fun NULL' : (prod nat (prod nat (prod nat nat))) -> (list A) -> Prop => forall _18129 : prod nat (prod nat (prod nat nat)), ((NULL' _18129 (@nil A)) = True) /\ (forall h : A, forall t : list A, (NULL' _18129 (@cons A h t)) = False)) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))))))).
Proof. exact (eq_refl (@NULL A)). Qed.
Definition EX {A : Type'} : (A -> Prop) -> (list A) -> Prop := @ε ((prod nat nat) -> (A -> Prop) -> (list A) -> Prop) (fun EX' : (prod nat nat) -> (A -> Prop) -> (list A) -> Prop => forall _18143 : prod nat nat, (forall P : A -> Prop, (EX' _18143 P (@nil A)) = False) /\ (forall h : A, forall P : A -> Prop, forall t : list A, (EX' _18143 P (@cons A h t)) = ((P h) \/ (EX' _18143 P t)))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT1 0))))))))).
Lemma EX_def {A : Type'} : (@EX A) = (@ε ((prod nat nat) -> (A -> Prop) -> (list A) -> Prop) (fun EX' : (prod nat nat) -> (A -> Prop) -> (list A) -> Prop => forall _18143 : prod nat nat, (forall P : A -> Prop, (EX' _18143 P (@nil A)) = False) /\ (forall h : A, forall P : A -> Prop, forall t : list A, (EX' _18143 P (@cons A h t)) = ((P h) \/ (EX' _18143 P t)))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT1 0)))))))))).
Proof. exact (eq_refl (@EX A)). Qed.
Definition ITLIST {A B : Type'} : (A -> B -> B) -> (list A) -> B -> B := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (A -> B -> B) -> (list A) -> B -> B) (fun ITLIST' : (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (A -> B -> B) -> (list A) -> B -> B => forall _18151 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), (forall f : A -> B -> B, forall b : B, (ITLIST' _18151 f (@nil A) b) = b) /\ (forall h : A, forall f : A -> B -> B, forall t : list A, forall b : B, (ITLIST' _18151 f (@cons A h t) b) = (f h (ITLIST' _18151 f t b)))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0))))))))))))).
Lemma ITLIST_def {A B : Type'} : (@ITLIST A B) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (A -> B -> B) -> (list A) -> B -> B) (fun ITLIST' : (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (A -> B -> B) -> (list A) -> B -> B => forall _18151 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), (forall f : A -> B -> B, forall b : B, (ITLIST' _18151 f (@nil A) b) = b) /\ (forall h : A, forall f : A -> B -> B, forall t : list A, forall b : B, (ITLIST' _18151 f (@cons A h t) b) = (f h (ITLIST' _18151 f t b)))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))))))))).
Proof. exact (eq_refl (@ITLIST A B)). Qed.
Definition ALL2 {A B : Type'} : (A -> B -> Prop) -> (list A) -> (list B) -> Prop := @ε ((prod nat (prod nat (prod nat nat))) -> (A -> B -> Prop) -> (list A) -> (list B) -> Prop) (fun ALL2' : (prod nat (prod nat (prod nat nat))) -> (A -> B -> Prop) -> (list A) -> (list B) -> Prop => forall _18166 : prod nat (prod nat (prod nat nat)), (forall P : A -> B -> Prop, forall l2 : list B, (ALL2' _18166 P (@nil A) l2) = (l2 = (@nil B))) /\ (forall h1' : A, forall P : A -> B -> Prop, forall t1 : list A, forall l2 : list B, (ALL2' _18166 P (@cons A h1' t1) l2) = (@COND Prop (l2 = (@nil B)) False ((P h1' (@hd B l2)) /\ (ALL2' _18166 P t1 (@tl B l2)))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))))).
Lemma ALL2_def {A B : Type'} : (@ALL2 A B) = (@ε ((prod nat (prod nat (prod nat nat))) -> (A -> B -> Prop) -> (list A) -> (list B) -> Prop) (fun ALL2' : (prod nat (prod nat (prod nat nat))) -> (A -> B -> Prop) -> (list A) -> (list B) -> Prop => forall _18166 : prod nat (prod nat (prod nat nat)), (forall P : A -> B -> Prop, forall l2 : list B, (ALL2' _18166 P (@nil A) l2) = (l2 = (@nil B))) /\ (forall h1' : A, forall P : A -> B -> Prop, forall t1 : list A, forall l2 : list B, (ALL2' _18166 P (@cons A h1' t1) l2) = (@COND Prop (l2 = (@nil B)) False ((P h1' (@hd B l2)) /\ (ALL2' _18166 P t1 (@tl B l2)))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0))))))))))).
Proof. exact (eq_refl (@ALL2 A B)). Qed.
Definition MAP2 {A B C : Type'} : (A -> B -> C) -> (list A) -> (list B) -> list C := @ε ((prod nat (prod nat (prod nat nat))) -> (A -> B -> C) -> (list A) -> (list B) -> list C) (fun MAP2' : (prod nat (prod nat (prod nat nat))) -> (A -> B -> C) -> (list A) -> (list B) -> list C => forall _18174 : prod nat (prod nat (prod nat nat)), (forall f : A -> B -> C, forall l : list B, (MAP2' _18174 f (@nil A) l) = (@nil C)) /\ (forall h1' : A, forall f : A -> B -> C, forall t1 : list A, forall l : list B, (MAP2' _18174 f (@cons A h1' t1) l) = (@cons C (f h1' (@hd B l)) (MAP2' _18174 f t1 (@tl B l))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))))).
Lemma MAP2_def {A B C : Type'} : (@MAP2 A B C) = (@ε ((prod nat (prod nat (prod nat nat))) -> (A -> B -> C) -> (list A) -> (list B) -> list C) (fun MAP2' : (prod nat (prod nat (prod nat nat))) -> (A -> B -> C) -> (list A) -> (list B) -> list C => forall _18174 : prod nat (prod nat (prod nat nat)), (forall f : A -> B -> C, forall l : list B, (MAP2' _18174 f (@nil A) l) = (@nil C)) /\ (forall h1' : A, forall f : A -> B -> C, forall t1 : list A, forall l : list B, (MAP2' _18174 f (@cons A h1' t1) l) = (@cons C (f h1' (@hd B l)) (MAP2' _18174 f t1 (@tl B l))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0))))))))))).
Proof. exact (eq_refl (@MAP2 A B C)). Qed.
Definition EL {A : Type'} : nat -> (list A) -> A := @ε ((prod nat nat) -> nat -> (list A) -> A) (fun EL' : (prod nat nat) -> nat -> (list A) -> A => forall _18178 : prod nat nat, (forall l : list A, (EL' _18178 (NUMERAL 0) l) = (@hd A l)) /\ (forall n : nat, forall l : list A, (EL' _18178 (S n) l) = (EL' _18178 n (@tl A l)))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0))))))))).
Lemma EL_def {A : Type'} : (@EL A) = (@ε ((prod nat nat) -> nat -> (list A) -> A) (fun EL' : (prod nat nat) -> nat -> (list A) -> A => forall _18178 : prod nat nat, (forall l : list A, (EL' _18178 (NUMERAL 0) l) = (@hd A l)) /\ (forall n : nat, forall l : list A, (EL' _18178 (S n) l) = (EL' _18178 n (@tl A l)))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))))).
Proof. exact (eq_refl (@EL A)). Qed.
Definition FILTER {A : Type'} : (A -> Prop) -> (list A) -> list A := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (A -> Prop) -> (list A) -> list A) (fun FILTER' : (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (A -> Prop) -> (list A) -> list A => forall _18185 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), (forall P : A -> Prop, (FILTER' _18185 P (@nil A)) = (@nil A)) /\ (forall h : A, forall P : A -> Prop, forall t : list A, (FILTER' _18185 P (@cons A h t)) = (@COND (list A) (P h) (@cons A h (FILTER' _18185 P t)) (FILTER' _18185 P t)))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0))))))))))))).
Lemma FILTER_def {A : Type'} : (@FILTER A) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (A -> Prop) -> (list A) -> list A) (fun FILTER' : (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (A -> Prop) -> (list A) -> list A => forall _18185 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), (forall P : A -> Prop, (FILTER' _18185 P (@nil A)) = (@nil A)) /\ (forall h : A, forall P : A -> Prop, forall t : list A, (FILTER' _18185 P (@cons A h t)) = (@COND (list A) (P h) (@cons A h (FILTER' _18185 P t)) (FILTER' _18185 P t)))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))))))))).
Proof. exact (eq_refl (@FILTER A)). Qed.
Definition ASSOC {A B : Type'} : A -> (list (prod A B)) -> B := @ε ((prod nat (prod nat (prod nat (prod nat nat)))) -> A -> (list (prod A B)) -> B) (fun ASSOC' : (prod nat (prod nat (prod nat (prod nat nat)))) -> A -> (list (prod A B)) -> B => forall _18192 : prod nat (prod nat (prod nat (prod nat nat))), forall h : prod A B, forall a : A, forall t : list (prod A B), (ASSOC' _18192 a (@cons (prod A B) h t)) = (@COND B ((@fst A B h) = a) (@snd A B h) (ASSOC' _18192 a t))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))))))).
Lemma ASSOC_def {A B : Type'} : (@ASSOC A B) = (@ε ((prod nat (prod nat (prod nat (prod nat nat)))) -> A -> (list (prod A B)) -> B) (fun ASSOC' : (prod nat (prod nat (prod nat (prod nat nat)))) -> A -> (list (prod A B)) -> B => forall _18192 : prod nat (prod nat (prod nat (prod nat nat))), forall h : prod A B, forall a : A, forall t : list (prod A B), (ASSOC' _18192 a (@cons (prod A B) h t)) = (@COND B ((@fst A B h) = a) (@snd A B h) (ASSOC' _18192 a t))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0))))))))))))).
Proof. exact (eq_refl (@ASSOC A B)). Qed.
Definition ITLIST2 {A B C : Type'} : (A -> B -> C -> C) -> (list A) -> (list B) -> C -> C := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (A -> B -> C -> C) -> (list A) -> (list B) -> C -> C) (fun ITLIST2' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (A -> B -> C -> C) -> (list A) -> (list B) -> C -> C => forall _18201 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))), (forall f : A -> B -> C -> C, forall l2 : list B, forall b : C, (ITLIST2' _18201 f (@nil A) l2 b) = b) /\ (forall h1' : A, forall f : A -> B -> C -> C, forall t1 : list A, forall l2 : list B, forall b : C, (ITLIST2' _18201 f (@cons A h1' t1) l2 b) = (f h1' (@hd B l2) (ITLIST2' _18201 f t1 (@tl B l2) b)))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0))))))))))))).
Lemma ITLIST2_def {A B C : Type'} : (@ITLIST2 A B C) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (A -> B -> C -> C) -> (list A) -> (list B) -> C -> C) (fun ITLIST2' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (A -> B -> C -> C) -> (list A) -> (list B) -> C -> C => forall _18201 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))), (forall f : A -> B -> C -> C, forall l2 : list B, forall b : C, (ITLIST2' _18201 f (@nil A) l2 b) = b) /\ (forall h1' : A, forall f : A -> B -> C -> C, forall t1 : list A, forall l2 : list B, forall b : C, (ITLIST2' _18201 f (@cons A h1' t1) l2 b) = (f h1' (@hd B l2) (ITLIST2' _18201 f t1 (@tl B l2) b)))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))))))))).
Proof. exact (eq_refl (@ITLIST2 A B C)). Qed.
Definition ZIP {A B : Type'} : (list A) -> (list B) -> list (prod A B) := @ε ((prod nat (prod nat nat)) -> (list A) -> (list B) -> list (prod A B)) (fun ZIP' : (prod nat (prod nat nat)) -> (list A) -> (list B) -> list (prod A B) => forall _18205 : prod nat (prod nat nat), (forall l2 : list B, (ZIP' _18205 (@nil A) l2) = (@nil (prod A B))) /\ (forall h1' : A, forall t1 : list A, forall l2 : list B, (ZIP' _18205 (@cons A h1' t1) l2) = (@cons (prod A B) (@pair A B h1' (@hd B l2)) (ZIP' _18205 t1 (@tl B l2))))) (@pair nat (prod nat nat) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))))).
Lemma ZIP_def {A B : Type'} : (@ZIP A B) = (@ε ((prod nat (prod nat nat)) -> (list A) -> (list B) -> list (prod A B)) (fun ZIP' : (prod nat (prod nat nat)) -> (list A) -> (list B) -> list (prod A B) => forall _18205 : prod nat (prod nat nat), (forall l2 : list B, (ZIP' _18205 (@nil A) l2) = (@nil (prod A B))) /\ (forall h1' : A, forall t1 : list A, forall l2 : list B, (ZIP' _18205 (@cons A h1' t1) l2) = (@cons (prod A B) (@pair A B h1' (@hd B l2)) (ZIP' _18205 t1 (@tl B l2))))) (@pair nat (prod nat nat) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0))))))))))).
Proof. exact (eq_refl (@ZIP A B)). Qed.
Definition ALLPAIRS {A B : Type'} : (A -> B -> Prop) -> (list A) -> (list B) -> Prop := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> (A -> B -> Prop) -> (list A) -> (list B) -> Prop) (fun ALLPAIRS' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> (A -> B -> Prop) -> (list A) -> (list B) -> Prop => forall _18213 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))), (forall f : A -> B -> Prop, forall l : list B, (ALLPAIRS' _18213 f (@nil A) l) = True) /\ (forall h : A, forall f : A -> B -> Prop, forall t : list A, forall l : list B, (ALLPAIRS' _18213 f (@cons A h t) l) = ((@List.Forall B (f h) l) /\ (ALLPAIRS' _18213 f t l)))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0))))))))))))))).
Lemma ALLPAIRS_def {A B : Type'} : (@ALLPAIRS A B) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> (A -> B -> Prop) -> (list A) -> (list B) -> Prop) (fun ALLPAIRS' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> (A -> B -> Prop) -> (list A) -> (list B) -> Prop => forall _18213 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))), (forall f : A -> B -> Prop, forall l : list B, (ALLPAIRS' _18213 f (@nil A) l) = True) /\ (forall h : A, forall f : A -> B -> Prop, forall t : list A, forall l : list B, (ALLPAIRS' _18213 f (@cons A h t) l) = ((@List.Forall B (f h) l) /\ (ALLPAIRS' _18213 f t l)))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))))))))))).
Proof. exact (eq_refl (@ALLPAIRS A B)). Qed.
Definition list_of_seq {A : Type'} : (nat -> A) -> nat -> list A := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))))))) -> (nat -> A) -> nat -> list A) (fun list_of_seq' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))))))) -> (nat -> A) -> nat -> list A => forall _18227 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))))), (forall s : nat -> A, (list_of_seq' _18227 s (NUMERAL 0)) = (@nil A)) /\ (forall s : nat -> A, forall n : nat, (list_of_seq' _18227 s (S n)) = (@List.app A (list_of_seq' _18227 s n) (@cons A (s n) (@nil A))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))))))))))))).
Lemma list_of_seq_def {A : Type'} : (@list_of_seq A) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))))))) -> (nat -> A) -> nat -> list A) (fun list_of_seq' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))))))) -> (nat -> A) -> nat -> list A => forall _18227 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))))), (forall s : nat -> A, (list_of_seq' _18227 s (NUMERAL 0)) = (@nil A)) /\ (forall s : nat -> A, forall n : nat, (list_of_seq' _18227 s (S n)) = (@List.app A (list_of_seq' _18227 s n) (@cons A (s n) (@nil A))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 0))))))))))))))))))).
Proof. exact (eq_refl (@list_of_seq A)). Qed.
Definition _22857 : Prop -> Prop -> Prop -> Prop -> Prop -> Prop -> Prop -> Prop -> Ascii.ascii := fun a0 : Prop => fun a1 : Prop => fun a2 : Prop => fun a3 : Prop => fun a4 : Prop => fun a5 : Prop => fun a6 : Prop => fun a7 : Prop => _mk_char ((fun a0' : Prop => fun a1' : Prop => fun a2' : Prop => fun a3' : Prop => fun a4' : Prop => fun a5' : Prop => fun a6' : Prop => fun a7' : Prop => @CONSTR (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop Prop))))))) (NUMERAL 0) (@pair Prop (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop Prop)))))) a0' (@pair Prop (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop Prop))))) a1' (@pair Prop (prod Prop (prod Prop (prod Prop (prod Prop Prop)))) a2' (@pair Prop (prod Prop (prod Prop (prod Prop Prop))) a3' (@pair Prop (prod Prop (prod Prop Prop)) a4' (@pair Prop (prod Prop Prop) a5' (@pair Prop Prop a6' a7'))))))) (fun n : nat => @BOTTOM (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop Prop))))))))) a0 a1 a2 a3 a4 a5 a6 a7).
Lemma _22857_def : _22857 = (fun a0 : Prop => fun a1 : Prop => fun a2 : Prop => fun a3 : Prop => fun a4 : Prop => fun a5 : Prop => fun a6 : Prop => fun a7 : Prop => _mk_char ((fun a0' : Prop => fun a1' : Prop => fun a2' : Prop => fun a3' : Prop => fun a4' : Prop => fun a5' : Prop => fun a6' : Prop => fun a7' : Prop => @CONSTR (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop Prop))))))) (NUMERAL 0) (@pair Prop (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop Prop)))))) a0' (@pair Prop (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop Prop))))) a1' (@pair Prop (prod Prop (prod Prop (prod Prop (prod Prop Prop)))) a2' (@pair Prop (prod Prop (prod Prop (prod Prop Prop))) a3' (@pair Prop (prod Prop (prod Prop Prop)) a4' (@pair Prop (prod Prop Prop) a5' (@pair Prop Prop a6' a7'))))))) (fun n : nat => @BOTTOM (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop Prop))))))))) a0 a1 a2 a3 a4 a5 a6 a7)).
Proof. exact (eq_refl _22857). Qed.
Definition ASCII : Prop -> Prop -> Prop -> Prop -> Prop -> Prop -> Prop -> Prop -> Ascii.ascii := _22857.
Lemma ASCII_def : ASCII = _22857.
Proof. exact (eq_refl ASCII). Qed.
Lemma dist_def : dist = (fun _22947 : prod nat nat => Nat.add (Nat.sub (@fst nat nat _22947) (@snd nat nat _22947)) (Nat.sub (@snd nat nat _22947) (@fst nat nat _22947))).
Proof. exact (eq_refl dist). Qed.
Lemma is_nadd_def : is_nadd = (fun _23257 : nat -> nat => exists B : nat, forall m : nat, forall n : nat, Peano.le (dist (@pair nat nat (Nat.mul m (_23257 n)) (Nat.mul n (_23257 m)))) (Nat.mul B (Nat.add m n))).
Proof. exact (eq_refl is_nadd). Qed.
Lemma nadd_eq_def : nadd_eq = (fun _23276 : nadd => fun _23277 : nadd => exists B : nat, forall n : nat, Peano.le (dist (@pair nat nat (dest_nadd _23276 n) (dest_nadd _23277 n))) B).
Proof. exact (eq_refl nadd_eq). Qed.
Lemma nadd_of_num_def : nadd_of_num = (fun _23288 : nat => mk_nadd (fun n : nat => Nat.mul _23288 n)).
Proof. exact (eq_refl nadd_of_num). Qed.
Lemma nadd_le_def : nadd_le = (fun _23295 : nadd => fun _23296 : nadd => exists B : nat, forall n : nat, Peano.le (dest_nadd _23295 n) (Nat.add (dest_nadd _23296 n) B)).
Proof. exact (eq_refl nadd_le). Qed.
Lemma nadd_add_def : nadd_add = (fun _23311 : nadd => fun _23312 : nadd => mk_nadd (fun n : nat => Nat.add (dest_nadd _23311 n) (dest_nadd _23312 n))).
Proof. exact (eq_refl nadd_add). Qed.
Lemma nadd_mul_def : nadd_mul = (fun _23325 : nadd => fun _23326 : nadd => mk_nadd (fun n : nat => dest_nadd _23325 (dest_nadd _23326 n))).
Proof. exact (eq_refl nadd_mul). Qed.
Lemma nadd_rinv_def : nadd_rinv = (fun _23462 : nadd => fun n : nat => Nat.div (Nat.mul n n) (dest_nadd _23462 n)).
Proof. exact (eq_refl nadd_rinv). Qed.
Lemma nadd_inv_def : nadd_inv = (fun _23476 : nadd => @COND nadd (nadd_eq _23476 (nadd_of_num (NUMERAL 0))) (nadd_of_num (NUMERAL 0)) (mk_nadd (nadd_rinv _23476))).
Proof. exact (eq_refl nadd_inv). Qed.
Lemma hreal_of_num_def : hreal_of_num = (fun m : nat => mk_hreal (fun u : nadd => nadd_eq (nadd_of_num m) u)).
Proof. exact (eq_refl hreal_of_num). Qed.
Lemma hreal_add_def : hreal_add = (fun x : hreal => fun y : hreal => mk_hreal (fun u : nadd => exists x' : nadd, exists y' : nadd, (nadd_eq (nadd_add x' y') u) /\ ((dest_hreal x x') /\ (dest_hreal y y')))).
Proof. exact (eq_refl hreal_add). Qed.
Lemma hreal_mul_def : hreal_mul = (fun x : hreal => fun y : hreal => mk_hreal (fun u : nadd => exists x' : nadd, exists y' : nadd, (nadd_eq (nadd_mul x' y') u) /\ ((dest_hreal x x') /\ (dest_hreal y y')))).
Proof. exact (eq_refl hreal_mul). Qed.
Lemma hreal_le_def : hreal_le = (fun x : hreal => fun y : hreal => @ε Prop (fun u : Prop => exists x' : nadd, exists y' : nadd, ((nadd_le x' y') = u) /\ ((dest_hreal x x') /\ (dest_hreal y y')))).
Proof. exact (eq_refl hreal_le). Qed.
Lemma hreal_inv_def : hreal_inv = (fun x : hreal => mk_hreal (fun u : nadd => exists x' : nadd, (nadd_eq (nadd_inv x') u) /\ (dest_hreal x x'))).
Proof. exact (eq_refl hreal_inv). Qed.
Lemma treal_of_num_def : treal_of_num = (fun _23721 : nat => @pair hreal hreal (hreal_of_num _23721) (hreal_of_num (NUMERAL 0))).
Proof. exact (eq_refl treal_of_num). Qed.
Lemma treal_neg_def : treal_neg = (fun _23726 : prod hreal hreal => @pair hreal hreal (@snd hreal hreal _23726) (@fst hreal hreal _23726)).
Proof. exact (eq_refl treal_neg). Qed.
Lemma treal_add_def : treal_add = (fun _23735 : prod hreal hreal => fun _23736 : prod hreal hreal => @pair hreal hreal (hreal_add (@fst hreal hreal _23735) (@fst hreal hreal _23736)) (hreal_add (@snd hreal hreal _23735) (@snd hreal hreal _23736))).
Proof. exact (eq_refl treal_add). Qed.
Lemma treal_mul_def : treal_mul = (fun _23757 : prod hreal hreal => fun _23758 : prod hreal hreal => @pair hreal hreal (hreal_add (hreal_mul (@fst hreal hreal _23757) (@fst hreal hreal _23758)) (hreal_mul (@snd hreal hreal _23757) (@snd hreal hreal _23758))) (hreal_add (hreal_mul (@fst hreal hreal _23757) (@snd hreal hreal _23758)) (hreal_mul (@snd hreal hreal _23757) (@fst hreal hreal _23758)))).
Proof. exact (eq_refl treal_mul). Qed.
Lemma treal_le_def : treal_le = (fun _23779 : prod hreal hreal => fun _23780 : prod hreal hreal => hreal_le (hreal_add (@fst hreal hreal _23779) (@snd hreal hreal _23780)) (hreal_add (@fst hreal hreal _23780) (@snd hreal hreal _23779))).
Proof. exact (eq_refl treal_le). Qed.
Lemma treal_inv_def : treal_inv = (fun _23801 : prod hreal hreal => @COND (prod hreal hreal) ((@fst hreal hreal _23801) = (@snd hreal hreal _23801)) (@pair hreal hreal (hreal_of_num (NUMERAL 0)) (hreal_of_num (NUMERAL 0))) (@COND (prod hreal hreal) (hreal_le (@snd hreal hreal _23801) (@fst hreal hreal _23801)) (@pair hreal hreal (hreal_inv (@ε hreal (fun d : hreal => (@fst hreal hreal _23801) = (hreal_add (@snd hreal hreal _23801) d)))) (hreal_of_num (NUMERAL 0))) (@pair hreal hreal (hreal_of_num (NUMERAL 0)) (hreal_inv (@ε hreal (fun d : hreal => (@snd hreal hreal _23801) = (hreal_add (@fst hreal hreal _23801) d))))))).
Proof. exact (eq_refl treal_inv). Qed.
Lemma treal_eq_def : treal_eq = (fun _23810 : prod hreal hreal => fun _23811 : prod hreal hreal => (hreal_add (@fst hreal hreal _23810) (@snd hreal hreal _23811)) = (hreal_add (@fst hreal hreal _23811) (@snd hreal hreal _23810))).
Proof. exact (eq_refl treal_eq). Qed.
Definition real_sgn : R -> R := fun _26598 : R => @COND R (Rlt (INR (NUMERAL 0)) _26598) (INR (NUMERAL (BIT1 0))) (@COND R (Rlt _26598 (INR (NUMERAL 0))) (Ropp (INR (NUMERAL (BIT1 0)))) (INR (NUMERAL 0))).
Lemma real_sgn_def : real_sgn = (fun _26598 : R => @COND R (Rlt (INR (NUMERAL 0)) _26598) (INR (NUMERAL (BIT1 0))) (@COND R (Rlt _26598 (INR (NUMERAL 0))) (Ropp (INR (NUMERAL (BIT1 0)))) (INR (NUMERAL 0)))).
Proof. exact (eq_refl real_sgn). Qed.
Definition sqrt : R -> R := fun _27149 : R => @ε R (fun y : R => ((real_sgn y) = (real_sgn _27149)) /\ ((Rpower_nat y (NUMERAL (BIT0 (BIT1 0)))) = (Rabs _27149))).
Lemma sqrt_def : sqrt = (fun _27149 : R => @ε R (fun y : R => ((real_sgn y) = (real_sgn _27149)) /\ ((Rpower_nat y (NUMERAL (BIT0 (BIT1 0)))) = (Rabs _27149)))).
Proof. exact (eq_refl sqrt). Qed.
Definition DECIMAL : nat -> nat -> R := fun _27828 : nat => fun _27829 : nat => Rdiv (INR _27828) (INR _27829).
Lemma DECIMAL_def : DECIMAL = (fun _27828 : nat => fun _27829 : nat => Rdiv (INR _27828) (INR _27829)).
Proof. exact (eq_refl DECIMAL). Qed.
Definition integer : R -> Prop := fun _28715 : R => exists n : nat, (Rabs _28715) = (INR n).
Lemma integer_def : integer = (fun _28715 : R => exists n : nat, (Rabs _28715) = (INR n)).
Proof. exact (eq_refl integer). Qed.
Definition int_le : Z -> Z -> Prop := fun _28741 : Z => fun _28742 : Z => Rle (IZR _28741) (IZR _28742).
Lemma int_le_def : int_le = (fun _28741 : Z => fun _28742 : Z => Rle (IZR _28741) (IZR _28742)).
Proof. exact (eq_refl int_le). Qed.
Definition int_lt : Z -> Z -> Prop := fun _28753 : Z => fun _28754 : Z => Rlt (IZR _28753) (IZR _28754).
Lemma int_lt_def : int_lt = (fun _28753 : Z => fun _28754 : Z => Rlt (IZR _28753) (IZR _28754)).
Proof. exact (eq_refl int_lt). Qed.
Definition int_ge : Z -> Z -> Prop := fun _28765 : Z => fun _28766 : Z => Rge (IZR _28765) (IZR _28766).
Lemma int_ge_def : int_ge = (fun _28765 : Z => fun _28766 : Z => Rge (IZR _28765) (IZR _28766)).
Proof. exact (eq_refl int_ge). Qed.
Definition int_gt : Z -> Z -> Prop := fun _28777 : Z => fun _28778 : Z => Rgt (IZR _28777) (IZR _28778).
Lemma int_gt_def : int_gt = (fun _28777 : Z => fun _28778 : Z => Rgt (IZR _28777) (IZR _28778)).
Proof. exact (eq_refl int_gt). Qed.
Definition int_of_num : nat -> Z := fun _28789 : nat => int_of_real (INR _28789).
Lemma int_of_num_def : int_of_num = (fun _28789 : nat => int_of_real (INR _28789)).
Proof. exact (eq_refl int_of_num). Qed.
Definition int_neg : Z -> Z := fun _28794 : Z => int_of_real (Ropp (IZR _28794)).
Lemma int_neg_def : int_neg = (fun _28794 : Z => int_of_real (Ropp (IZR _28794))).
Proof. exact (eq_refl int_neg). Qed.
Definition int_add : Z -> Z -> Z := fun _28803 : Z => fun _28804 : Z => int_of_real (Rplus (IZR _28803) (IZR _28804)).
Lemma int_add_def : int_add = (fun _28803 : Z => fun _28804 : Z => int_of_real (Rplus (IZR _28803) (IZR _28804))).
Proof. exact (eq_refl int_add). Qed.
Definition int_sub : Z -> Z -> Z := fun _28835 : Z => fun _28836 : Z => int_of_real (Rminus (IZR _28835) (IZR _28836)).
Lemma int_sub_def : int_sub = (fun _28835 : Z => fun _28836 : Z => int_of_real (Rminus (IZR _28835) (IZR _28836))).
Proof. exact (eq_refl int_sub). Qed.
Definition int_mul : Z -> Z -> Z := fun _28847 : Z => fun _28848 : Z => int_of_real (Rmult (IZR _28847) (IZR _28848)).
Lemma int_mul_def : int_mul = (fun _28847 : Z => fun _28848 : Z => int_of_real (Rmult (IZR _28847) (IZR _28848))).
Proof. exact (eq_refl int_mul). Qed.
Definition int_abs : Z -> Z := fun _28867 : Z => int_of_real (Rabs (IZR _28867)).
Lemma int_abs_def : int_abs = (fun _28867 : Z => int_of_real (Rabs (IZR _28867))).
Proof. exact (eq_refl int_abs). Qed.
Definition int_sgn : Z -> Z := fun _28878 : Z => int_of_real (real_sgn (IZR _28878)).
Lemma int_sgn_def : int_sgn = (fun _28878 : Z => int_of_real (real_sgn (IZR _28878))).
Proof. exact (eq_refl int_sgn). Qed.
Definition int_max : Z -> Z -> Z := fun _28938 : Z => fun _28939 : Z => int_of_real (Rmax (IZR _28938) (IZR _28939)).
Lemma int_max_def : int_max = (fun _28938 : Z => fun _28939 : Z => int_of_real (Rmax (IZR _28938) (IZR _28939))).
Proof. exact (eq_refl int_max). Qed.
Definition int_min : Z -> Z -> Z := fun _28956 : Z => fun _28957 : Z => int_of_real (Rmin (IZR _28956) (IZR _28957)).
Lemma int_min_def : int_min = (fun _28956 : Z => fun _28957 : Z => int_of_real (Rmin (IZR _28956) (IZR _28957))).
Proof. exact (eq_refl int_min). Qed.
Definition int_pow : Z -> nat -> Z := fun _28974 : Z => fun _28975 : nat => int_of_real (Rpower_nat (IZR _28974) _28975).
Lemma int_pow_def : int_pow = (fun _28974 : Z => fun _28975 : nat => int_of_real (Rpower_nat (IZR _28974) _28975)).
Proof. exact (eq_refl int_pow). Qed.
Definition div : Z -> Z -> Z := @ε ((prod nat (prod nat nat)) -> Z -> Z -> Z) (fun q : (prod nat (prod nat nat)) -> Z -> Z -> Z => forall _29326 : prod nat (prod nat nat), exists r : Z -> Z -> Z, forall m : Z, forall n : Z, @COND Prop (n = (int_of_num (NUMERAL 0))) (((q _29326 m n) = (int_of_num (NUMERAL 0))) /\ ((r m n) = m)) ((int_le (int_of_num (NUMERAL 0)) (r m n)) /\ ((int_lt (r m n) (int_abs n)) /\ (m = (int_add (int_mul (q _29326 m n) n) (r m n)))))) (@pair nat (prod nat nat) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))))).
Lemma div_def : div = (@ε ((prod nat (prod nat nat)) -> Z -> Z -> Z) (fun q : (prod nat (prod nat nat)) -> Z -> Z -> Z => forall _29326 : prod nat (prod nat nat), exists r : Z -> Z -> Z, forall m : Z, forall n : Z, @COND Prop (n = (int_of_num (NUMERAL 0))) (((q _29326 m n) = (int_of_num (NUMERAL 0))) /\ ((r m n) = m)) ((int_le (int_of_num (NUMERAL 0)) (r m n)) /\ ((int_lt (r m n) (int_abs n)) /\ (m = (int_add (int_mul (q _29326 m n) n) (r m n)))))) (@pair nat (prod nat nat) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 (BIT1 0))))))))))).
Proof. exact (eq_refl div). Qed.
Definition rem : Z -> Z -> Z := @ε ((prod nat (prod nat nat)) -> Z -> Z -> Z) (fun r : (prod nat (prod nat nat)) -> Z -> Z -> Z => forall _29327 : prod nat (prod nat nat), forall m : Z, forall n : Z, @COND Prop (n = (int_of_num (NUMERAL 0))) (((div m n) = (int_of_num (NUMERAL 0))) /\ ((r _29327 m n) = m)) ((int_le (int_of_num (NUMERAL 0)) (r _29327 m n)) /\ ((int_lt (r _29327 m n) (int_abs n)) /\ (m = (int_add (int_mul (div m n) n) (r _29327 m n)))))) (@pair nat (prod nat nat) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))))).
Lemma rem_def : rem = (@ε ((prod nat (prod nat nat)) -> Z -> Z -> Z) (fun r : (prod nat (prod nat nat)) -> Z -> Z -> Z => forall _29327 : prod nat (prod nat nat), forall m : Z, forall n : Z, @COND Prop (n = (int_of_num (NUMERAL 0))) (((div m n) = (int_of_num (NUMERAL 0))) /\ ((r _29327 m n) = m)) ((int_le (int_of_num (NUMERAL 0)) (r _29327 m n)) /\ ((int_lt (r _29327 m n) (int_abs n)) /\ (m = (int_add (int_mul (div m n) n) (r _29327 m n)))))) (@pair nat (prod nat nat) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 0))))))))))).
Proof. exact (eq_refl rem). Qed.
Definition eq2 {A : Type'} : A -> A -> (A -> A -> Prop) -> Prop := fun _29602 : A => fun _29603 : A => fun _29604 : A -> A -> Prop => _29604 _29602 _29603.
Lemma eq2_def {A : Type'} : (@eq2 A) = (fun _29602 : A => fun _29603 : A => fun _29604 : A -> A -> Prop => _29604 _29602 _29603).
Proof. exact (eq_refl (@eq2 A)). Qed.
Definition real_mod : R -> R -> R -> Prop := fun _29623 : R => fun _29624 : R => fun _29625 : R => exists q : R, (integer q) /\ ((Rminus _29624 _29625) = (Rmult q _29623)).
Lemma real_mod_def : real_mod = (fun _29623 : R => fun _29624 : R => fun _29625 : R => exists q : R, (integer q) /\ ((Rminus _29624 _29625) = (Rmult q _29623))).
Proof. exact (eq_refl real_mod). Qed.
Definition int_divides : Z -> Z -> Prop := fun _29644 : Z => fun _29645 : Z => exists x : Z, _29645 = (int_mul _29644 x).
Lemma int_divides_def : int_divides = (fun _29644 : Z => fun _29645 : Z => exists x : Z, _29645 = (int_mul _29644 x)).
Proof. exact (eq_refl int_divides). Qed.
Definition int_mod : Z -> Z -> Z -> Prop := fun _29664 : Z => fun _29665 : Z => fun _29666 : Z => int_divides _29664 (int_sub _29665 _29666).
Lemma int_mod_def : int_mod = (fun _29664 : Z => fun _29665 : Z => fun _29666 : Z => int_divides _29664 (int_sub _29665 _29666)).
Proof. exact (eq_refl int_mod). Qed.
Definition int_coprime : (prod Z Z) -> Prop := fun _29691 : prod Z Z => exists x : Z, exists y : Z, (int_add (int_mul (@fst Z Z _29691) x) (int_mul (@snd Z Z _29691) y)) = (int_of_num (NUMERAL (BIT1 0))).
Lemma int_coprime_def : int_coprime = (fun _29691 : prod Z Z => exists x : Z, exists y : Z, (int_add (int_mul (@fst Z Z _29691) x) (int_mul (@snd Z Z _29691) y)) = (int_of_num (NUMERAL (BIT1 0)))).
Proof. exact (eq_refl int_coprime). Qed.
Definition int_gcd : (prod Z Z) -> Z := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (prod Z Z) -> Z) (fun d : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (prod Z Z) -> Z => forall _30960 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))), forall a : Z, forall b : Z, (int_le (int_of_num (NUMERAL 0)) (d _30960 (@pair Z Z a b))) /\ ((int_divides (d _30960 (@pair Z Z a b)) a) /\ ((int_divides (d _30960 (@pair Z Z a b)) b) /\ (exists x : Z, exists y : Z, (d _30960 (@pair Z Z a b)) = (int_add (int_mul a x) (int_mul b y)))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))))))))).
Lemma int_gcd_def : int_gcd = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (prod Z Z) -> Z) (fun d : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (prod Z Z) -> Z => forall _30960 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))), forall a : Z, forall b : Z, (int_le (int_of_num (NUMERAL 0)) (d _30960 (@pair Z Z a b))) /\ ((int_divides (d _30960 (@pair Z Z a b)) a) /\ ((int_divides (d _30960 (@pair Z Z a b)) b) /\ (exists x : Z, exists y : Z, (d _30960 (@pair Z Z a b)) = (int_add (int_mul a x) (int_mul b y)))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0))))))))))))))).
Proof. exact (eq_refl int_gcd). Qed.
Definition int_lcm : (prod Z Z) -> Z := fun _30961 : prod Z Z => @COND Z ((int_mul (@fst Z Z _30961) (@snd Z Z _30961)) = (int_of_num (NUMERAL 0))) (int_of_num (NUMERAL 0)) (div (int_abs (int_mul (@fst Z Z _30961) (@snd Z Z _30961))) (int_gcd (@pair Z Z (@fst Z Z _30961) (@snd Z Z _30961)))).
Lemma int_lcm_def : int_lcm = (fun _30961 : prod Z Z => @COND Z ((int_mul (@fst Z Z _30961) (@snd Z Z _30961)) = (int_of_num (NUMERAL 0))) (int_of_num (NUMERAL 0)) (div (int_abs (int_mul (@fst Z Z _30961) (@snd Z Z _30961))) (int_gcd (@pair Z Z (@fst Z Z _30961) (@snd Z Z _30961))))).
Proof. exact (eq_refl int_lcm). Qed.
Definition num_of_int : Z -> nat := fun _31234 : Z => @ε nat (fun n : nat => (int_of_num n) = _31234).
Lemma num_of_int_def : num_of_int = (fun _31234 : Z => @ε nat (fun n : nat => (int_of_num n) = _31234)).
Proof. exact (eq_refl num_of_int). Qed.
Definition num_divides : nat -> nat -> Prop := fun _31266 : nat => fun _31267 : nat => int_divides (int_of_num _31266) (int_of_num _31267).
Lemma num_divides_def : num_divides = (fun _31266 : nat => fun _31267 : nat => int_divides (int_of_num _31266) (int_of_num _31267)).
Proof. exact (eq_refl num_divides). Qed.
Definition num_mod : nat -> nat -> nat -> Prop := fun _31278 : nat => fun _31279 : nat => fun _31280 : nat => int_mod (int_of_num _31278) (int_of_num _31279) (int_of_num _31280).
Lemma num_mod_def : num_mod = (fun _31278 : nat => fun _31279 : nat => fun _31280 : nat => int_mod (int_of_num _31278) (int_of_num _31279) (int_of_num _31280)).
Proof. exact (eq_refl num_mod). Qed.
Definition num_coprime : (prod nat nat) -> Prop := fun _31299 : prod nat nat => int_coprime (@pair Z Z (int_of_num (@fst nat nat _31299)) (int_of_num (@snd nat nat _31299))).
Lemma num_coprime_def : num_coprime = (fun _31299 : prod nat nat => int_coprime (@pair Z Z (int_of_num (@fst nat nat _31299)) (int_of_num (@snd nat nat _31299)))).
Proof. exact (eq_refl num_coprime). Qed.
Definition num_gcd : (prod nat nat) -> nat := fun _31308 : prod nat nat => num_of_int (int_gcd (@pair Z Z (int_of_num (@fst nat nat _31308)) (int_of_num (@snd nat nat _31308)))).
Lemma num_gcd_def : num_gcd = (fun _31308 : prod nat nat => num_of_int (int_gcd (@pair Z Z (int_of_num (@fst nat nat _31308)) (int_of_num (@snd nat nat _31308))))).
Proof. exact (eq_refl num_gcd). Qed.
Definition num_lcm : (prod nat nat) -> nat := fun _31317 : prod nat nat => num_of_int (int_lcm (@pair Z Z (int_of_num (@fst nat nat _31317)) (int_of_num (@snd nat nat _31317)))).
Lemma num_lcm_def : num_lcm = (fun _31317 : prod nat nat => num_of_int (int_lcm (@pair Z Z (int_of_num (@fst nat nat _31317)) (int_of_num (@snd nat nat _31317))))).
Proof. exact (eq_refl num_lcm). Qed.
Definition prime : nat -> Prop := fun _32102 : nat => (~ (_32102 = (NUMERAL (BIT1 0)))) /\ (forall x : nat, (num_divides x _32102) -> (x = (NUMERAL (BIT1 0))) \/ (x = _32102)).
Lemma prime_def : prime = (fun _32102 : nat => (~ (_32102 = (NUMERAL (BIT1 0)))) /\ (forall x : nat, (num_divides x _32102) -> (x = (NUMERAL (BIT1 0))) \/ (x = _32102))).
Proof. exact (eq_refl prime). Qed.
Definition real_zpow : R -> Z -> R := fun _32260 : R => fun _32261 : Z => @COND R (int_le (int_of_num (NUMERAL 0)) _32261) (Rpower_nat _32260 (num_of_int _32261)) (Rinv (Rpower_nat _32260 (num_of_int (int_neg _32261)))).
Lemma real_zpow_def : real_zpow = (fun _32260 : R => fun _32261 : Z => @COND R (int_le (int_of_num (NUMERAL 0)) _32261) (Rpower_nat _32260 (num_of_int _32261)) (Rinv (Rpower_nat _32260 (num_of_int (int_neg _32261))))).
Proof. exact (eq_refl real_zpow). Qed.
Definition IN {A : Type'} : A -> (A -> Prop) -> Prop := fun _32317 : A => fun _32318 : A -> Prop => _32318 _32317.
Lemma IN_def {A : Type'} : (@IN A) = (fun _32317 : A => fun _32318 : A -> Prop => _32318 _32317).
Proof. exact (eq_refl (@IN A)). Qed.
Definition GSPEC {A : Type'} : (A -> Prop) -> A -> Prop := fun _32329 : A -> Prop => _32329.
Lemma GSPEC_def {A : Type'} : (@GSPEC A) = (fun _32329 : A -> Prop => _32329).
Proof. exact (eq_refl (@GSPEC A)). Qed.
Definition SETSPEC {A : Type'} : A -> Prop -> A -> Prop := fun _32334 : A => fun _32335 : Prop => fun _32336 : A => _32335 /\ (_32334 = _32336).
Lemma SETSPEC_def {A : Type'} : (@SETSPEC A) = (fun _32334 : A => fun _32335 : Prop => fun _32336 : A => _32335 /\ (_32334 = _32336)).
Proof. exact (eq_refl (@SETSPEC A)). Qed.
Definition EMPTY {A : Type'} : A -> Prop := fun x : A => False.
Lemma EMPTY_def {A : Type'} : (@EMPTY A) = (fun x : A => False).
Proof. exact (eq_refl (@EMPTY A)). Qed.
Definition INSERT {A : Type'} : A -> (A -> Prop) -> A -> Prop := fun _32373 : A => fun _32374 : A -> Prop => fun y : A => (@IN A y _32374) \/ (y = _32373).
Lemma INSERT_def {A : Type'} : (@INSERT A) = (fun _32373 : A => fun _32374 : A -> Prop => fun y : A => (@IN A y _32374) \/ (y = _32373)).
Proof. exact (eq_refl (@INSERT A)). Qed.
Definition UNIV {A : Type'} : A -> Prop := fun x : A => True.
Lemma UNIV_def {A : Type'} : (@UNIV A) = (fun x : A => True).
Proof. exact (eq_refl (@UNIV A)). Qed.
Definition UNION {A : Type'} : (A -> Prop) -> (A -> Prop) -> A -> Prop := fun _32385 : A -> Prop => fun _32386 : A -> Prop => @GSPEC A (fun GEN_PVAR_0 : A => exists x : A, @SETSPEC A GEN_PVAR_0 ((@IN A x _32385) \/ (@IN A x _32386)) x).
Lemma UNION_def {A : Type'} : (@UNION A) = (fun _32385 : A -> Prop => fun _32386 : A -> Prop => @GSPEC A (fun GEN_PVAR_0 : A => exists x : A, @SETSPEC A GEN_PVAR_0 ((@IN A x _32385) \/ (@IN A x _32386)) x)).
Proof. exact (eq_refl (@UNION A)). Qed.
Definition UNIONS {A : Type'} : ((A -> Prop) -> Prop) -> A -> Prop := fun _32397 : (A -> Prop) -> Prop => @GSPEC A (fun GEN_PVAR_1 : A => exists x : A, @SETSPEC A GEN_PVAR_1 (exists u : A -> Prop, (@IN (A -> Prop) u _32397) /\ (@IN A x u)) x).
Lemma UNIONS_def {A : Type'} : (@UNIONS A) = (fun _32397 : (A -> Prop) -> Prop => @GSPEC A (fun GEN_PVAR_1 : A => exists x : A, @SETSPEC A GEN_PVAR_1 (exists u : A -> Prop, (@IN (A -> Prop) u _32397) /\ (@IN A x u)) x)).
Proof. exact (eq_refl (@UNIONS A)). Qed.
Definition INTER {A : Type'} : (A -> Prop) -> (A -> Prop) -> A -> Prop := fun _32402 : A -> Prop => fun _32403 : A -> Prop => @GSPEC A (fun GEN_PVAR_2 : A => exists x : A, @SETSPEC A GEN_PVAR_2 ((@IN A x _32402) /\ (@IN A x _32403)) x).
Lemma INTER_def {A : Type'} : (@INTER A) = (fun _32402 : A -> Prop => fun _32403 : A -> Prop => @GSPEC A (fun GEN_PVAR_2 : A => exists x : A, @SETSPEC A GEN_PVAR_2 ((@IN A x _32402) /\ (@IN A x _32403)) x)).
Proof. exact (eq_refl (@INTER A)). Qed.
Definition INTERS {A : Type'} : ((A -> Prop) -> Prop) -> A -> Prop := fun _32414 : (A -> Prop) -> Prop => @GSPEC A (fun GEN_PVAR_3 : A => exists x : A, @SETSPEC A GEN_PVAR_3 (forall u : A -> Prop, (@IN (A -> Prop) u _32414) -> @IN A x u) x).
Lemma INTERS_def {A : Type'} : (@INTERS A) = (fun _32414 : (A -> Prop) -> Prop => @GSPEC A (fun GEN_PVAR_3 : A => exists x : A, @SETSPEC A GEN_PVAR_3 (forall u : A -> Prop, (@IN (A -> Prop) u _32414) -> @IN A x u) x)).
Proof. exact (eq_refl (@INTERS A)). Qed.
Definition DIFF {A : Type'} : (A -> Prop) -> (A -> Prop) -> A -> Prop := fun _32419 : A -> Prop => fun _32420 : A -> Prop => @GSPEC A (fun GEN_PVAR_4 : A => exists x : A, @SETSPEC A GEN_PVAR_4 ((@IN A x _32419) /\ (~ (@IN A x _32420))) x).
Lemma DIFF_def {A : Type'} : (@DIFF A) = (fun _32419 : A -> Prop => fun _32420 : A -> Prop => @GSPEC A (fun GEN_PVAR_4 : A => exists x : A, @SETSPEC A GEN_PVAR_4 ((@IN A x _32419) /\ (~ (@IN A x _32420))) x)).
Proof. exact (eq_refl (@DIFF A)). Qed.
Definition DELETE {A : Type'} : (A -> Prop) -> A -> A -> Prop := fun _32431 : A -> Prop => fun _32432 : A => @GSPEC A (fun GEN_PVAR_6 : A => exists y : A, @SETSPEC A GEN_PVAR_6 ((@IN A y _32431) /\ (~ (y = _32432))) y).
Lemma DELETE_def {A : Type'} : (@DELETE A) = (fun _32431 : A -> Prop => fun _32432 : A => @GSPEC A (fun GEN_PVAR_6 : A => exists y : A, @SETSPEC A GEN_PVAR_6 ((@IN A y _32431) /\ (~ (y = _32432))) y)).
Proof. exact (eq_refl (@DELETE A)). Qed.
Definition SUBSET {A : Type'} : (A -> Prop) -> (A -> Prop) -> Prop := fun _32443 : A -> Prop => fun _32444 : A -> Prop => forall x : A, (@IN A x _32443) -> @IN A x _32444.
Lemma SUBSET_def {A : Type'} : (@SUBSET A) = (fun _32443 : A -> Prop => fun _32444 : A -> Prop => forall x : A, (@IN A x _32443) -> @IN A x _32444).
Proof. exact (eq_refl (@SUBSET A)). Qed.
Definition PSUBSET {A : Type'} : (A -> Prop) -> (A -> Prop) -> Prop := fun _32455 : A -> Prop => fun _32456 : A -> Prop => (@SUBSET A _32455 _32456) /\ (~ (_32455 = _32456)).
Lemma PSUBSET_def {A : Type'} : (@PSUBSET A) = (fun _32455 : A -> Prop => fun _32456 : A -> Prop => (@SUBSET A _32455 _32456) /\ (~ (_32455 = _32456))).
Proof. exact (eq_refl (@PSUBSET A)). Qed.
Definition DISJOINT {A : Type'} : (A -> Prop) -> (A -> Prop) -> Prop := fun _32467 : A -> Prop => fun _32468 : A -> Prop => (@INTER A _32467 _32468) = (@EMPTY A).
Lemma DISJOINT_def {A : Type'} : (@DISJOINT A) = (fun _32467 : A -> Prop => fun _32468 : A -> Prop => (@INTER A _32467 _32468) = (@EMPTY A)).
Proof. exact (eq_refl (@DISJOINT A)). Qed.
Definition SING {A : Type'} : (A -> Prop) -> Prop := fun _32479 : A -> Prop => exists x : A, _32479 = (@INSERT A x (@EMPTY A)).
Lemma SING_def {A : Type'} : (@SING A) = (fun _32479 : A -> Prop => exists x : A, _32479 = (@INSERT A x (@EMPTY A))).
Proof. exact (eq_refl (@SING A)). Qed.
Definition FINITE {A : Type'} : (A -> Prop) -> Prop := fun a : A -> Prop => forall FINITE' : (A -> Prop) -> Prop, (forall a' : A -> Prop, ((a' = (@EMPTY A)) \/ (exists x : A, exists s : A -> Prop, (a' = (@INSERT A x s)) /\ (FINITE' s))) -> FINITE' a') -> FINITE' a.
Lemma FINITE_def {A : Type'} : (@FINITE A) = (fun a : A -> Prop => forall FINITE' : (A -> Prop) -> Prop, (forall a' : A -> Prop, ((a' = (@EMPTY A)) \/ (exists x : A, exists s : A -> Prop, (a' = (@INSERT A x s)) /\ (FINITE' s))) -> FINITE' a') -> FINITE' a).
Proof. exact (eq_refl (@FINITE A)). Qed.
Definition INFINITE {A : Type'} : (A -> Prop) -> Prop := fun _32488 : A -> Prop => ~ (@FINITE A _32488).
Lemma INFINITE_def {A : Type'} : (@INFINITE A) = (fun _32488 : A -> Prop => ~ (@FINITE A _32488)).
Proof. exact (eq_refl (@INFINITE A)). Qed.
Definition IMAGE {A B : Type'} : (A -> B) -> (A -> Prop) -> B -> Prop := fun _32493 : A -> B => fun _32494 : A -> Prop => @GSPEC B (fun GEN_PVAR_7 : B => exists y : B, @SETSPEC B GEN_PVAR_7 (exists x : A, (@IN A x _32494) /\ (y = (_32493 x))) y).
Lemma IMAGE_def {A B : Type'} : (@IMAGE A B) = (fun _32493 : A -> B => fun _32494 : A -> Prop => @GSPEC B (fun GEN_PVAR_7 : B => exists y : B, @SETSPEC B GEN_PVAR_7 (exists x : A, (@IN A x _32494) /\ (y = (_32493 x))) y)).
Proof. exact (eq_refl (@IMAGE A B)). Qed.
Definition INJ {A B : Type'} : (A -> B) -> (A -> Prop) -> (B -> Prop) -> Prop := fun _32505 : A -> B => fun _32506 : A -> Prop => fun _32507 : B -> Prop => (forall x : A, (@IN A x _32506) -> @IN B (_32505 x) _32507) /\ (forall x : A, forall y : A, ((@IN A x _32506) /\ ((@IN A y _32506) /\ ((_32505 x) = (_32505 y)))) -> x = y).
Lemma INJ_def {A B : Type'} : (@INJ A B) = (fun _32505 : A -> B => fun _32506 : A -> Prop => fun _32507 : B -> Prop => (forall x : A, (@IN A x _32506) -> @IN B (_32505 x) _32507) /\ (forall x : A, forall y : A, ((@IN A x _32506) /\ ((@IN A y _32506) /\ ((_32505 x) = (_32505 y)))) -> x = y)).
Proof. exact (eq_refl (@INJ A B)). Qed.
Definition SURJ {A B : Type'} : (A -> B) -> (A -> Prop) -> (B -> Prop) -> Prop := fun _32526 : A -> B => fun _32527 : A -> Prop => fun _32528 : B -> Prop => (forall x : A, (@IN A x _32527) -> @IN B (_32526 x) _32528) /\ (forall x : B, (@IN B x _32528) -> exists y : A, (@IN A y _32527) /\ ((_32526 y) = x)).
Lemma SURJ_def {A B : Type'} : (@SURJ A B) = (fun _32526 : A -> B => fun _32527 : A -> Prop => fun _32528 : B -> Prop => (forall x : A, (@IN A x _32527) -> @IN B (_32526 x) _32528) /\ (forall x : B, (@IN B x _32528) -> exists y : A, (@IN A y _32527) /\ ((_32526 y) = x))).
Proof. exact (eq_refl (@SURJ A B)). Qed.
Definition BIJ {A B : Type'} : (A -> B) -> (A -> Prop) -> (B -> Prop) -> Prop := fun _32547 : A -> B => fun _32548 : A -> Prop => fun _32549 : B -> Prop => (@INJ A B _32547 _32548 _32549) /\ (@SURJ A B _32547 _32548 _32549).
Lemma BIJ_def {A B : Type'} : (@BIJ A B) = (fun _32547 : A -> B => fun _32548 : A -> Prop => fun _32549 : B -> Prop => (@INJ A B _32547 _32548 _32549) /\ (@SURJ A B _32547 _32548 _32549)).
Proof. exact (eq_refl (@BIJ A B)). Qed.
Definition CHOICE {A : Type'} : (A -> Prop) -> A := fun _32568 : A -> Prop => @ε A (fun x : A => @IN A x _32568).
Lemma CHOICE_def {A : Type'} : (@CHOICE A) = (fun _32568 : A -> Prop => @ε A (fun x : A => @IN A x _32568)).
Proof. exact (eq_refl (@CHOICE A)). Qed.
Definition REST {A : Type'} : (A -> Prop) -> A -> Prop := fun _32573 : A -> Prop => @DELETE A _32573 (@CHOICE A _32573).
Lemma REST_def {A : Type'} : (@REST A) = (fun _32573 : A -> Prop => @DELETE A _32573 (@CHOICE A _32573)).
Proof. exact (eq_refl (@REST A)). Qed.
Definition FINREC {A B : Type'} : (A -> B -> B) -> B -> (A -> Prop) -> B -> nat -> Prop := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (A -> B -> B) -> B -> (A -> Prop) -> B -> nat -> Prop) (fun FINREC' : (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (A -> B -> B) -> B -> (A -> Prop) -> B -> nat -> Prop => forall _42175 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), (forall f : A -> B -> B, forall s : A -> Prop, forall a : B, forall b : B, (FINREC' _42175 f b s a (NUMERAL 0)) = ((s = (@EMPTY A)) /\ (a = b))) /\ (forall b : B, forall s : A -> Prop, forall n : nat, forall a : B, forall f : A -> B -> B, (FINREC' _42175 f b s a (S n)) = (exists x : A, exists c : B, (@IN A x s) /\ ((FINREC' _42175 f b (@DELETE A s x) c n) /\ (a = (f x c)))))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0))))))))))))).
Lemma FINREC_def {A B : Type'} : (@FINREC A B) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (A -> B -> B) -> B -> (A -> Prop) -> B -> nat -> Prop) (fun FINREC' : (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (A -> B -> B) -> B -> (A -> Prop) -> B -> nat -> Prop => forall _42175 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), (forall f : A -> B -> B, forall s : A -> Prop, forall a : B, forall b : B, (FINREC' _42175 f b s a (NUMERAL 0)) = ((s = (@EMPTY A)) /\ (a = b))) /\ (forall b : B, forall s : A -> Prop, forall n : nat, forall a : B, forall f : A -> B -> B, (FINREC' _42175 f b s a (S n)) = (exists x : A, exists c : B, (@IN A x s) /\ ((FINREC' _42175 f b (@DELETE A s x) c n) /\ (a = (f x c)))))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))))))))).
Proof. exact (eq_refl (@FINREC A B)). Qed.
Definition ITSET {A B : Type'} : (A -> B -> B) -> (A -> Prop) -> B -> B := fun _43025 : A -> B -> B => fun _43026 : A -> Prop => fun _43027 : B => @ε ((A -> Prop) -> B) (fun g : (A -> Prop) -> B => ((g (@EMPTY A)) = _43027) /\ (forall x : A, forall s : A -> Prop, (@FINITE A s) -> (g (@INSERT A x s)) = (@COND B (@IN A x s) (g s) (_43025 x (g s))))) _43026.
Lemma ITSET_def {A B : Type'} : (@ITSET A B) = (fun _43025 : A -> B -> B => fun _43026 : A -> Prop => fun _43027 : B => @ε ((A -> Prop) -> B) (fun g : (A -> Prop) -> B => ((g (@EMPTY A)) = _43027) /\ (forall x : A, forall s : A -> Prop, (@FINITE A s) -> (g (@INSERT A x s)) = (@COND B (@IN A x s) (g s) (_43025 x (g s))))) _43026).
Proof. exact (eq_refl (@ITSET A B)). Qed.
Definition CARD {A : Type'} : (A -> Prop) -> nat := fun _43228 : A -> Prop => @ITSET A nat (fun x : A => fun n : nat => S n) _43228 (NUMERAL 0).
Lemma CARD_def {A : Type'} : (@CARD A) = (fun _43228 : A -> Prop => @ITSET A nat (fun x : A => fun n : nat => S n) _43228 (NUMERAL 0)).
Proof. exact (eq_refl (@CARD A)). Qed.
Definition HAS_SIZE {A : Type'} : (A -> Prop) -> nat -> Prop := fun _43403 : A -> Prop => fun _43404 : nat => (@FINITE A _43403) /\ ((@CARD A _43403) = _43404).
Lemma HAS_SIZE_def {A : Type'} : (@HAS_SIZE A) = (fun _43403 : A -> Prop => fun _43404 : nat => (@FINITE A _43403) /\ ((@CARD A _43403) = _43404)).
Proof. exact (eq_refl (@HAS_SIZE A)). Qed.
Definition CROSS {A B : Type'} : (A -> Prop) -> (B -> Prop) -> (prod A B) -> Prop := fun _47322 : A -> Prop => fun _47323 : B -> Prop => @GSPEC (prod A B) (fun GEN_PVAR_132 : prod A B => exists x : A, exists y : B, @SETSPEC (prod A B) GEN_PVAR_132 ((@IN A x _47322) /\ (@IN B y _47323)) (@pair A B x y)).
Lemma CROSS_def {A B : Type'} : (@CROSS A B) = (fun _47322 : A -> Prop => fun _47323 : B -> Prop => @GSPEC (prod A B) (fun GEN_PVAR_132 : prod A B => exists x : A, exists y : B, @SETSPEC (prod A B) GEN_PVAR_132 ((@IN A x _47322) /\ (@IN B y _47323)) (@pair A B x y))).
Proof. exact (eq_refl (@CROSS A B)). Qed.
Definition ARB {A : Type'} : A := @ε A (fun x : A => False).
Lemma ARB_def {A : Type'} : (@ARB A) = (@ε A (fun x : A => False)).
Proof. exact (eq_refl (@ARB A)). Qed.
Definition EXTENSIONAL {A B : Type'} : (A -> Prop) -> (A -> B) -> Prop := fun _48096 : A -> Prop => @GSPEC (A -> B) (fun GEN_PVAR_141 : A -> B => exists f : A -> B, @SETSPEC (A -> B) GEN_PVAR_141 (forall x : A, (~ (@IN A x _48096)) -> (f x) = (@ARB B)) f).
Lemma EXTENSIONAL_def {A B : Type'} : (@EXTENSIONAL A B) = (fun _48096 : A -> Prop => @GSPEC (A -> B) (fun GEN_PVAR_141 : A -> B => exists f : A -> B, @SETSPEC (A -> B) GEN_PVAR_141 (forall x : A, (~ (@IN A x _48096)) -> (f x) = (@ARB B)) f)).
Proof. exact (eq_refl (@EXTENSIONAL A B)). Qed.
Definition RESTRICTION {A B : Type'} : (A -> Prop) -> (A -> B) -> A -> B := fun _48148 : A -> Prop => fun _48149 : A -> B => fun _48150 : A => @COND B (@IN A _48150 _48148) (_48149 _48150) (@ARB B).
Lemma RESTRICTION_def {A B : Type'} : (@RESTRICTION A B) = (fun _48148 : A -> Prop => fun _48149 : A -> B => fun _48150 : A => @COND B (@IN A _48150 _48148) (_48149 _48150) (@ARB B)).
Proof. exact (eq_refl (@RESTRICTION A B)). Qed.
Definition cartesian_product {A K : Type'} : (K -> Prop) -> (K -> A -> Prop) -> (K -> A) -> Prop := fun _48343 : K -> Prop => fun _48344 : K -> A -> Prop => @GSPEC (K -> A) (fun GEN_PVAR_142 : K -> A => exists f : K -> A, @SETSPEC (K -> A) GEN_PVAR_142 ((@EXTENSIONAL K A _48343 f) /\ (forall i : K, (@IN K i _48343) -> @IN A (f i) (_48344 i))) f).
Lemma cartesian_product_def {A K : Type'} : (@cartesian_product A K) = (fun _48343 : K -> Prop => fun _48344 : K -> A -> Prop => @GSPEC (K -> A) (fun GEN_PVAR_142 : K -> A => exists f : K -> A, @SETSPEC (K -> A) GEN_PVAR_142 ((@EXTENSIONAL K A _48343 f) /\ (forall i : K, (@IN K i _48343) -> @IN A (f i) (_48344 i))) f)).
Proof. exact (eq_refl (@cartesian_product A K)). Qed.
Definition product_map {A B K : Type'} : (K -> Prop) -> (K -> A -> B) -> (K -> A) -> K -> B := fun _49392 : K -> Prop => fun _49393 : K -> A -> B => fun x : K -> A => @RESTRICTION K B _49392 (fun i : K => _49393 i (x i)).
Lemma product_map_def {A B K : Type'} : (@product_map A B K) = (fun _49392 : K -> Prop => fun _49393 : K -> A -> B => fun x : K -> A => @RESTRICTION K B _49392 (fun i : K => _49393 i (x i))).
Proof. exact (eq_refl (@product_map A B K)). Qed.
Definition disjoint_union {A K : Type'} : (K -> Prop) -> (K -> A -> Prop) -> (prod K A) -> Prop := fun _49528 : K -> Prop => fun _49529 : K -> A -> Prop => @GSPEC (prod K A) (fun GEN_PVAR_145 : prod K A => exists i : K, exists x : A, @SETSPEC (prod K A) GEN_PVAR_145 ((@IN K i _49528) /\ (@IN A x (_49529 i))) (@pair K A i x)).
Lemma disjoint_union_def {A K : Type'} : (@disjoint_union A K) = (fun _49528 : K -> Prop => fun _49529 : K -> A -> Prop => @GSPEC (prod K A) (fun GEN_PVAR_145 : prod K A => exists i : K, exists x : A, @SETSPEC (prod K A) GEN_PVAR_145 ((@IN K i _49528) /\ (@IN A x (_49529 i))) (@pair K A i x))).
Proof. exact (eq_refl (@disjoint_union A K)). Qed.
Definition set_of_list {A : Type'} : (list A) -> A -> Prop := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))))))) -> (list A) -> A -> Prop) (fun set_of_list' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))))))) -> (list A) -> A -> Prop => forall _56425 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))))), ((set_of_list' _56425 (@nil A)) = (@EMPTY A)) /\ (forall h : A, forall t : list A, (set_of_list' _56425 (@cons A h t)) = (@INSERT A h (set_of_list' _56425 t)))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))))) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))))) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))))))))))))).
Lemma set_of_list_def {A : Type'} : (@set_of_list A) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))))))) -> (list A) -> A -> Prop) (fun set_of_list' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))))))) -> (list A) -> A -> Prop => forall _56425 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))))), ((set_of_list' _56425 (@nil A)) = (@EMPTY A)) /\ (forall h : A, forall t : list A, (set_of_list' _56425 (@cons A h t)) = (@INSERT A h (set_of_list' _56425 t)))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))))) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))))) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 (BIT1 0))))))))))))))))))).
Proof. exact (eq_refl (@set_of_list A)). Qed.
Definition list_of_set {A : Type'} : (A -> Prop) -> list A := fun _56426 : A -> Prop => @ε (list A) (fun l : list A => ((@set_of_list A l) = _56426) /\ ((@List.length A l) = (@CARD A _56426))).
Lemma list_of_set_def {A : Type'} : (@list_of_set A) = (fun _56426 : A -> Prop => @ε (list A) (fun l : list A => ((@set_of_list A l) = _56426) /\ ((@List.length A l) = (@CARD A _56426)))).
Proof. exact (eq_refl (@list_of_set A)). Qed.
Definition pairwise {A : Type'} : (A -> A -> Prop) -> (A -> Prop) -> Prop := fun _56616 : A -> A -> Prop => fun _56617 : A -> Prop => forall x : A, forall y : A, ((@IN A x _56617) /\ ((@IN A y _56617) /\ (~ (x = y)))) -> _56616 x y.
Lemma pairwise_def {A : Type'} : (@pairwise A) = (fun _56616 : A -> A -> Prop => fun _56617 : A -> Prop => forall x : A, forall y : A, ((@IN A x _56617) /\ ((@IN A y _56617) /\ (~ (x = y)))) -> _56616 x y).
Proof. exact (eq_refl (@pairwise A)). Qed.
Definition UNION_OF {A : Type'} : (((A -> Prop) -> Prop) -> Prop) -> ((A -> Prop) -> Prop) -> (A -> Prop) -> Prop := fun _57329 : ((A -> Prop) -> Prop) -> Prop => fun _57330 : (A -> Prop) -> Prop => fun s : A -> Prop => exists u : (A -> Prop) -> Prop, (_57329 u) /\ ((forall c : A -> Prop, (@IN (A -> Prop) c u) -> _57330 c) /\ ((@UNIONS A u) = s)).
Lemma UNION_OF_def {A : Type'} : (@UNION_OF A) = (fun _57329 : ((A -> Prop) -> Prop) -> Prop => fun _57330 : (A -> Prop) -> Prop => fun s : A -> Prop => exists u : (A -> Prop) -> Prop, (_57329 u) /\ ((forall c : A -> Prop, (@IN (A -> Prop) c u) -> _57330 c) /\ ((@UNIONS A u) = s))).
Proof. exact (eq_refl (@UNION_OF A)). Qed.
Definition INTERSECTION_OF {A : Type'} : (((A -> Prop) -> Prop) -> Prop) -> ((A -> Prop) -> Prop) -> (A -> Prop) -> Prop := fun _57341 : ((A -> Prop) -> Prop) -> Prop => fun _57342 : (A -> Prop) -> Prop => fun s : A -> Prop => exists u : (A -> Prop) -> Prop, (_57341 u) /\ ((forall c : A -> Prop, (@IN (A -> Prop) c u) -> _57342 c) /\ ((@INTERS A u) = s)).
Lemma INTERSECTION_OF_def {A : Type'} : (@INTERSECTION_OF A) = (fun _57341 : ((A -> Prop) -> Prop) -> Prop => fun _57342 : (A -> Prop) -> Prop => fun s : A -> Prop => exists u : (A -> Prop) -> Prop, (_57341 u) /\ ((forall c : A -> Prop, (@IN (A -> Prop) c u) -> _57342 c) /\ ((@INTERS A u) = s))).
Proof. exact (eq_refl (@INTERSECTION_OF A)). Qed.
Definition ARBITRARY {A : Type'} : ((A -> Prop) -> Prop) -> Prop := fun _57477 : (A -> Prop) -> Prop => True.
Lemma ARBITRARY_def {A : Type'} : (@ARBITRARY A) = (fun _57477 : (A -> Prop) -> Prop => True).
Proof. exact (eq_refl (@ARBITRARY A)). Qed.
Definition le_c {A B : Type'} : (A -> Prop) -> (B -> Prop) -> Prop := fun _64071 : A -> Prop => fun _64072 : B -> Prop => exists f : A -> B, (forall x : A, (@IN A x _64071) -> @IN B (f x) _64072) /\ (forall x : A, forall y : A, ((@IN A x _64071) /\ ((@IN A y _64071) /\ ((f x) = (f y)))) -> x = y).
Lemma le_c_def {A B : Type'} : (@le_c A B) = (fun _64071 : A -> Prop => fun _64072 : B -> Prop => exists f : A -> B, (forall x : A, (@IN A x _64071) -> @IN B (f x) _64072) /\ (forall x : A, forall y : A, ((@IN A x _64071) /\ ((@IN A y _64071) /\ ((f x) = (f y)))) -> x = y)).
Proof. exact (eq_refl (@le_c A B)). Qed.
Definition lt_c {A B : Type'} : (A -> Prop) -> (B -> Prop) -> Prop := fun _64083 : A -> Prop => fun _64084 : B -> Prop => (@le_c A B _64083 _64084) /\ (~ (@le_c B A _64084 _64083)).
Lemma lt_c_def {A B : Type'} : (@lt_c A B) = (fun _64083 : A -> Prop => fun _64084 : B -> Prop => (@le_c A B _64083 _64084) /\ (~ (@le_c B A _64084 _64083))).
Proof. exact (eq_refl (@lt_c A B)). Qed.
Definition eq_c {A B : Type'} : (A -> Prop) -> (B -> Prop) -> Prop := fun _64095 : A -> Prop => fun _64096 : B -> Prop => exists f : A -> B, (forall x : A, (@IN A x _64095) -> @IN B (f x) _64096) /\ (forall y : B, (@IN B y _64096) -> @ex1 A (fun x : A => (@IN A x _64095) /\ ((f x) = y))).
Lemma eq_c_def {A B : Type'} : (@eq_c A B) = (fun _64095 : A -> Prop => fun _64096 : B -> Prop => exists f : A -> B, (forall x : A, (@IN A x _64095) -> @IN B (f x) _64096) /\ (forall y : B, (@IN B y _64096) -> @ex1 A (fun x : A => (@IN A x _64095) /\ ((f x) = y)))).
Proof. exact (eq_refl (@eq_c A B)). Qed.
Definition ge_c {A B : Type'} : (A -> Prop) -> (B -> Prop) -> Prop := fun _64107 : A -> Prop => fun _64108 : B -> Prop => @le_c B A _64108 _64107.
Lemma ge_c_def {A B : Type'} : (@ge_c A B) = (fun _64107 : A -> Prop => fun _64108 : B -> Prop => @le_c B A _64108 _64107).
Proof. exact (eq_refl (@ge_c A B)). Qed.
Definition gt_c {A B : Type'} : (A -> Prop) -> (B -> Prop) -> Prop := fun _64119 : A -> Prop => fun _64120 : B -> Prop => @lt_c B A _64120 _64119.
Lemma gt_c_def {A B : Type'} : (@gt_c A B) = (fun _64119 : A -> Prop => fun _64120 : B -> Prop => @lt_c B A _64120 _64119).
Proof. exact (eq_refl (@gt_c A B)). Qed.
Definition COUNTABLE {A : Type'} : (A -> Prop) -> Prop := fun _64270 : A -> Prop => @ge_c nat A (@UNIV nat) _64270.
Lemma COUNTABLE_def {A : Type'} : (@COUNTABLE A) = (fun _64270 : A -> Prop => @ge_c nat A (@UNIV nat) _64270).
Proof. exact (eq_refl (@COUNTABLE A)). Qed.
Definition sup : (R -> Prop) -> R := fun _64275 : R -> Prop => @ε R (fun a : R => (forall x : R, (@IN R x _64275) -> Rle x a) /\ (forall b : R, (forall x : R, (@IN R x _64275) -> Rle x b) -> Rle a b)).
Lemma sup_def : sup = (fun _64275 : R -> Prop => @ε R (fun a : R => (forall x : R, (@IN R x _64275) -> Rle x a) /\ (forall b : R, (forall x : R, (@IN R x _64275) -> Rle x b) -> Rle a b))).
Proof. exact (eq_refl sup). Qed.
Definition inf : (R -> Prop) -> R := fun _65134 : R -> Prop => @ε R (fun a : R => (forall x : R, (@IN R x _65134) -> Rle a x) /\ (forall b : R, (forall x : R, (@IN R x _65134) -> Rle b x) -> Rle b a)).
Lemma inf_def : inf = (fun _65134 : R -> Prop => @ε R (fun a : R => (forall x : R, (@IN R x _65134) -> Rle a x) /\ (forall b : R, (forall x : R, (@IN R x _65134) -> Rle b x) -> Rle b a))).
Proof. exact (eq_refl inf). Qed.
Definition has_inf : (R -> Prop) -> R -> Prop := fun _66484 : R -> Prop => fun _66485 : R => forall c : R, (forall x : R, (@IN R x _66484) -> Rle c x) = (Rle c _66485).
Lemma has_inf_def : has_inf = (fun _66484 : R -> Prop => fun _66485 : R => forall c : R, (forall x : R, (@IN R x _66484) -> Rle c x) = (Rle c _66485)).
Proof. exact (eq_refl has_inf). Qed.
Definition has_sup : (R -> Prop) -> R -> Prop := fun _66496 : R -> Prop => fun _66497 : R => forall c : R, (forall x : R, (@IN R x _66496) -> Rle x c) = (Rle _66497 c).
Lemma has_sup_def : has_sup = (fun _66496 : R -> Prop => fun _66497 : R => forall c : R, (forall x : R, (@IN R x _66496) -> Rle x c) = (Rle _66497 c)).
Proof. exact (eq_refl has_sup). Qed.
Definition dotdot : nat -> nat -> nat -> Prop := fun _66922 : nat => fun _66923 : nat => @GSPEC nat (fun GEN_PVAR_231 : nat => exists x : nat, @SETSPEC nat GEN_PVAR_231 ((Peano.le _66922 x) /\ (Peano.le x _66923)) x).
Lemma dotdot_def : dotdot = (fun _66922 : nat => fun _66923 : nat => @GSPEC nat (fun GEN_PVAR_231 : nat => exists x : nat, @SETSPEC nat GEN_PVAR_231 ((Peano.le _66922 x) /\ (Peano.le x _66923)) x)).
Proof. exact (eq_refl dotdot). Qed.
Definition neutral {A : Type'} : (A -> A -> A) -> A := fun _68834 : A -> A -> A => @ε A (fun x : A => forall y : A, ((_68834 x y) = y) /\ ((_68834 y x) = y)).
Lemma neutral_def {A : Type'} : (@neutral A) = (fun _68834 : A -> A -> A => @ε A (fun x : A => forall y : A, ((_68834 x y) = y) /\ ((_68834 y x) = y))).
Proof. exact (eq_refl (@neutral A)). Qed.
Definition monoidal {A : Type'} : (A -> A -> A) -> Prop := fun _68839 : A -> A -> A => (forall x : A, forall y : A, (_68839 x y) = (_68839 y x)) /\ ((forall x : A, forall y : A, forall z : A, (_68839 x (_68839 y z)) = (_68839 (_68839 x y) z)) /\ (forall x : A, (_68839 (@neutral A _68839) x) = x)).
Lemma monoidal_def {A : Type'} : (@monoidal A) = (fun _68839 : A -> A -> A => (forall x : A, forall y : A, (_68839 x y) = (_68839 y x)) /\ ((forall x : A, forall y : A, forall z : A, (_68839 x (_68839 y z)) = (_68839 (_68839 x y) z)) /\ (forall x : A, (_68839 (@neutral A _68839) x) = x))).
Proof. exact (eq_refl (@monoidal A)). Qed.
Definition support {A B : Type'} : (B -> B -> B) -> (A -> B) -> (A -> Prop) -> A -> Prop := fun _68924 : B -> B -> B => fun _68925 : A -> B => fun _68926 : A -> Prop => @GSPEC A (fun GEN_PVAR_239 : A => exists x : A, @SETSPEC A GEN_PVAR_239 ((@IN A x _68926) /\ (~ ((_68925 x) = (@neutral B _68924)))) x).
Lemma support_def {A B : Type'} : (@support A B) = (fun _68924 : B -> B -> B => fun _68925 : A -> B => fun _68926 : A -> Prop => @GSPEC A (fun GEN_PVAR_239 : A => exists x : A, @SETSPEC A GEN_PVAR_239 ((@IN A x _68926) /\ (~ ((_68925 x) = (@neutral B _68924)))) x)).
Proof. exact (eq_refl (@support A B)). Qed.
Definition iterate {A B : Type'} : (B -> B -> B) -> (A -> Prop) -> (A -> B) -> B := fun _68945 : B -> B -> B => fun _68946 : A -> Prop => fun _68947 : A -> B => @COND B (@FINITE A (@support A B _68945 _68947 _68946)) (@ITSET A B (fun x : A => fun a : B => _68945 (_68947 x) a) (@support A B _68945 _68947 _68946) (@neutral B _68945)) (@neutral B _68945).
Lemma iterate_def {A B : Type'} : (@iterate A B) = (fun _68945 : B -> B -> B => fun _68946 : A -> Prop => fun _68947 : A -> B => @COND B (@FINITE A (@support A B _68945 _68947 _68946)) (@ITSET A B (fun x : A => fun a : B => _68945 (_68947 x) a) (@support A B _68945 _68947 _68946) (@neutral B _68945)) (@neutral B _68945)).
Proof. exact (eq_refl (@iterate A B)). Qed.
Definition iterato {A K : Type'} : (A -> Prop) -> A -> (A -> A -> A) -> (K -> K -> Prop) -> (K -> Prop) -> (K -> A) -> A := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (A -> Prop) -> A -> (A -> A -> A) -> (K -> K -> Prop) -> (K -> Prop) -> (K -> A) -> A) (fun itty : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (A -> Prop) -> A -> (A -> A -> A) -> (K -> K -> Prop) -> (K -> Prop) -> (K -> A) -> A => forall _76701 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))), forall dom : A -> Prop, forall neut : A, forall op : A -> A -> A, forall ltle : K -> K -> Prop, forall k : K -> Prop, forall f : K -> A, (itty _76701 dom neut op ltle k f) = (@COND A ((@FINITE K (@GSPEC K (fun GEN_PVAR_265 : K => exists i : K, @SETSPEC K GEN_PVAR_265 ((@IN K i k) /\ (@IN A (f i) (@DIFF A dom (@INSERT A neut (@EMPTY A))))) i))) /\ (~ ((@GSPEC K (fun GEN_PVAR_266 : K => exists i : K, @SETSPEC K GEN_PVAR_266 ((@IN K i k) /\ (@IN A (f i) (@DIFF A dom (@INSERT A neut (@EMPTY A))))) i)) = (@EMPTY K)))) (@LET K A (fun i : K => @LET_END A (op (f i) (itty _76701 dom neut op ltle (@GSPEC K (fun GEN_PVAR_267 : K => exists j : K, @SETSPEC K GEN_PVAR_267 ((@IN K j (@DELETE K k i)) /\ (@IN A (f j) (@DIFF A dom (@INSERT A neut (@EMPTY A))))) j)) f))) (@COND K (exists i : K, (@IN K i k) /\ ((@IN A (f i) (@DIFF A dom (@INSERT A neut (@EMPTY A)))) /\ (forall j : K, ((ltle j i) /\ ((@IN K j k) /\ (@IN A (f j) (@DIFF A dom (@INSERT A neut (@EMPTY A)))))) -> j = i))) (@ε K (fun i : K => (@IN K i k) /\ ((@IN A (f i) (@DIFF A dom (@INSERT A neut (@EMPTY A)))) /\ (forall j : K, ((ltle j i) /\ ((@IN K j k) /\ (@IN A (f j) (@DIFF A dom (@INSERT A neut (@EMPTY A)))))) -> j = i)))) (@ε K (fun i : K => (@IN K i k) /\ (@IN A (f i) (@DIFF A dom (@INSERT A neut (@EMPTY A)))))))) neut)) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))))))))).
Lemma iterato_def {A K : Type'} : (@iterato A K) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (A -> Prop) -> A -> (A -> A -> A) -> (K -> K -> Prop) -> (K -> Prop) -> (K -> A) -> A) (fun itty : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (A -> Prop) -> A -> (A -> A -> A) -> (K -> K -> Prop) -> (K -> Prop) -> (K -> A) -> A => forall _76701 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))), forall dom : A -> Prop, forall neut : A, forall op : A -> A -> A, forall ltle : K -> K -> Prop, forall k : K -> Prop, forall f : K -> A, (itty _76701 dom neut op ltle k f) = (@COND A ((@FINITE K (@GSPEC K (fun GEN_PVAR_265 : K => exists i : K, @SETSPEC K GEN_PVAR_265 ((@IN K i k) /\ (@IN A (f i) (@DIFF A dom (@INSERT A neut (@EMPTY A))))) i))) /\ (~ ((@GSPEC K (fun GEN_PVAR_266 : K => exists i : K, @SETSPEC K GEN_PVAR_266 ((@IN K i k) /\ (@IN A (f i) (@DIFF A dom (@INSERT A neut (@EMPTY A))))) i)) = (@EMPTY K)))) (@LET K A (fun i : K => @LET_END A (op (f i) (itty _76701 dom neut op ltle (@GSPEC K (fun GEN_PVAR_267 : K => exists j : K, @SETSPEC K GEN_PVAR_267 ((@IN K j (@DELETE K k i)) /\ (@IN A (f j) (@DIFF A dom (@INSERT A neut (@EMPTY A))))) j)) f))) (@COND K (exists i : K, (@IN K i k) /\ ((@IN A (f i) (@DIFF A dom (@INSERT A neut (@EMPTY A)))) /\ (forall j : K, ((ltle j i) /\ ((@IN K j k) /\ (@IN A (f j) (@DIFF A dom (@INSERT A neut (@EMPTY A)))))) -> j = i))) (@ε K (fun i : K => (@IN K i k) /\ ((@IN A (f i) (@DIFF A dom (@INSERT A neut (@EMPTY A)))) /\ (forall j : K, ((ltle j i) /\ ((@IN K j k) /\ (@IN A (f j) (@DIFF A dom (@INSERT A neut (@EMPTY A)))))) -> j = i)))) (@ε K (fun i : K => (@IN K i k) /\ (@IN A (f i) (@DIFF A dom (@INSERT A neut (@EMPTY A)))))))) neut)) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 0))))))))))))))).
Proof. exact (eq_refl (@iterato A K)). Qed.
Definition nproduct {A : Type'} : (A -> Prop) -> (A -> nat) -> nat := @iterate A nat Nat.mul.
Lemma nproduct_def {A : Type'} : (@nproduct A) = (@iterate A nat Nat.mul).
Proof. exact (eq_refl (@nproduct A)). Qed.
Definition iproduct {A : Type'} : (A -> Prop) -> (A -> Z) -> Z := @iterate A Z int_mul.
Lemma iproduct_def {A : Type'} : (@iproduct A) = (@iterate A Z int_mul).
Proof. exact (eq_refl (@iproduct A)). Qed.
Definition product {A : Type'} : (A -> Prop) -> (A -> R) -> R := @iterate A R Rmult.
Lemma product_def {A : Type'} : (@product A) = (@iterate A R Rmult).
Proof. exact (eq_refl (@product A)). Qed.
Definition isum {A : Type'} : (A -> Prop) -> (A -> Z) -> Z := @iterate A Z int_add.
Lemma isum_def {A : Type'} : (@isum A) = (@iterate A Z int_add).
Proof. exact (eq_refl (@isum A)). Qed.
Definition nsum {A : Type'} : (A -> Prop) -> (A -> nat) -> nat := @iterate A nat Nat.add.
Lemma nsum_def {A : Type'} : (@nsum A) = (@iterate A nat Nat.add).
Proof. exact (eq_refl (@nsum A)). Qed.
Definition sum {A : Type'} : (A -> Prop) -> (A -> R) -> R := @iterate A R Rplus.
Lemma sum_def {A : Type'} : (@sum A) = (@iterate A R Rplus).
Proof. exact (eq_refl (@sum A)). Qed.
Definition polynomial_function : (R -> R) -> Prop := fun _94114 : R -> R => exists m : nat, exists c : nat -> R, forall x : R, (_94114 x) = (@sum nat (dotdot (NUMERAL 0) m) (fun i : nat => Rmult (c i) (Rpower_nat x i))).
Lemma polynomial_function_def : polynomial_function = (fun _94114 : R -> R => exists m : nat, exists c : nat -> R, forall x : R, (_94114 x) = (@sum nat (dotdot (NUMERAL 0) m) (fun i : nat => Rmult (c i) (Rpower_nat x i)))).
Proof. exact (eq_refl polynomial_function). Qed.
Definition dimindex {A : Type'} : (A -> Prop) -> nat := fun _94156 : A -> Prop => @COND nat (@FINITE A (@UNIV A)) (@CARD A (@UNIV A)) (NUMERAL (BIT1 0)).
Lemma dimindex_def {A : Type'} : (@dimindex A) = (fun _94156 : A -> Prop => @COND nat (@FINITE A (@UNIV A)) (@CARD A (@UNIV A)) (NUMERAL (BIT1 0))).
Proof. exact (eq_refl (@dimindex A)). Qed.
Definition dollar {A N : Type'} : (cart A N) -> nat -> A := fun _94566 : cart A N => fun _94567 : nat => @dest_cart A N _94566 (@finite_index N _94567).
Lemma dollar_def {A N : Type'} : (@dollar A N) = (fun _94566 : cart A N => fun _94567 : nat => @dest_cart A N _94566 (@finite_index N _94567)).
Proof. exact (eq_refl (@dollar A N)). Qed.
Definition lambda {A B : Type'} : (nat -> A) -> cart A B := fun _94602 : nat -> A => @ε (cart A B) (fun f : cart A B => forall i : nat, ((Peano.le (NUMERAL (BIT1 0)) i) /\ (Peano.le i (@dimindex B (@UNIV B)))) -> (@dollar A B f i) = (_94602 i)).
Lemma lambda_def {A B : Type'} : (@lambda A B) = (fun _94602 : nat -> A => @ε (cart A B) (fun f : cart A B => forall i : nat, ((Peano.le (NUMERAL (BIT1 0)) i) /\ (Peano.le i (@dimindex B (@UNIV B)))) -> (@dollar A B f i) = (_94602 i))).
Proof. exact (eq_refl (@lambda A B)). Qed.
Definition pastecart {A M N : Type'} : (cart A M) -> (cart A N) -> cart A (finite_sum M N) := fun _94893 : cart A M => fun _94894 : cart A N => @lambda A (finite_sum M N) (fun i : nat => @COND A (Peano.le i (@dimindex M (@UNIV M))) (@dollar A M _94893 i) (@dollar A N _94894 (Nat.sub i (@dimindex M (@UNIV M))))).
Lemma pastecart_def {A M N : Type'} : (@pastecart A M N) = (fun _94893 : cart A M => fun _94894 : cart A N => @lambda A (finite_sum M N) (fun i : nat => @COND A (Peano.le i (@dimindex M (@UNIV M))) (@dollar A M _94893 i) (@dollar A N _94894 (Nat.sub i (@dimindex M (@UNIV M)))))).
Proof. exact (eq_refl (@pastecart A M N)). Qed.
Definition fstcart {A M N : Type'} : (cart A (finite_sum M N)) -> cart A M := fun _94905 : cart A (finite_sum M N) => @lambda A M (fun i : nat => @dollar A (finite_sum M N) _94905 i).
Lemma fstcart_def {A M N : Type'} : (@fstcart A M N) = (fun _94905 : cart A (finite_sum M N) => @lambda A M (fun i : nat => @dollar A (finite_sum M N) _94905 i)).
Proof. exact (eq_refl (@fstcart A M N)). Qed.
Definition sndcart {A M N : Type'} : (cart A (finite_sum M N)) -> cart A N := fun _94910 : cart A (finite_sum M N) => @lambda A N (fun i : nat => @dollar A (finite_sum M N) _94910 (Nat.add i (@dimindex M (@UNIV M)))).
Lemma sndcart_def {A M N : Type'} : (@sndcart A M N) = (fun _94910 : cart A (finite_sum M N) => @lambda A N (fun i : nat => @dollar A (finite_sum M N) _94910 (Nat.add i (@dimindex M (@UNIV M))))).
Proof. exact (eq_refl (@sndcart A M N)). Qed.
Definition _100320 {A : Type'} : (finite_sum A A) -> tybit0 A := fun a : finite_sum A A => @_mk_tybit0 A ((fun a' : finite_sum A A => @CONSTR (finite_sum A A) (NUMERAL 0) a' (fun n : nat => @BOTTOM (finite_sum A A))) a).
Lemma _100320_def {A : Type'} : (@_100320 A) = (fun a : finite_sum A A => @_mk_tybit0 A ((fun a' : finite_sum A A => @CONSTR (finite_sum A A) (NUMERAL 0) a' (fun n : nat => @BOTTOM (finite_sum A A))) a)).
Proof. exact (eq_refl (@_100320 A)). Qed.
Definition mktybit0 {A : Type'} : (finite_sum A A) -> tybit0 A := @_100320 A.
Lemma mktybit0_def {A : Type'} : (@mktybit0 A) = (@_100320 A).
Proof. exact (eq_refl (@mktybit0 A)). Qed.
Definition _100339 {A : Type'} : (finite_sum (finite_sum A A) unit) -> tybit1 A := fun a : finite_sum (finite_sum A A) unit => @_mk_tybit1 A ((fun a' : finite_sum (finite_sum A A) unit => @CONSTR (finite_sum (finite_sum A A) unit) (NUMERAL 0) a' (fun n : nat => @BOTTOM (finite_sum (finite_sum A A) unit))) a).
Lemma _100339_def {A : Type'} : (@_100339 A) = (fun a : finite_sum (finite_sum A A) unit => @_mk_tybit1 A ((fun a' : finite_sum (finite_sum A A) unit => @CONSTR (finite_sum (finite_sum A A) unit) (NUMERAL 0) a' (fun n : nat => @BOTTOM (finite_sum (finite_sum A A) unit))) a)).
Proof. exact (eq_refl (@_100339 A)). Qed.
Definition mktybit1 {A : Type'} : (finite_sum (finite_sum A A) unit) -> tybit1 A := @_100339 A.
Lemma mktybit1_def {A : Type'} : (@mktybit1 A) = (@_100339 A).
Proof. exact (eq_refl (@mktybit1 A)). Qed.
Definition vector {A N : Type'} : (list A) -> cart A N := fun _102033 : list A => @lambda A N (fun i : nat => @EL A (Nat.sub i (NUMERAL (BIT1 0))) _102033).
Lemma vector_def {A N : Type'} : (@vector A N) = (fun _102033 : list A => @lambda A N (fun i : nat => @EL A (Nat.sub i (NUMERAL (BIT1 0))) _102033)).
Proof. exact (eq_refl (@vector A N)). Qed.
Definition PCROSS {A M N : Type'} : ((cart A M) -> Prop) -> ((cart A N) -> Prop) -> (cart A (finite_sum M N)) -> Prop := fun _102060 : (cart A M) -> Prop => fun _102061 : (cart A N) -> Prop => @GSPEC (cart A (finite_sum M N)) (fun GEN_PVAR_363 : cart A (finite_sum M N) => exists x : cart A M, exists y : cart A N, @SETSPEC (cart A (finite_sum M N)) GEN_PVAR_363 ((@IN (cart A M) x _102060) /\ (@IN (cart A N) y _102061)) (@pastecart A M N x y)).
Lemma PCROSS_def {A M N : Type'} : (@PCROSS A M N) = (fun _102060 : (cart A M) -> Prop => fun _102061 : (cart A N) -> Prop => @GSPEC (cart A (finite_sum M N)) (fun GEN_PVAR_363 : cart A (finite_sum M N) => exists x : cart A M, exists y : cart A N, @SETSPEC (cart A (finite_sum M N)) GEN_PVAR_363 ((@IN (cart A M) x _102060) /\ (@IN (cart A N) y _102061)) (@pastecart A M N x y))).
Proof. exact (eq_refl (@PCROSS A M N)). Qed.
Definition CASEWISE {_137714 _137750 _137754 _137755 : Type'} : (list (prod (_137750 -> _137754) (_137755 -> _137750 -> _137714))) -> _137755 -> _137754 -> _137714 := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> (list (prod (_137750 -> _137754) (_137755 -> _137750 -> _137714))) -> _137755 -> _137754 -> _137714) (fun CASEWISE' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> (list (prod (_137750 -> _137754) (_137755 -> _137750 -> _137714))) -> _137755 -> _137754 -> _137714 => forall _102665 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))), (forall f : _137755, forall x : _137754, (CASEWISE' _102665 (@nil (prod (_137750 -> _137754) (_137755 -> _137750 -> _137714))) f x) = (@ε _137714 (fun y : _137714 => True))) /\ (forall h : prod (_137750 -> _137754) (_137755 -> _137750 -> _137714), forall t : list (prod (_137750 -> _137754) (_137755 -> _137750 -> _137714)), forall f : _137755, forall x : _137754, (CASEWISE' _102665 (@cons (prod (_137750 -> _137754) (_137755 -> _137750 -> _137714)) h t) f x) = (@COND _137714 (exists y : _137750, (@fst (_137750 -> _137754) (_137755 -> _137750 -> _137714) h y) = x) (@snd (_137750 -> _137754) (_137755 -> _137750 -> _137714) h f (@ε _137750 (fun y : _137750 => (@fst (_137750 -> _137754) (_137755 -> _137750 -> _137714) h y) = x))) (CASEWISE' _102665 t f x)))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0))))))))))))))).
Lemma CASEWISE_def {_137714 _137750 _137754 _137755 : Type'} : (@CASEWISE _137714 _137750 _137754 _137755) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> (list (prod (_137750 -> _137754) (_137755 -> _137750 -> _137714))) -> _137755 -> _137754 -> _137714) (fun CASEWISE' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> (list (prod (_137750 -> _137754) (_137755 -> _137750 -> _137714))) -> _137755 -> _137754 -> _137714 => forall _102665 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))), (forall f : _137755, forall x : _137754, (CASEWISE' _102665 (@nil (prod (_137750 -> _137754) (_137755 -> _137750 -> _137714))) f x) = (@ε _137714 (fun y : _137714 => True))) /\ (forall h : prod (_137750 -> _137754) (_137755 -> _137750 -> _137714), forall t : list (prod (_137750 -> _137754) (_137755 -> _137750 -> _137714)), forall f : _137755, forall x : _137754, (CASEWISE' _102665 (@cons (prod (_137750 -> _137754) (_137755 -> _137750 -> _137714)) h t) f x) = (@COND _137714 (exists y : _137750, (@fst (_137750 -> _137754) (_137755 -> _137750 -> _137714) h y) = x) (@snd (_137750 -> _137754) (_137755 -> _137750 -> _137714) h f (@ε _137750 (fun y : _137750 => (@fst (_137750 -> _137754) (_137755 -> _137750 -> _137714) h y) = x))) (CASEWISE' _102665 t f x)))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))))))))))).
Proof. exact (eq_refl (@CASEWISE _137714 _137750 _137754 _137755)). Qed.
Definition admissible {_138045 _138048 _138052 _138053 _138058 : Type'} : (_138052 -> _138045 -> Prop) -> ((_138052 -> _138048) -> _138058 -> Prop) -> (_138058 -> _138045) -> ((_138052 -> _138048) -> _138058 -> _138053) -> Prop := fun _103732 : _138052 -> _138045 -> Prop => fun _103733 : (_138052 -> _138048) -> _138058 -> Prop => fun _103734 : _138058 -> _138045 => fun _103735 : (_138052 -> _138048) -> _138058 -> _138053 => forall f : _138052 -> _138048, forall g : _138052 -> _138048, forall a : _138058, ((_103733 f a) /\ ((_103733 g a) /\ (forall z : _138052, (_103732 z (_103734 a)) -> (f z) = (g z)))) -> (_103735 f a) = (_103735 g a).
Lemma admissible_def {_138045 _138048 _138052 _138053 _138058 : Type'} : (@admissible _138045 _138048 _138052 _138053 _138058) = (fun _103732 : _138052 -> _138045 -> Prop => fun _103733 : (_138052 -> _138048) -> _138058 -> Prop => fun _103734 : _138058 -> _138045 => fun _103735 : (_138052 -> _138048) -> _138058 -> _138053 => forall f : _138052 -> _138048, forall g : _138052 -> _138048, forall a : _138058, ((_103733 f a) /\ ((_103733 g a) /\ (forall z : _138052, (_103732 z (_103734 a)) -> (f z) = (g z)))) -> (_103735 f a) = (_103735 g a)).
Proof. exact (eq_refl (@admissible _138045 _138048 _138052 _138053 _138058)). Qed.
Definition tailadmissible {A B P : Type'} : (A -> A -> Prop) -> ((A -> B) -> P -> Prop) -> (P -> A) -> ((A -> B) -> P -> B) -> Prop := fun _103764 : A -> A -> Prop => fun _103765 : (A -> B) -> P -> Prop => fun _103766 : P -> A => fun _103767 : (A -> B) -> P -> B => exists P' : (A -> B) -> P -> Prop, exists G : (A -> B) -> P -> A, exists H : (A -> B) -> P -> B, (forall f : A -> B, forall a : P, forall y : A, ((P' f a) /\ (_103764 y (G f a))) -> _103764 y (_103766 a)) /\ ((forall f : A -> B, forall g : A -> B, forall a : P, (forall z : A, (_103764 z (_103766 a)) -> (f z) = (g z)) -> ((P' f a) = (P' g a)) /\ (((G f a) = (G g a)) /\ ((H f a) = (H g a)))) /\ (forall f : A -> B, forall a : P, (_103765 f a) -> (_103767 f a) = (@COND B (P' f a) (f (G f a)) (H f a)))).
Lemma tailadmissible_def {A B P : Type'} : (@tailadmissible A B P) = (fun _103764 : A -> A -> Prop => fun _103765 : (A -> B) -> P -> Prop => fun _103766 : P -> A => fun _103767 : (A -> B) -> P -> B => exists P' : (A -> B) -> P -> Prop, exists G : (A -> B) -> P -> A, exists H : (A -> B) -> P -> B, (forall f : A -> B, forall a : P, forall y : A, ((P' f a) /\ (_103764 y (G f a))) -> _103764 y (_103766 a)) /\ ((forall f : A -> B, forall g : A -> B, forall a : P, (forall z : A, (_103764 z (_103766 a)) -> (f z) = (g z)) -> ((P' f a) = (P' g a)) /\ (((G f a) = (G g a)) /\ ((H f a) = (H g a)))) /\ (forall f : A -> B, forall a : P, (_103765 f a) -> (_103767 f a) = (@COND B (P' f a) (f (G f a)) (H f a))))).
Proof. exact (eq_refl (@tailadmissible A B P)). Qed.
Definition superadmissible {_138202 _138204 _138210 : Type'} : (_138202 -> _138202 -> Prop) -> ((_138202 -> _138204) -> _138210 -> Prop) -> (_138210 -> _138202) -> ((_138202 -> _138204) -> _138210 -> _138204) -> Prop := fun _103796 : _138202 -> _138202 -> Prop => fun _103797 : (_138202 -> _138204) -> _138210 -> Prop => fun _103798 : _138210 -> _138202 => fun _103799 : (_138202 -> _138204) -> _138210 -> _138204 => (@admissible _138202 _138204 _138202 Prop _138210 _103796 (fun f : _138202 -> _138204 => fun a : _138210 => True) _103798 _103797) -> @tailadmissible _138202 _138204 _138210 _103796 _103797 _103798 _103799.
Lemma superadmissible_def {_138202 _138204 _138210 : Type'} : (@superadmissible _138202 _138204 _138210) = (fun _103796 : _138202 -> _138202 -> Prop => fun _103797 : (_138202 -> _138204) -> _138210 -> Prop => fun _103798 : _138210 -> _138202 => fun _103799 : (_138202 -> _138204) -> _138210 -> _138204 => (@admissible _138202 _138204 _138202 Prop _138210 _103796 (fun f : _138202 -> _138204 => fun a : _138210 => True) _103798 _103797) -> @tailadmissible _138202 _138204 _138210 _103796 _103797 _103798 _103799).
Proof. exact (eq_refl (@superadmissible _138202 _138204 _138210)). Qed.