-
Notifications
You must be signed in to change notification settings - Fork 1
/
terms.v
166 lines (166 loc) · 44 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
Require Import coq.
Require Import theory_hol.
Require Import types.
Definition _FALSITY_ := 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'} := 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'} := fun x : A => x.
Lemma I_def {A : Type'} : (@I A) = (fun x : A => x).
Proof. exact (eq_refl (@I A)). Qed.
Definition hashek := True.
Lemma hashek_def : hashek = True.
Proof. exact (eq_refl hashek). Qed.
Definition LET {A B : Type'} := 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'} := 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'} := 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'} := 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'} := 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 := 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 := 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'} := 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'} := 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'} := 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'} := 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'} := 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 := 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 := 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'} := 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 {_25210 : Type'} := fun _8094 : _25210 -> nat => fun x : _25210 => fun y : _25210 => Peano.lt (_8094 x) (_8094 y).
Lemma MEASURE_def {_25210 : Type'} : (@MEASURE _25210) = (fun _8094 : _25210 -> nat => fun x : _25210 => fun y : _25210 => Peano.lt (_8094 x) (_8094 y)).
Proof. exact (eq_refl (@MEASURE _25210)). Qed.
Definition 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))).
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 := @ε ((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 := @ε ((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 := 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'} := 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'} := 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'} := 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'} := 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'} := 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'} := @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'} := @_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'} := 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'} := 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'} := @ε ((prod nat (prod nat (prod nat nat))) -> (sum A B) -> A) (fun OUTL' : (prod nat (prod nat (prod nat nat))) -> (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))) -> (sum A B) -> A) (fun OUTL' : (prod nat (prod nat (prod nat nat))) -> (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'} := @ε ((prod nat (prod nat (prod nat nat))) -> (sum A B) -> B) (fun OUTR' : (prod nat (prod nat (prod nat nat))) -> (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))) -> (sum A B) -> B) (fun OUTR' : (prod nat (prod nat (prod nat nat))) -> (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'} := @ε ((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 {_34091 : Type'} := @ε ((prod nat (prod nat (prod nat nat))) -> (list _34091) -> Prop) (fun NULL' : (prod nat (prod nat (prod nat nat))) -> (list _34091) -> Prop => forall _18129 : prod nat (prod nat (prod nat nat)), ((NULL' _18129 (@nil _34091)) = True) /\ (forall h : _34091, forall t : list _34091, (NULL' _18129 (@cons _34091 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 {_34091 : Type'} : (@NULL _34091) = (@ε ((prod nat (prod nat (prod nat nat))) -> (list _34091) -> Prop) (fun NULL' : (prod nat (prod nat (prod nat nat))) -> (list _34091) -> Prop => forall _18129 : prod nat (prod nat (prod nat nat)), ((NULL' _18129 (@nil _34091)) = True) /\ (forall h : _34091, forall t : list _34091, (NULL' _18129 (@cons _34091 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 _34091)). Qed.
Definition EX {_34132 : Type'} := @ε ((prod nat nat) -> (_34132 -> Prop) -> (list _34132) -> Prop) (fun EX' : (prod nat nat) -> (_34132 -> Prop) -> (list _34132) -> Prop => forall _18143 : prod nat nat, (forall P : _34132 -> Prop, (EX' _18143 P (@nil _34132)) = False) /\ (forall h : _34132, forall P : _34132 -> Prop, forall t : list _34132, (EX' _18143 P (@cons _34132 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 {_34132 : Type'} : (@EX _34132) = (@ε ((prod nat nat) -> (_34132 -> Prop) -> (list _34132) -> Prop) (fun EX' : (prod nat nat) -> (_34132 -> Prop) -> (list _34132) -> Prop => forall _18143 : prod nat nat, (forall P : _34132 -> Prop, (EX' _18143 P (@nil _34132)) = False) /\ (forall h : _34132, forall P : _34132 -> Prop, forall t : list _34132, (EX' _18143 P (@cons _34132 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 _34132)). Qed.
Definition ALL2 {_34213 _34220 : Type'} := @ε ((prod nat (prod nat (prod nat nat))) -> (_34213 -> _34220 -> Prop) -> (list _34213) -> (list _34220) -> Prop) (fun ALL2' : (prod nat (prod nat (prod nat nat))) -> (_34213 -> _34220 -> Prop) -> (list _34213) -> (list _34220) -> Prop => forall _18166 : prod nat (prod nat (prod nat nat)), (forall P : _34213 -> _34220 -> Prop, forall l2 : list _34220, (ALL2' _18166 P (@nil _34213) l2) = (l2 = (@nil _34220))) /\ (forall h1' : _34213, forall P : _34213 -> _34220 -> Prop, forall t1 : list _34213, forall l2 : list _34220, (ALL2' _18166 P (@cons _34213 h1' t1) l2) = (@COND Prop (l2 = (@nil _34220)) False ((P h1' (@hd _34220 l2)) /\ (ALL2' _18166 P t1 (@tl _34220 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 {_34213 _34220 : Type'} : (@ALL2 _34213 _34220) = (@ε ((prod nat (prod nat (prod nat nat))) -> (_34213 -> _34220 -> Prop) -> (list _34213) -> (list _34220) -> Prop) (fun ALL2' : (prod nat (prod nat (prod nat nat))) -> (_34213 -> _34220 -> Prop) -> (list _34213) -> (list _34220) -> Prop => forall _18166 : prod nat (prod nat (prod nat nat)), (forall P : _34213 -> _34220 -> Prop, forall l2 : list _34220, (ALL2' _18166 P (@nil _34213) l2) = (l2 = (@nil _34220))) /\ (forall h1' : _34213, forall P : _34213 -> _34220 -> Prop, forall t1 : list _34213, forall l2 : list _34220, (ALL2' _18166 P (@cons _34213 h1' t1) l2) = (@COND Prop (l2 = (@nil _34220)) False ((P h1' (@hd _34220 l2)) /\ (ALL2' _18166 P t1 (@tl _34220 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 _34213 _34220)). Qed.
Definition MAP2 {_34302 _34305 _34312 : Type'} := @ε ((prod nat (prod nat (prod nat nat))) -> (_34305 -> _34312 -> _34302) -> (list _34305) -> (list _34312) -> list _34302) (fun MAP2' : (prod nat (prod nat (prod nat nat))) -> (_34305 -> _34312 -> _34302) -> (list _34305) -> (list _34312) -> list _34302 => forall _18174 : prod nat (prod nat (prod nat nat)), (forall f : _34305 -> _34312 -> _34302, forall l : list _34312, (MAP2' _18174 f (@nil _34305) l) = (@nil _34302)) /\ (forall h1' : _34305, forall f : _34305 -> _34312 -> _34302, forall t1 : list _34305, forall l : list _34312, (MAP2' _18174 f (@cons _34305 h1' t1) l) = (@cons _34302 (f h1' (@hd _34312 l)) (MAP2' _18174 f t1 (@tl _34312 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 {_34302 _34305 _34312 : Type'} : (@MAP2 _34302 _34305 _34312) = (@ε ((prod nat (prod nat (prod nat nat))) -> (_34305 -> _34312 -> _34302) -> (list _34305) -> (list _34312) -> list _34302) (fun MAP2' : (prod nat (prod nat (prod nat nat))) -> (_34305 -> _34312 -> _34302) -> (list _34305) -> (list _34312) -> list _34302 => forall _18174 : prod nat (prod nat (prod nat nat)), (forall f : _34305 -> _34312 -> _34302, forall l : list _34312, (MAP2' _18174 f (@nil _34305) l) = (@nil _34302)) /\ (forall h1' : _34305, forall f : _34305 -> _34312 -> _34302, forall t1 : list _34305, forall l : list _34312, (MAP2' _18174 f (@cons _34305 h1' t1) l) = (@cons _34302 (f h1' (@hd _34312 l)) (MAP2' _18174 f t1 (@tl _34312 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 _34302 _34305 _34312)). Qed.
Definition EL {_34373 : Type'} := @ε ((prod nat nat) -> nat -> (list _34373) -> _34373) (fun EL' : (prod nat nat) -> nat -> (list _34373) -> _34373 => forall _18178 : prod nat nat, (forall l : list _34373, (EL' _18178 (NUMERAL 0) l) = (@hd _34373 l)) /\ (forall n : nat, forall l : list _34373, (EL' _18178 (S n) l) = (EL' _18178 n (@tl _34373 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 {_34373 : Type'} : (@EL _34373) = (@ε ((prod nat nat) -> nat -> (list _34373) -> _34373) (fun EL' : (prod nat nat) -> nat -> (list _34373) -> _34373 => forall _18178 : prod nat nat, (forall l : list _34373, (EL' _18178 (NUMERAL 0) l) = (@hd _34373 l)) /\ (forall n : nat, forall l : list _34373, (EL' _18178 (S n) l) = (EL' _18178 n (@tl _34373 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 _34373)). Qed.
Definition FILTER {_34398 : Type'} := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (_34398 -> Prop) -> (list _34398) -> list _34398) (fun FILTER' : (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (_34398 -> Prop) -> (list _34398) -> list _34398 => forall _18185 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), (forall P : _34398 -> Prop, (FILTER' _18185 P (@nil _34398)) = (@nil _34398)) /\ (forall h : _34398, forall P : _34398 -> Prop, forall t : list _34398, (FILTER' _18185 P (@cons _34398 h t)) = (@COND (list _34398) (P h) (@cons _34398 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 {_34398 : Type'} : (@FILTER _34398) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (_34398 -> Prop) -> (list _34398) -> list _34398) (fun FILTER' : (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (_34398 -> Prop) -> (list _34398) -> list _34398 => forall _18185 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), (forall P : _34398 -> Prop, (FILTER' _18185 P (@nil _34398)) = (@nil _34398)) /\ (forall h : _34398, forall P : _34398 -> Prop, forall t : list _34398, (FILTER' _18185 P (@cons _34398 h t)) = (@COND (list _34398) (P h) (@cons _34398 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 _34398)). Qed.
Definition ASSOC {_34421 _34427 : Type'} := @ε ((prod nat (prod nat (prod nat (prod nat nat)))) -> _34427 -> (list (prod _34427 _34421)) -> _34421) (fun ASSOC' : (prod nat (prod nat (prod nat (prod nat nat)))) -> _34427 -> (list (prod _34427 _34421)) -> _34421 => forall _18192 : prod nat (prod nat (prod nat (prod nat nat))), forall h : prod _34427 _34421, forall a : _34427, forall t : list (prod _34427 _34421), (ASSOC' _18192 a (@cons (prod _34427 _34421) h t)) = (@COND _34421 ((@fst _34427 _34421 h) = a) (@snd _34427 _34421 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 {_34421 _34427 : Type'} : (@ASSOC _34421 _34427) = (@ε ((prod nat (prod nat (prod nat (prod nat nat)))) -> _34427 -> (list (prod _34427 _34421)) -> _34421) (fun ASSOC' : (prod nat (prod nat (prod nat (prod nat nat)))) -> _34427 -> (list (prod _34427 _34421)) -> _34421 => forall _18192 : prod nat (prod nat (prod nat (prod nat nat))), forall h : prod _34427 _34421, forall a : _34427, forall t : list (prod _34427 _34421), (ASSOC' _18192 a (@cons (prod _34427 _34421) h t)) = (@COND _34421 ((@fst _34427 _34421 h) = a) (@snd _34427 _34421 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 _34421 _34427)). Qed.
Definition ITLIST2 {_34449 _34451 _34459 : Type'} := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (_34451 -> _34459 -> _34449 -> _34449) -> (list _34451) -> (list _34459) -> _34449 -> _34449) (fun ITLIST2' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (_34451 -> _34459 -> _34449 -> _34449) -> (list _34451) -> (list _34459) -> _34449 -> _34449 => forall _18201 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))), (forall f : _34451 -> _34459 -> _34449 -> _34449, forall l2 : list _34459, forall b : _34449, (ITLIST2' _18201 f (@nil _34451) l2 b) = b) /\ (forall h1' : _34451, forall f : _34451 -> _34459 -> _34449 -> _34449, forall t1 : list _34451, forall l2 : list _34459, forall b : _34449, (ITLIST2' _18201 f (@cons _34451 h1' t1) l2 b) = (f h1' (@hd _34459 l2) (ITLIST2' _18201 f t1 (@tl _34459 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 {_34449 _34451 _34459 : Type'} : (@ITLIST2 _34449 _34451 _34459) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (_34451 -> _34459 -> _34449 -> _34449) -> (list _34451) -> (list _34459) -> _34449 -> _34449) (fun ITLIST2' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (_34451 -> _34459 -> _34449 -> _34449) -> (list _34451) -> (list _34459) -> _34449 -> _34449 => forall _18201 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))), (forall f : _34451 -> _34459 -> _34449 -> _34449, forall l2 : list _34459, forall b : _34449, (ITLIST2' _18201 f (@nil _34451) l2 b) = b) /\ (forall h1' : _34451, forall f : _34451 -> _34459 -> _34449 -> _34449, forall t1 : list _34451, forall l2 : list _34459, forall b : _34449, (ITLIST2' _18201 f (@cons _34451 h1' t1) l2 b) = (f h1' (@hd _34459 l2) (ITLIST2' _18201 f t1 (@tl _34459 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 _34449 _34451 _34459)). Qed.
Definition ZIP {_34523 _34531 : Type'} := @ε ((prod nat (prod nat nat)) -> (list _34523) -> (list _34531) -> list (prod _34523 _34531)) (fun ZIP' : (prod nat (prod nat nat)) -> (list _34523) -> (list _34531) -> list (prod _34523 _34531) => forall _18205 : prod nat (prod nat nat), (forall l2 : list _34531, (ZIP' _18205 (@nil _34523) l2) = (@nil (prod _34523 _34531))) /\ (forall h1' : _34523, forall t1 : list _34523, forall l2 : list _34531, (ZIP' _18205 (@cons _34523 h1' t1) l2) = (@cons (prod _34523 _34531) (@pair _34523 _34531 h1' (@hd _34531 l2)) (ZIP' _18205 t1 (@tl _34531 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 {_34523 _34531 : Type'} : (@ZIP _34523 _34531) = (@ε ((prod nat (prod nat nat)) -> (list _34523) -> (list _34531) -> list (prod _34523 _34531)) (fun ZIP' : (prod nat (prod nat nat)) -> (list _34523) -> (list _34531) -> list (prod _34523 _34531) => forall _18205 : prod nat (prod nat nat), (forall l2 : list _34531, (ZIP' _18205 (@nil _34523) l2) = (@nil (prod _34523 _34531))) /\ (forall h1' : _34523, forall t1 : list _34523, forall l2 : list _34531, (ZIP' _18205 (@cons _34523 h1' t1) l2) = (@cons (prod _34523 _34531) (@pair _34523 _34531 h1' (@hd _34531 l2)) (ZIP' _18205 t1 (@tl _34531 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 _34523 _34531)). Qed.
Definition ALLPAIRS {_34590 _34591 : Type'} := @ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> (_34591 -> _34590 -> Prop) -> (list _34591) -> (list _34590) -> Prop) (fun ALLPAIRS' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> (_34591 -> _34590 -> Prop) -> (list _34591) -> (list _34590) -> Prop => forall _18213 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))), (forall f : _34591 -> _34590 -> Prop, forall l : list _34590, (ALLPAIRS' _18213 f (@nil _34591) l) = True) /\ (forall h : _34591, forall f : _34591 -> _34590 -> Prop, forall t : list _34591, forall l : list _34590, (ALLPAIRS' _18213 f (@cons _34591 h t) l) = ((@List.Forall _34590 (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 {_34590 _34591 : Type'} : (@ALLPAIRS _34590 _34591) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> (_34591 -> _34590 -> Prop) -> (list _34591) -> (list _34590) -> Prop) (fun ALLPAIRS' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> (_34591 -> _34590 -> Prop) -> (list _34591) -> (list _34590) -> Prop => forall _18213 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))), (forall f : _34591 -> _34590 -> Prop, forall l : list _34590, (ALLPAIRS' _18213 f (@nil _34591) l) = True) /\ (forall h : _34591, forall f : _34591 -> _34590 -> Prop, forall t : list _34591, forall l : list _34590, (ALLPAIRS' _18213 f (@cons _34591 h t) l) = ((@List.Forall _34590 (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 _34590 _34591)). Qed.
Definition list_of_seq {A : Type'} := @ε ((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 _22893 := 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 _22893_def : _22893 = (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 _22893). Qed.
Definition ASCII := _22893.
Lemma ASCII_def : ASCII = _22893.
Proof. exact (eq_refl ASCII). Qed.