-
Notifications
You must be signed in to change notification settings - Fork 1
/
terms.v
261 lines (261 loc) · 61.8 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
Require Import HOLLight_Real.
Require Import 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 {_4611 _4614 : Type'} : (_4614 -> _4611 -> Prop) -> (_4614 -> _4611 -> Prop) -> _4614 -> _4611 -> Prop := fun r : _4614 -> _4611 -> Prop => fun s : _4614 -> _4611 -> Prop => fun x : _4614 => @COND (_4611 -> Prop) (exists y : _4611, r x y) (r x) (s x).
Lemma _SEQPATTERN_def {_4611 _4614 : Type'} : (@_SEQPATTERN _4611 _4614) = (fun r : _4614 -> _4611 -> Prop => fun s : _4614 -> _4611 -> Prop => fun x : _4614 => @COND (_4611 -> Prop) (exists y : _4611, r x y) (r x) (s x)).
Proof. exact (eq_refl (@_SEQPATTERN _4611 _4614)). 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 {_4656 _4660 : Type'} : _4656 -> (_4656 -> _4660 -> Prop) -> _4660 := fun e : _4656 => fun r : _4656 -> _4660 -> Prop => @COND _4660 (@ex1 _4660 (r e)) (@ε _4660 (r e)) (@ε _4660 (fun z : _4660 => False)).
Lemma _MATCH_def {_4656 _4660 : Type'} : (@_MATCH _4656 _4660) = (fun e : _4656 => fun r : _4656 -> _4660 -> Prop => @COND _4660 (@ex1 _4660 (r e)) (@ε _4660 (r e)) (@ε _4660 (fun z : _4660 => False))).
Proof. exact (eq_refl (@_MATCH _4656 _4660)). Qed.
Definition _FUNCTION {_4678 _4682 : Type'} : (_4678 -> _4682 -> Prop) -> _4678 -> _4682 := fun r : _4678 -> _4682 -> Prop => fun x : _4678 => @COND _4682 (@ex1 _4682 (r x)) (@ε _4682 (r x)) (@ε _4682 (fun z : _4682 => False)).
Lemma _FUNCTION_def {_4678 _4682 : Type'} : (@_FUNCTION _4678 _4682) = (fun r : _4678 -> _4682 -> Prop => fun x : _4678 => @COND _4682 (@ex1 _4682 (r x)) (@ε _4682 (r x)) (@ε _4682 (fun z : _4682 => False))).
Proof. exact (eq_refl (@_FUNCTION _4678 _4682)). 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 _6373 : nat -> Prop => @ε nat (fun n : nat => (_6373 n) /\ (forall m : nat, (Peano.lt m n) -> ~ (_6373 m))).
Lemma minimal_def : minimal = (fun _6373 : nat -> Prop => @ε nat (fun n : nat => (_6373 n) /\ (forall m : nat, (Peano.lt m n) -> ~ (_6373 m)))).
Proof. exact (eq_refl minimal). Qed.
Definition WF {A : Type'} : (A -> A -> Prop) -> Prop := fun _6760 : A -> A -> Prop => forall P : A -> Prop, (exists x : A, P x) -> exists x : A, (P x) /\ (forall y : A, (_6760 y x) -> ~ (P y)).
Lemma WF_def {A : Type'} : (@WF A) = (fun _6760 : A -> A -> Prop => forall P : A -> Prop, (exists x : A, P x) -> exists x : A, (P x) /\ (forall y : A, (_6760 y x) -> ~ (P y))).
Proof. exact (eq_refl (@WF A)). Qed.
Definition MEASURE {_16406 : Type'} : (_16406 -> nat) -> _16406 -> _16406 -> Prop := fun _7931 : _16406 -> nat => fun x : _16406 => fun y : _16406 => Peano.lt (_7931 x) (_7931 y).
Lemma MEASURE_def {_16406 : Type'} : (@MEASURE _16406) = (fun _7931 : _16406 -> nat => fun x : _16406 => fun y : _16406 => Peano.lt (_7931 x) (_7931 y)).
Proof. exact (eq_refl (@MEASURE _16406)). Qed.
Definition NUMPAIR : nat -> nat -> nat := fun _17324 : nat => fun _17325 : nat => Nat.mul (Nat.pow (NUMERAL (BIT0 (BIT1 0))) _17324) (Nat.add (Nat.mul (NUMERAL (BIT0 (BIT1 0))) _17325) (NUMERAL (BIT1 0))).
Lemma NUMPAIR_def : NUMPAIR = (fun _17324 : nat => fun _17325 : nat => Nat.mul (Nat.pow (NUMERAL (BIT0 (BIT1 0))) _17324) (Nat.add (Nat.mul (NUMERAL (BIT0 (BIT1 0))) _17325) (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 _17340 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), exists Y : nat -> nat, forall x : nat, forall y : nat, ((X _17340 (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 _17340 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), exists Y : nat -> nat, forall x : nat, forall y : nat, ((X _17340 (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 _17341 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), forall x : nat, forall y : nat, ((NUMFST (NUMPAIR x y)) = x) /\ ((Y _17341 (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 _17341 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), forall x : nat, forall y : nat, ((NUMFST (NUMPAIR x y)) = x) /\ ((Y _17341 (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 _17342 : Prop => fun _17343 : nat => @COND nat _17342 (S (Nat.mul (NUMERAL (BIT0 (BIT1 0))) _17343)) (Nat.mul (NUMERAL (BIT0 (BIT1 0))) _17343).
Lemma NUMSUM_def : NUMSUM = (fun _17342 : Prop => fun _17343 : nat => @COND nat _17342 (S (Nat.mul (NUMERAL (BIT0 (BIT1 0))) _17343)) (Nat.mul (NUMERAL (BIT0 (BIT1 0))) _17343)).
Proof. exact (eq_refl NUMSUM). Qed.
Definition INJN {A : Type'} : nat -> nat -> A -> Prop := fun _17374 : nat => fun n : nat => fun a : A => n = _17374.
Lemma INJN_def {A : Type'} : (@INJN A) = (fun _17374 : nat => fun n : nat => fun a : A => n = _17374).
Proof. exact (eq_refl (@INJN A)). Qed.
Definition INJA {A : Type'} : A -> nat -> A -> Prop := fun _17379 : A => fun n : nat => fun b : A => b = _17379.
Lemma INJA_def {A : Type'} : (@INJA A) = (fun _17379 : A => fun n : nat => fun b : A => b = _17379).
Proof. exact (eq_refl (@INJA A)). Qed.
Definition INJF {A : Type'} : (nat -> nat -> A -> Prop) -> nat -> A -> Prop := fun _17386 : nat -> nat -> A -> Prop => fun n : nat => _17386 (NUMFST n) (NUMSND n).
Lemma INJF_def {A : Type'} : (@INJF A) = (fun _17386 : nat -> nat -> A -> Prop => fun n : nat => _17386 (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 _17391 : nat -> A -> Prop => fun _17392 : nat -> A -> Prop => fun n : nat => fun a : A => @COND Prop (NUMLEFT n) (_17391 (NUMRIGHT n) a) (_17392 (NUMRIGHT n) a).
Lemma INJP_def {A : Type'} : (@INJP A) = (fun _17391 : nat -> A -> Prop => fun _17392 : nat -> A -> Prop => fun n : nat => fun a : A => @COND Prop (NUMLEFT n) (_17391 (NUMRIGHT n) a) (_17392 (NUMRIGHT n) a)).
Proof. exact (eq_refl (@INJP A)). Qed.
Definition ZCONSTR {A : Type'} : nat -> A -> (nat -> nat -> A -> Prop) -> nat -> A -> Prop := fun _17403 : nat => fun _17404 : A => fun _17405 : nat -> nat -> A -> Prop => @INJP A (@INJN A (S _17403)) (@INJP A (@INJA A _17404) (@INJF A _17405)).
Lemma ZCONSTR_def {A : Type'} : (@ZCONSTR A) = (fun _17403 : nat => fun _17404 : A => fun _17405 : nat -> nat -> A -> Prop => @INJP A (@INJN A (S _17403)) (@INJP A (@INJA A _17404) (@INJF A _17405))).
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 _17428 : nat => fun _17429 : A => fun _17430 : nat -> recspace A => @_mk_rec A (@ZCONSTR A _17428 _17429 (fun n : nat => @_dest_rec A (_17430 n))).
Lemma CONSTR_def {A : Type'} : (@CONSTR A) = (fun _17428 : nat => fun _17429 : A => fun _17430 : nat -> recspace A => @_mk_rec A (@ZCONSTR A _17428 _17429 (fun n : nat => @_dest_rec A (_17430 n)))).
Proof. exact (eq_refl (@CONSTR A)). Qed.
Definition FNIL {A : Type'} : nat -> A := fun _17461 : nat => @ε A (fun x : A => True).
Lemma FNIL_def {A : Type'} : (@FNIL A) = (fun _17461 : 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 _17486 : prod nat (prod nat (prod nat nat)), forall x : A, (OUTL' _17486 (@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 _17486 : prod nat (prod nat (prod nat nat)), forall x : A, (OUTL' _17486 (@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 _17488 : prod nat (prod nat (prod nat nat)), forall y : B, (OUTR' _17488 (@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 _17488 : prod nat (prod nat (prod nat nat)), forall y : B, (OUTR' _17488 (@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 _17954 : prod nat (prod nat (prod nat nat)), forall h : A, forall t : list A, (LAST' _17954 (@cons A h t)) = (@COND A (t = (@nil A)) h (LAST' _17954 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 _17954 : prod nat (prod nat (prod nat nat)), forall h : A, forall t : list A, (LAST' _17954 (@cons A h t)) = (@COND A (t = (@nil A)) h (LAST' _17954 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 {_25287 : Type'} : (list _25287) -> Prop := @ε ((prod nat (prod nat (prod nat nat))) -> (list _25287) -> Prop) (fun NULL' : (prod nat (prod nat (prod nat nat))) -> (list _25287) -> Prop => forall _17966 : prod nat (prod nat (prod nat nat)), ((NULL' _17966 (@nil _25287)) = True) /\ (forall h : _25287, forall t : list _25287, (NULL' _17966 (@cons _25287 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 {_25287 : Type'} : (@NULL _25287) = (@ε ((prod nat (prod nat (prod nat nat))) -> (list _25287) -> Prop) (fun NULL' : (prod nat (prod nat (prod nat nat))) -> (list _25287) -> Prop => forall _17966 : prod nat (prod nat (prod nat nat)), ((NULL' _17966 (@nil _25287)) = True) /\ (forall h : _25287, forall t : list _25287, (NULL' _17966 (@cons _25287 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 _25287)). Qed.
Definition EX {_25328 : Type'} : (_25328 -> Prop) -> (list _25328) -> Prop := @ε ((prod nat nat) -> (_25328 -> Prop) -> (list _25328) -> Prop) (fun EX' : (prod nat nat) -> (_25328 -> Prop) -> (list _25328) -> Prop => forall _17980 : prod nat nat, (forall P : _25328 -> Prop, (EX' _17980 P (@nil _25328)) = False) /\ (forall h : _25328, forall P : _25328 -> Prop, forall t : list _25328, (EX' _17980 P (@cons _25328 h t)) = ((P h) \/ (EX' _17980 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 {_25328 : Type'} : (@EX _25328) = (@ε ((prod nat nat) -> (_25328 -> Prop) -> (list _25328) -> Prop) (fun EX' : (prod nat nat) -> (_25328 -> Prop) -> (list _25328) -> Prop => forall _17980 : prod nat nat, (forall P : _25328 -> Prop, (EX' _17980 P (@nil _25328)) = False) /\ (forall h : _25328, forall P : _25328 -> Prop, forall t : list _25328, (EX' _17980 P (@cons _25328 h t)) = ((P h) \/ (EX' _17980 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 _25328)). Qed.
Definition ITLIST {_25350 _25351 : Type'} : (_25351 -> _25350 -> _25350) -> (list _25351) -> _25350 -> _25350 := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (_25351 -> _25350 -> _25350) -> (list _25351) -> _25350 -> _25350) (fun ITLIST' : (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (_25351 -> _25350 -> _25350) -> (list _25351) -> _25350 -> _25350 => forall _17988 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), (forall f : _25351 -> _25350 -> _25350, forall b : _25350, (ITLIST' _17988 f (@nil _25351) b) = b) /\ (forall h : _25351, forall f : _25351 -> _25350 -> _25350, forall t : list _25351, forall b : _25350, (ITLIST' _17988 f (@cons _25351 h t) b) = (f h (ITLIST' _17988 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 {_25350 _25351 : Type'} : (@ITLIST _25350 _25351) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (_25351 -> _25350 -> _25350) -> (list _25351) -> _25350 -> _25350) (fun ITLIST' : (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (_25351 -> _25350 -> _25350) -> (list _25351) -> _25350 -> _25350 => forall _17988 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), (forall f : _25351 -> _25350 -> _25350, forall b : _25350, (ITLIST' _17988 f (@nil _25351) b) = b) /\ (forall h : _25351, forall f : _25351 -> _25350 -> _25350, forall t : list _25351, forall b : _25350, (ITLIST' _17988 f (@cons _25351 h t) b) = (f h (ITLIST' _17988 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 _25350 _25351)). Qed.
Definition ALL2 {_25409 _25416 : Type'} : (_25409 -> _25416 -> Prop) -> (list _25409) -> (list _25416) -> Prop := @ε ((prod nat (prod nat (prod nat nat))) -> (_25409 -> _25416 -> Prop) -> (list _25409) -> (list _25416) -> Prop) (fun ALL2' : (prod nat (prod nat (prod nat nat))) -> (_25409 -> _25416 -> Prop) -> (list _25409) -> (list _25416) -> Prop => forall _18003 : prod nat (prod nat (prod nat nat)), (forall P : _25409 -> _25416 -> Prop, forall l2 : list _25416, (ALL2' _18003 P (@nil _25409) l2) = (l2 = (@nil _25416))) /\ (forall h1' : _25409, forall P : _25409 -> _25416 -> Prop, forall t1 : list _25409, forall l2 : list _25416, (ALL2' _18003 P (@cons _25409 h1' t1) l2) = (@COND Prop (l2 = (@nil _25416)) False ((P h1' (@hd _25416 l2)) /\ (ALL2' _18003 P t1 (@tl _25416 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 {_25409 _25416 : Type'} : (@ALL2 _25409 _25416) = (@ε ((prod nat (prod nat (prod nat nat))) -> (_25409 -> _25416 -> Prop) -> (list _25409) -> (list _25416) -> Prop) (fun ALL2' : (prod nat (prod nat (prod nat nat))) -> (_25409 -> _25416 -> Prop) -> (list _25409) -> (list _25416) -> Prop => forall _18003 : prod nat (prod nat (prod nat nat)), (forall P : _25409 -> _25416 -> Prop, forall l2 : list _25416, (ALL2' _18003 P (@nil _25409) l2) = (l2 = (@nil _25416))) /\ (forall h1' : _25409, forall P : _25409 -> _25416 -> Prop, forall t1 : list _25409, forall l2 : list _25416, (ALL2' _18003 P (@cons _25409 h1' t1) l2) = (@COND Prop (l2 = (@nil _25416)) False ((P h1' (@hd _25416 l2)) /\ (ALL2' _18003 P t1 (@tl _25416 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 _25409 _25416)). Qed.
Definition MAP2 {_25498 _25501 _25508 : Type'} : (_25501 -> _25508 -> _25498) -> (list _25501) -> (list _25508) -> list _25498 := @ε ((prod nat (prod nat (prod nat nat))) -> (_25501 -> _25508 -> _25498) -> (list _25501) -> (list _25508) -> list _25498) (fun MAP2' : (prod nat (prod nat (prod nat nat))) -> (_25501 -> _25508 -> _25498) -> (list _25501) -> (list _25508) -> list _25498 => forall _18011 : prod nat (prod nat (prod nat nat)), (forall f : _25501 -> _25508 -> _25498, forall l : list _25508, (MAP2' _18011 f (@nil _25501) l) = (@nil _25498)) /\ (forall h1' : _25501, forall f : _25501 -> _25508 -> _25498, forall t1 : list _25501, forall l : list _25508, (MAP2' _18011 f (@cons _25501 h1' t1) l) = (@cons _25498 (f h1' (@hd _25508 l)) (MAP2' _18011 f t1 (@tl _25508 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 {_25498 _25501 _25508 : Type'} : (@MAP2 _25498 _25501 _25508) = (@ε ((prod nat (prod nat (prod nat nat))) -> (_25501 -> _25508 -> _25498) -> (list _25501) -> (list _25508) -> list _25498) (fun MAP2' : (prod nat (prod nat (prod nat nat))) -> (_25501 -> _25508 -> _25498) -> (list _25501) -> (list _25508) -> list _25498 => forall _18011 : prod nat (prod nat (prod nat nat)), (forall f : _25501 -> _25508 -> _25498, forall l : list _25508, (MAP2' _18011 f (@nil _25501) l) = (@nil _25498)) /\ (forall h1' : _25501, forall f : _25501 -> _25508 -> _25498, forall t1 : list _25501, forall l : list _25508, (MAP2' _18011 f (@cons _25501 h1' t1) l) = (@cons _25498 (f h1' (@hd _25508 l)) (MAP2' _18011 f t1 (@tl _25508 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 _25498 _25501 _25508)). Qed.
Definition EL {_25569 : Type'} : nat -> (list _25569) -> _25569 := @ε ((prod nat nat) -> nat -> (list _25569) -> _25569) (fun EL' : (prod nat nat) -> nat -> (list _25569) -> _25569 => forall _18015 : prod nat nat, (forall l : list _25569, (EL' _18015 (NUMERAL 0) l) = (@hd _25569 l)) /\ (forall n : nat, forall l : list _25569, (EL' _18015 (S n) l) = (EL' _18015 n (@tl _25569 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 {_25569 : Type'} : (@EL _25569) = (@ε ((prod nat nat) -> nat -> (list _25569) -> _25569) (fun EL' : (prod nat nat) -> nat -> (list _25569) -> _25569 => forall _18015 : prod nat nat, (forall l : list _25569, (EL' _18015 (NUMERAL 0) l) = (@hd _25569 l)) /\ (forall n : nat, forall l : list _25569, (EL' _18015 (S n) l) = (EL' _18015 n (@tl _25569 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 _25569)). Qed.
Definition FILTER {_25594 : Type'} : (_25594 -> Prop) -> (list _25594) -> list _25594 := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (_25594 -> Prop) -> (list _25594) -> list _25594) (fun FILTER' : (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (_25594 -> Prop) -> (list _25594) -> list _25594 => forall _18022 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), (forall P : _25594 -> Prop, (FILTER' _18022 P (@nil _25594)) = (@nil _25594)) /\ (forall h : _25594, forall P : _25594 -> Prop, forall t : list _25594, (FILTER' _18022 P (@cons _25594 h t)) = (@COND (list _25594) (P h) (@cons _25594 h (FILTER' _18022 P t)) (FILTER' _18022 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 {_25594 : Type'} : (@FILTER _25594) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (_25594 -> Prop) -> (list _25594) -> list _25594) (fun FILTER' : (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (_25594 -> Prop) -> (list _25594) -> list _25594 => forall _18022 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), (forall P : _25594 -> Prop, (FILTER' _18022 P (@nil _25594)) = (@nil _25594)) /\ (forall h : _25594, forall P : _25594 -> Prop, forall t : list _25594, (FILTER' _18022 P (@cons _25594 h t)) = (@COND (list _25594) (P h) (@cons _25594 h (FILTER' _18022 P t)) (FILTER' _18022 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 _25594)). Qed.
Definition ASSOC {_25617 _25623 : Type'} : _25623 -> (list (prod _25623 _25617)) -> _25617 := @ε ((prod nat (prod nat (prod nat (prod nat nat)))) -> _25623 -> (list (prod _25623 _25617)) -> _25617) (fun ASSOC' : (prod nat (prod nat (prod nat (prod nat nat)))) -> _25623 -> (list (prod _25623 _25617)) -> _25617 => forall _18029 : prod nat (prod nat (prod nat (prod nat nat))), forall h : prod _25623 _25617, forall a : _25623, forall t : list (prod _25623 _25617), (ASSOC' _18029 a (@cons (prod _25623 _25617) h t)) = (@COND _25617 ((@fst _25623 _25617 h) = a) (@snd _25623 _25617 h) (ASSOC' _18029 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 {_25617 _25623 : Type'} : (@ASSOC _25617 _25623) = (@ε ((prod nat (prod nat (prod nat (prod nat nat)))) -> _25623 -> (list (prod _25623 _25617)) -> _25617) (fun ASSOC' : (prod nat (prod nat (prod nat (prod nat nat)))) -> _25623 -> (list (prod _25623 _25617)) -> _25617 => forall _18029 : prod nat (prod nat (prod nat (prod nat nat))), forall h : prod _25623 _25617, forall a : _25623, forall t : list (prod _25623 _25617), (ASSOC' _18029 a (@cons (prod _25623 _25617) h t)) = (@COND _25617 ((@fst _25623 _25617 h) = a) (@snd _25623 _25617 h) (ASSOC' _18029 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 _25617 _25623)). Qed.
Definition ITLIST2 {_25645 _25647 _25655 : Type'} : (_25647 -> _25655 -> _25645 -> _25645) -> (list _25647) -> (list _25655) -> _25645 -> _25645 := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (_25647 -> _25655 -> _25645 -> _25645) -> (list _25647) -> (list _25655) -> _25645 -> _25645) (fun ITLIST2' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (_25647 -> _25655 -> _25645 -> _25645) -> (list _25647) -> (list _25655) -> _25645 -> _25645 => forall _18038 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))), (forall f : _25647 -> _25655 -> _25645 -> _25645, forall l2 : list _25655, forall b : _25645, (ITLIST2' _18038 f (@nil _25647) l2 b) = b) /\ (forall h1' : _25647, forall f : _25647 -> _25655 -> _25645 -> _25645, forall t1 : list _25647, forall l2 : list _25655, forall b : _25645, (ITLIST2' _18038 f (@cons _25647 h1' t1) l2 b) = (f h1' (@hd _25655 l2) (ITLIST2' _18038 f t1 (@tl _25655 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 {_25645 _25647 _25655 : Type'} : (@ITLIST2 _25645 _25647 _25655) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (_25647 -> _25655 -> _25645 -> _25645) -> (list _25647) -> (list _25655) -> _25645 -> _25645) (fun ITLIST2' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (_25647 -> _25655 -> _25645 -> _25645) -> (list _25647) -> (list _25655) -> _25645 -> _25645 => forall _18038 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))), (forall f : _25647 -> _25655 -> _25645 -> _25645, forall l2 : list _25655, forall b : _25645, (ITLIST2' _18038 f (@nil _25647) l2 b) = b) /\ (forall h1' : _25647, forall f : _25647 -> _25655 -> _25645 -> _25645, forall t1 : list _25647, forall l2 : list _25655, forall b : _25645, (ITLIST2' _18038 f (@cons _25647 h1' t1) l2 b) = (f h1' (@hd _25655 l2) (ITLIST2' _18038 f t1 (@tl _25655 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 _25645 _25647 _25655)). Qed.
Definition ZIP {_25719 _25727 : Type'} : (list _25719) -> (list _25727) -> list (prod _25719 _25727) := @ε ((prod nat (prod nat nat)) -> (list _25719) -> (list _25727) -> list (prod _25719 _25727)) (fun ZIP' : (prod nat (prod nat nat)) -> (list _25719) -> (list _25727) -> list (prod _25719 _25727) => forall _18042 : prod nat (prod nat nat), (forall l2 : list _25727, (ZIP' _18042 (@nil _25719) l2) = (@nil (prod _25719 _25727))) /\ (forall h1' : _25719, forall t1 : list _25719, forall l2 : list _25727, (ZIP' _18042 (@cons _25719 h1' t1) l2) = (@cons (prod _25719 _25727) (@pair _25719 _25727 h1' (@hd _25727 l2)) (ZIP' _18042 t1 (@tl _25727 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 {_25719 _25727 : Type'} : (@ZIP _25719 _25727) = (@ε ((prod nat (prod nat nat)) -> (list _25719) -> (list _25727) -> list (prod _25719 _25727)) (fun ZIP' : (prod nat (prod nat nat)) -> (list _25719) -> (list _25727) -> list (prod _25719 _25727) => forall _18042 : prod nat (prod nat nat), (forall l2 : list _25727, (ZIP' _18042 (@nil _25719) l2) = (@nil (prod _25719 _25727))) /\ (forall h1' : _25719, forall t1 : list _25719, forall l2 : list _25727, (ZIP' _18042 (@cons _25719 h1' t1) l2) = (@cons (prod _25719 _25727) (@pair _25719 _25727 h1' (@hd _25727 l2)) (ZIP' _18042 t1 (@tl _25727 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 _25719 _25727)). Qed.
Definition ALLPAIRS {_25786 _25787 : Type'} : (_25787 -> _25786 -> Prop) -> (list _25787) -> (list _25786) -> Prop := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> (_25787 -> _25786 -> Prop) -> (list _25787) -> (list _25786) -> Prop) (fun ALLPAIRS' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> (_25787 -> _25786 -> Prop) -> (list _25787) -> (list _25786) -> Prop => forall _18050 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))), (forall f : _25787 -> _25786 -> Prop, forall l : list _25786, (ALLPAIRS' _18050 f (@nil _25787) l) = True) /\ (forall h : _25787, forall f : _25787 -> _25786 -> Prop, forall t : list _25787, forall l : list _25786, (ALLPAIRS' _18050 f (@cons _25787 h t) l) = ((@List.Forall _25786 (f h) l) /\ (ALLPAIRS' _18050 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 {_25786 _25787 : Type'} : (@ALLPAIRS _25786 _25787) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> (_25787 -> _25786 -> Prop) -> (list _25787) -> (list _25786) -> Prop) (fun ALLPAIRS' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> (_25787 -> _25786 -> Prop) -> (list _25787) -> (list _25786) -> Prop => forall _18050 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))), (forall f : _25787 -> _25786 -> Prop, forall l : list _25786, (ALLPAIRS' _18050 f (@nil _25787) l) = True) /\ (forall h : _25787, forall f : _25787 -> _25786 -> Prop, forall t : list _25787, forall l : list _25786, (ALLPAIRS' _18050 f (@cons _25787 h t) l) = ((@List.Forall _25786 (f h) l) /\ (ALLPAIRS' _18050 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 _25786 _25787)). 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 _18064 : 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' _18064 s (NUMERAL 0)) = (@nil A)) /\ (forall s : nat -> A, forall n : nat, (list_of_seq' _18064 s (S n)) = (@List.app A (list_of_seq' _18064 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 _18064 : 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' _18064 s (NUMERAL 0)) = (@nil A)) /\ (forall s : nat -> A, forall n : nat, (list_of_seq' _18064 s (S n)) = (@List.app A (list_of_seq' _18064 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 _22730 : 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 _22730_def : _22730 = (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 _22730). Qed.
Definition ASCII : Prop -> Prop -> Prop -> Prop -> Prop -> Prop -> Prop -> Prop -> Ascii.ascii := _22730.
Lemma ASCII_def : ASCII = _22730.
Proof. exact (eq_refl ASCII). Qed.
Lemma dist_def : dist = (fun _22820 : prod nat nat => Nat.add (Nat.sub (@fst nat nat _22820) (@snd nat nat _22820)) (Nat.sub (@snd nat nat _22820) (@fst nat nat _22820))).
Proof. exact (eq_refl dist). Qed.
Lemma is_nadd_def : is_nadd = (fun _23130 : nat -> nat => exists B : nat, forall m : nat, forall n : nat, Peano.le (dist (@pair nat nat (Nat.mul m (_23130 n)) (Nat.mul n (_23130 m)))) (Nat.mul B (Nat.add m n))).
Proof. exact (eq_refl is_nadd). Qed.
Lemma nadd_eq_def : nadd_eq = (fun _23149 : nadd => fun _23150 : nadd => exists B : nat, forall n : nat, Peano.le (dist (@pair nat nat (dest_nadd _23149 n) (dest_nadd _23150 n))) B).
Proof. exact (eq_refl nadd_eq). Qed.
Lemma nadd_of_num_def : nadd_of_num = (fun _23161 : nat => mk_nadd (fun n : nat => Nat.mul _23161 n)).
Proof. exact (eq_refl nadd_of_num). Qed.
Lemma nadd_le_def : nadd_le = (fun _23168 : nadd => fun _23169 : nadd => exists B : nat, forall n : nat, Peano.le (dest_nadd _23168 n) (Nat.add (dest_nadd _23169 n) B)).
Proof. exact (eq_refl nadd_le). Qed.
Lemma nadd_add_def : nadd_add = (fun _23184 : nadd => fun _23185 : nadd => mk_nadd (fun n : nat => Nat.add (dest_nadd _23184 n) (dest_nadd _23185 n))).
Proof. exact (eq_refl nadd_add). Qed.
Lemma nadd_mul_def : nadd_mul = (fun _23198 : nadd => fun _23199 : nadd => mk_nadd (fun n : nat => dest_nadd _23198 (dest_nadd _23199 n))).
Proof. exact (eq_refl nadd_mul). Qed.
Lemma nadd_rinv_def : nadd_rinv = (fun _23335 : nadd => fun n : nat => Nat.div (Nat.mul n n) (dest_nadd _23335 n)).
Proof. exact (eq_refl nadd_rinv). Qed.
Lemma nadd_inv_def : nadd_inv = (fun _23349 : nadd => @COND nadd (nadd_eq _23349 (nadd_of_num (NUMERAL 0))) (nadd_of_num (NUMERAL 0)) (mk_nadd (nadd_rinv _23349))).
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 _23594 : nat => @pair hreal hreal (hreal_of_num _23594) (hreal_of_num (NUMERAL 0))).
Proof. exact (eq_refl treal_of_num). Qed.
Lemma treal_neg_def : treal_neg = (fun _23599 : prod hreal hreal => @pair hreal hreal (@snd hreal hreal _23599) (@fst hreal hreal _23599)).
Proof. exact (eq_refl treal_neg). Qed.
Lemma treal_add_def : treal_add = (fun _23608 : prod hreal hreal => fun _23609 : prod hreal hreal => @pair hreal hreal (hreal_add (@fst hreal hreal _23608) (@fst hreal hreal _23609)) (hreal_add (@snd hreal hreal _23608) (@snd hreal hreal _23609))).
Proof. exact (eq_refl treal_add). Qed.
Lemma treal_mul_def : treal_mul = (fun _23630 : prod hreal hreal => fun _23631 : prod hreal hreal => @pair hreal hreal (hreal_add (hreal_mul (@fst hreal hreal _23630) (@fst hreal hreal _23631)) (hreal_mul (@snd hreal hreal _23630) (@snd hreal hreal _23631))) (hreal_add (hreal_mul (@fst hreal hreal _23630) (@snd hreal hreal _23631)) (hreal_mul (@snd hreal hreal _23630) (@fst hreal hreal _23631)))).
Proof. exact (eq_refl treal_mul). Qed.
Lemma treal_le_def : treal_le = (fun _23652 : prod hreal hreal => fun _23653 : prod hreal hreal => hreal_le (hreal_add (@fst hreal hreal _23652) (@snd hreal hreal _23653)) (hreal_add (@fst hreal hreal _23653) (@snd hreal hreal _23652))).
Proof. exact (eq_refl treal_le). Qed.
Lemma treal_inv_def : treal_inv = (fun _23674 : prod hreal hreal => @COND (prod hreal hreal) ((@fst hreal hreal _23674) = (@snd hreal hreal _23674)) (@pair hreal hreal (hreal_of_num (NUMERAL 0)) (hreal_of_num (NUMERAL 0))) (@COND (prod hreal hreal) (hreal_le (@snd hreal hreal _23674) (@fst hreal hreal _23674)) (@pair hreal hreal (hreal_inv (@ε hreal (fun d : hreal => (@fst hreal hreal _23674) = (hreal_add (@snd hreal hreal _23674) d)))) (hreal_of_num (NUMERAL 0))) (@pair hreal hreal (hreal_of_num (NUMERAL 0)) (hreal_inv (@ε hreal (fun d : hreal => (@snd hreal hreal _23674) = (hreal_add (@fst hreal hreal _23674) d))))))).
Proof. exact (eq_refl treal_inv). Qed.
Lemma treal_eq_def : treal_eq = (fun _23683 : prod hreal hreal => fun _23684 : prod hreal hreal => (hreal_add (@fst hreal hreal _23683) (@snd hreal hreal _23684)) = (hreal_add (@fst hreal hreal _23684) (@snd hreal hreal _23683))).
Proof. exact (eq_refl treal_eq). Qed.
Definition real_of_num : nat -> real := fun m : nat => mk_real (fun u : prod hreal hreal => treal_eq (treal_of_num m) u).
Lemma real_of_num_def : real_of_num = (fun m : nat => mk_real (fun u : prod hreal hreal => treal_eq (treal_of_num m) u)).
Proof. exact (eq_refl real_of_num). Qed.
Definition real_neg : real -> real := fun x1 : real => mk_real (fun u : prod hreal hreal => exists x1' : prod hreal hreal, (treal_eq (treal_neg x1') u) /\ (dest_real x1 x1')).
Lemma real_neg_def : real_neg = (fun x1 : real => mk_real (fun u : prod hreal hreal => exists x1' : prod hreal hreal, (treal_eq (treal_neg x1') u) /\ (dest_real x1 x1'))).
Proof. exact (eq_refl real_neg). Qed.
Definition real_add : real -> real -> real := fun x1 : real => fun y1 : real => mk_real (fun u : prod hreal hreal => exists x1' : prod hreal hreal, exists y1' : prod hreal hreal, (treal_eq (treal_add x1' y1') u) /\ ((dest_real x1 x1') /\ (dest_real y1 y1'))).
Lemma real_add_def : real_add = (fun x1 : real => fun y1 : real => mk_real (fun u : prod hreal hreal => exists x1' : prod hreal hreal, exists y1' : prod hreal hreal, (treal_eq (treal_add x1' y1') u) /\ ((dest_real x1 x1') /\ (dest_real y1 y1')))).
Proof. exact (eq_refl real_add). Qed.
Definition real_mul : real -> real -> real := fun x1 : real => fun y1 : real => mk_real (fun u : prod hreal hreal => exists x1' : prod hreal hreal, exists y1' : prod hreal hreal, (treal_eq (treal_mul x1' y1') u) /\ ((dest_real x1 x1') /\ (dest_real y1 y1'))).
Lemma real_mul_def : real_mul = (fun x1 : real => fun y1 : real => mk_real (fun u : prod hreal hreal => exists x1' : prod hreal hreal, exists y1' : prod hreal hreal, (treal_eq (treal_mul x1' y1') u) /\ ((dest_real x1 x1') /\ (dest_real y1 y1')))).
Proof. exact (eq_refl real_mul). Qed.
Definition real_le : real -> real -> Prop := fun x1 : real => fun y1 : real => @ε Prop (fun u : Prop => exists x1' : prod hreal hreal, exists y1' : prod hreal hreal, ((treal_le x1' y1') = u) /\ ((dest_real x1 x1') /\ (dest_real y1 y1'))).
Lemma real_le_def : real_le = (fun x1 : real => fun y1 : real => @ε Prop (fun u : Prop => exists x1' : prod hreal hreal, exists y1' : prod hreal hreal, ((treal_le x1' y1') = u) /\ ((dest_real x1 x1') /\ (dest_real y1 y1')))).
Proof. exact (eq_refl real_le). Qed.
Definition real_inv : real -> real := fun x : real => mk_real (fun u : prod hreal hreal => exists x' : prod hreal hreal, (treal_eq (treal_inv x') u) /\ (dest_real x x')).
Lemma real_inv_def : real_inv = (fun x : real => mk_real (fun u : prod hreal hreal => exists x' : prod hreal hreal, (treal_eq (treal_inv x') u) /\ (dest_real x x'))).
Proof. exact (eq_refl real_inv). Qed.
Definition real_sub : real -> real -> real := fun _23899 : real => fun _23900 : real => real_add _23899 (real_neg _23900).
Lemma real_sub_def : real_sub = (fun _23899 : real => fun _23900 : real => real_add _23899 (real_neg _23900)).
Proof. exact (eq_refl real_sub). Qed.
Definition real_lt : real -> real -> Prop := fun _23911 : real => fun _23912 : real => ~ (real_le _23912 _23911).
Lemma real_lt_def : real_lt = (fun _23911 : real => fun _23912 : real => ~ (real_le _23912 _23911)).
Proof. exact (eq_refl real_lt). Qed.
Definition real_ge : real -> real -> Prop := fun _23923 : real => fun _23924 : real => real_le _23924 _23923.
Lemma real_ge_def : real_ge = (fun _23923 : real => fun _23924 : real => real_le _23924 _23923).
Proof. exact (eq_refl real_ge). Qed.
Definition real_gt : real -> real -> Prop := fun _23935 : real => fun _23936 : real => real_lt _23936 _23935.
Lemma real_gt_def : real_gt = (fun _23935 : real => fun _23936 : real => real_lt _23936 _23935).
Proof. exact (eq_refl real_gt). Qed.
Definition real_abs : real -> real := fun _23947 : real => @COND real (real_le (real_of_num (NUMERAL 0)) _23947) _23947 (real_neg _23947).
Lemma real_abs_def : real_abs = (fun _23947 : real => @COND real (real_le (real_of_num (NUMERAL 0)) _23947) _23947 (real_neg _23947)).
Proof. exact (eq_refl real_abs). Qed.
Definition real_pow : real -> nat -> real := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> real -> nat -> real) (fun real_pow' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> real -> nat -> real => forall _23958 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))), (forall x : real, (real_pow' _23958 x (NUMERAL 0)) = (real_of_num (NUMERAL (BIT1 0)))) /\ (forall x : real, forall n : nat, (real_pow' _23958 x (S n)) = (real_mul x (real_pow' _23958 x n)))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair 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 nat)))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (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 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 (BIT1 0))))))))))))))).
Lemma real_pow_def : real_pow = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> real -> nat -> real) (fun real_pow' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> real -> nat -> real => forall _23958 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))), (forall x : real, (real_pow' _23958 x (NUMERAL 0)) = (real_of_num (NUMERAL (BIT1 0)))) /\ (forall x : real, forall n : nat, (real_pow' _23958 x (S n)) = (real_mul x (real_pow' _23958 x n)))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair 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 nat)))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (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 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT0 (BIT1 (BIT1 (BIT1 0)))))))))))))))).
Proof. exact (eq_refl real_pow). Qed.
Definition real_div : real -> real -> real := fun _23959 : real => fun _23960 : real => real_mul _23959 (real_inv _23960).
Lemma real_div_def : real_div = (fun _23959 : real => fun _23960 : real => real_mul _23959 (real_inv _23960)).
Proof. exact (eq_refl real_div). Qed.
Definition real_max : real -> real -> real := fun _23971 : real => fun _23972 : real => @COND real (real_le _23971 _23972) _23972 _23971.
Lemma real_max_def : real_max = (fun _23971 : real => fun _23972 : real => @COND real (real_le _23971 _23972) _23972 _23971).
Proof. exact (eq_refl real_max). Qed.
Definition real_min : real -> real -> real := fun _23983 : real => fun _23984 : real => @COND real (real_le _23983 _23984) _23983 _23984.
Lemma real_min_def : real_min = (fun _23983 : real => fun _23984 : real => @COND real (real_le _23983 _23984) _23983 _23984).
Proof. exact (eq_refl real_min). Qed.
Definition real_sgn : real -> real := fun _26471 : real => @COND real (real_lt (real_of_num (NUMERAL 0)) _26471) (real_of_num (NUMERAL (BIT1 0))) (@COND real (real_lt _26471 (real_of_num (NUMERAL 0))) (real_neg (real_of_num (NUMERAL (BIT1 0)))) (real_of_num (NUMERAL 0))).
Lemma real_sgn_def : real_sgn = (fun _26471 : real => @COND real (real_lt (real_of_num (NUMERAL 0)) _26471) (real_of_num (NUMERAL (BIT1 0))) (@COND real (real_lt _26471 (real_of_num (NUMERAL 0))) (real_neg (real_of_num (NUMERAL (BIT1 0)))) (real_of_num (NUMERAL 0)))).
Proof. exact (eq_refl real_sgn). Qed.
Definition sqrt : real -> real := fun _27022 : real => @ε real (fun y : real => ((real_sgn y) = (real_sgn _27022)) /\ ((real_pow y (NUMERAL (BIT0 (BIT1 0)))) = (real_abs _27022))).
Lemma sqrt_def : sqrt = (fun _27022 : real => @ε real (fun y : real => ((real_sgn y) = (real_sgn _27022)) /\ ((real_pow y (NUMERAL (BIT0 (BIT1 0)))) = (real_abs _27022)))).
Proof. exact (eq_refl sqrt). Qed.