6
version
"Data.Bool.!"
const
0
def
"->"
typeOp
1
def
1
ref
"Number.Natural.natural"
typeOp
nil
opType
2
def
"bool"
typeOp
nil
opType
3
def
nil
cons
4
def
cons
opType
5
def
4
ref
cons
opType
6
def
constTerm
7
def
refl
8
def
"m"
2
ref
var
9
def
nil
"t"
3
ref
var
10
def
"Number.Natural.<"
"<"
1
ref
2
ref
5
ref
nil
cons
11
def
cons
opType
12
def
var
13
def
nil
cons
cons
nil
cons
13
ref
"Data.Bool./\\"
const
1
ref
3
ref
1
ref
3
ref
4
ref
cons
opType
14
def
nil
cons
cons
opType
15
def
constTerm
16
def
7
ref
9
ref
"="
const
17
def
15
ref
constTerm
18
def
13
ref
varTerm
19
def
9
ref
varTerm
20
def
appTerm
21
def
"Number.Natural.zero"
const
2
ref
constTerm
22
def
appTerm
appTerm
"Data.Bool.F"
const
3
ref
constTerm
23
def
appTerm
absTerm
appTerm
appTerm
7
ref
9
ref
7
ref
"n"
2
ref
var
24
def
18
ref
21
ref
"Number.Natural.suc"
const
1
ref
2
ref
2
ref
nil
cons
25
def
cons
opType
constTerm
26
def
24
ref
varTerm
27
def
appTerm
28
def
appTerm
appTerm
"Data.Bool.\\/"
const
15
ref
constTerm
29
def
17
ref
12
ref
constTerm
20
ref
appTerm
30
def
27
ref
appTerm
appTerm
31
def
21
remove
27
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
32
def
refl
33
def
17
ref
1
ref
12
ref
1
ref
12
ref
4
ref
cons
opType
34
def
nil
cons
cons
opType
constTerm
35
def
19
ref
appTerm
36
def
"select"
const
37
def
1
ref
34
ref
12
ref
nil
cons
38
def
cons
opType
constTerm
39
def
32
ref
appTerm
appTerm
assume
sym
appThm
32
ref
19
ref
appTerm
betaConv
40
def
trans
"A"
38
ref
cons
nil
cons
41
def
nil
nil
cons
42
def
cons
43
def
nil
17
ref
1
ref
1
ref
1
ref
"A"
varType
44
def
4
ref
cons
opType
45
def
4
ref
cons
opType
46
def
1
ref
46
ref
4
ref
cons
opType
nil
cons
cons
opType
constTerm
47
def
"Data.Bool.?"
const
48
def
46
ref
constTerm
49
def
appTerm
50
def
"p"
45
ref
var
51
def
51
ref
varTerm
52
def
37
remove
1
ref
45
ref
44
ref
nil
cons
53
def
cons
opType
constTerm
52
ref
appTerm
appTerm
absTerm
appTerm
axiom
subst
54
def
33
remove
appThm
"p"
34
ref
var
55
def
55
remove
varTerm
56
def
39
ref
56
remove
appTerm
appTerm
absTerm
57
def
32
ref
appTerm
betaConv
trans
48
ref
1
ref
34
ref
4
ref
cons
opType
58
def
constTerm
59
def
refl
60
def
"fn"
12
ref
var
61
def
16
ref
17
ref
1
ref
5
ref
6
remove
nil
cons
cons
opType
constTerm
62
def
61
ref
varTerm
63
def
22
ref
appTerm
appTerm
64
def
9
ref
23
ref
absTerm
65
def
appTerm
appTerm
refl
8
ref
24
ref
62
ref
63
ref
28
ref
appTerm
appTerm
refl
66
def
"_1952"
5
ref
var
67
def
24
ref
9
ref
31
ref
67
remove
varTerm
20
ref
appTerm
appTerm
absTerm
absTerm
absTerm
68
def
63
remove
27
ref
appTerm
69
def
appTerm
betaConv
27
ref
refl
70
def
appThm
"n'"
2
ref
var
71
def
9
ref
29
ref
30
ref
71
ref
varTerm
72
def
appTerm
appTerm
69
ref
20
ref
appTerm
73
def
appTerm
absTerm
absTerm
27
ref
appTerm
betaConv
trans
appThm
absThm
appThm
appThm
absThm
appThm
nil
"f"
1
ref
5
ref
38
remove
cons
opType
var
74
def
68
remove
nil
cons
cons
"e"
5
ref
var
75
def
65
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
"A"
11
remove
cons
nil
cons
42
ref
cons
"f"
1
ref
44
ref
1
ref
2
ref
53
ref
cons
opType
76
def
nil
cons
77
def
cons
opType
78
def
var
79
def
"Data.Bool.?!"
const
80
def
1
ref
1
ref
76
ref
4
ref
cons
opType
81
def
4
ref
cons
opType
82
def
constTerm
"fn"
76
remove
var
83
def
16
ref
17
ref
1
ref
44
ref
45
ref
nil
cons
cons
opType
constTerm
84
def
83
remove
varTerm
85
def
22
ref
appTerm
appTerm
"e"
44
ref
var
86
def
varTerm
87
def
appTerm
appTerm
7
ref
24
ref
84
ref
85
ref
28
ref
appTerm
appTerm
79
remove
varTerm
88
def
85
remove
27
ref
appTerm
appTerm
27
ref
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
89
def
appTerm
90
def
absTerm
91
def
88
ref
appTerm
92
def
betaConv
86
remove
0
ref
1
ref
1
ref
78
ref
4
ref
cons
opType
93
def
4
ref
cons
opType
constTerm
91
ref
appTerm
94
def
absTerm
95
def
87
ref
appTerm
96
def
betaConv
nil
0
ref
46
ref
constTerm
97
def
95
ref
appTerm
98
def
axiom
nil
"p"
3
ref
var
99
def
98
remove
nil
cons
cons
"q"
3
ref
var
100
def
96
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
18
ref
"Data.Bool.==>"
const
15
ref
constTerm
101
def
99
ref
varTerm
102
def
appTerm
100
ref
varTerm
103
def
appTerm
104
def
appTerm
refl
99
ref
100
ref
18
ref
16
ref
102
ref
appTerm
105
def
103
ref
appTerm
106
def
appTerm
107
def
102
ref
appTerm
absTerm
108
def
absTerm
109
def
102
ref
appTerm
betaConv
103
ref
refl
110
def
appThm
108
remove
103
ref
appTerm
betaConv
trans
appThm
nil
17
ref
1
ref
15
ref
1
ref
15
ref
4
ref
cons
opType
111
def
nil
cons
cons
opType
constTerm
112
def
101
ref
appTerm
109
remove
appTerm
axiom
102
ref
refl
113
def
appThm
110
ref
appThm
eqMp
114
def
sym
115
def
107
remove
refl
100
ref
17
ref
1
ref
111
ref
1
ref
111
remove
4
ref
cons
opType
nil
cons
cons
opType
constTerm
116
def
"f"
15
remove
var
117
def
117
ref
varTerm
118
def
102
ref
appTerm
103
ref
appTerm
absTerm
119
def
appTerm
117
ref
118
ref
"Data.Bool.T"
const
3
ref
constTerm
120
def
appTerm
120
ref
appTerm
absTerm
121
def
appTerm
absTerm
122
def
103
ref
appTerm
betaConv
appThm
17
ref
1
ref
14
ref
1
ref
14
ref
4
ref
cons
opType
123
def
nil
cons
cons
opType
constTerm
124
def
105
remove
appTerm
refl
99
ref
122
remove
absTerm
125
def
102
ref
appTerm
betaConv
appThm
nil
112
remove
16
ref
appTerm
125
ref
appTerm
axiom
126
def
113
remove
appThm
eqMp
110
ref
appThm
eqMp
127
def
sym
117
ref
118
ref
refl
nil
10
ref
102
ref
nil
cons
128
def
cons
nil
cons
nil
cons
cons
18
ref
10
ref
varTerm
129
def
appTerm
130
def
120
ref
appTerm
assume
sym
nil
120
ref
axiom
131
def
eqMp
129
ref
assume
131
ref
deductAntisym
deductAntisym
132
def
subst
102
ref
assume
133
def
eqMp
appThm
nil
10
ref
103
ref
nil
cons
134
def
cons
nil
cons
nil
cons
cons
132
ref
subst
103
ref
assume
eqMp
appThm
absThm
eqMp
135
def
nil
"P"
3
ref
var
136
def
128
remove
cons
"Q"
3
ref
var
137
def
134
remove
cons
nil
cons
cons
nil
cons
cons
18
ref
refl
138
def
117
ref
118
remove
136
ref
varTerm
139
def
appTerm
140
def
137
ref
varTerm
141
def
appTerm
absTerm
142
def
99
ref
100
ref
102
ref
absTerm
absTerm
143
def
appTerm
betaConv
143
ref
139
ref
appTerm
betaConv
141
ref
refl
144
def
appThm
100
ref
139
ref
absTerm
141
ref
appTerm
betaConv
trans
trans
appThm
121
ref
143
ref
appTerm
betaConv
143
ref
120
ref
appTerm
betaConv
120
ref
refl
145
def
appThm
100
ref
120
ref
absTerm
120
ref
appTerm
betaConv
trans
trans
appThm
18
ref
16
ref
139
ref
appTerm
146
def
141
ref
appTerm
147
def
appTerm
refl
100
ref
116
remove
117
remove
140
remove
103
ref
appTerm
absTerm
appTerm
121
ref
appTerm
absTerm
141
ref
appTerm
betaConv
appThm
124
remove
146
remove
appTerm
refl
125
remove
139
ref
appTerm
betaConv
appThm
126
remove
139
ref
refl
appThm
eqMp
144
ref
appThm
eqMp
147
remove
assume
eqMp
148
def
143
remove
refl
appThm
eqMp
sym
131
ref
eqMp
149
def
subst
150
def
deductAntisym
eqMp
114
remove
104
ref
assume
eqMp
sym
133
ref
eqMp
138
ref
119
remove
99
ref
100
ref
103
ref
absTerm
151
def
absTerm
152
def
appTerm
betaConv
152
ref
102
ref
appTerm
betaConv
110
remove
appThm
151
ref
103
ref
appTerm
betaConv
trans
trans
appThm
121
remove
152
ref
appTerm
betaConv
152
ref
120
ref
appTerm
betaConv
145
remove
appThm
151
ref
120
ref
appTerm
betaConv
trans
trans
153
def
appThm
127
remove
106
remove
assume
eqMp
152
ref
refl
154
def
appThm
eqMp
sym
131
ref
eqMp
155
def
proveHyp
deductAntisym
156
def
subst
proveHyp
"A"
53
remove
cons
nil
cons
157
def
"P"
45
ref
var
158
def
95
remove
nil
cons
cons
"x"
44
ref
var
159
def
87
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
99
ref
97
ref
158
ref
varTerm
160
def
appTerm
161
def
nil
cons
162
def
cons
100
ref
160
ref
159
ref
varTerm
163
def
appTerm
164
def
nil
cons
165
def
cons
nil
cons
cons
nil
cons
cons
166
def
115
ref
subst
166
remove
155
remove
135
remove
deductAntisym
167
def
subst
18
ref
164
ref
appTerm
refl
159
ref
120
remove
absTerm
168
def
163
ref
appTerm
betaConv
appThm
51
ref
17
remove
1
remove
45
remove
46
ref
nil
cons
cons
opType
constTerm
52
ref
appTerm
168
remove
appTerm
absTerm
169
def
160
ref
appTerm
betaConv
170
def
nil
47
ref
97
ref
appTerm
169
remove
appTerm
axiom
160
ref
refl
171
def
appThm
172
def
161
ref
assume
eqMp
eqMp
163
ref
refl
appThm
eqMp
sym
131
ref
eqMp
eqMp
nil
136
ref
162
remove
cons
137
ref
165
ref
cons
nil
cons
cons
nil
cons
cons
149
ref
subst
deductAntisym
eqMp
173
def
subst
eqMp
eqMp
nil
99
ref
94
remove
nil
cons
cons
100
ref
92
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
156
ref
subst
proveHyp
"A"
78
ref
nil
cons
cons
nil
cons
"P"
93
remove
var
91
remove
nil
cons
cons
"x"
78
remove
var
88
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
eqMp
eqMp
nil
99
ref
90
remove
nil
cons
cons
100
ref
48
remove
82
remove
constTerm
89
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
156
ref
subst
proveHyp
"A"
77
remove
cons
nil
cons
"P"
81
remove
var
89
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
99
ref
80
remove
46
remove
constTerm
174
def
160
ref
appTerm
175
def
nil
cons
176
def
cons
177
def
100
ref
49
ref
160
ref
appTerm
178
def
nil
cons
179
def
cons
nil
cons
cons
nil
cons
cons
180
def
115
ref
subst
180
remove
167
ref
subst
nil
177
remove
100
ref
16
ref
178
ref
appTerm
97
ref
159
ref
97
ref
"y"
44
remove
var
181
def
101
ref
16
ref
164
ref
appTerm
160
ref
181
ref
varTerm
182
def
appTerm
appTerm
appTerm
84
remove
163
ref
appTerm
182
ref
appTerm
183
def
appTerm
absTerm
appTerm
absTerm
appTerm
184
def
appTerm
185
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
186
def
156
ref
subst
18
ref
175
ref
appTerm
187
def
refl
51
ref
16
ref
49
remove
52
ref
appTerm
appTerm
97
ref
159
ref
97
ref
181
remove
101
ref
16
ref
52
ref
163
ref
appTerm
188
def
appTerm
52
remove
182
remove
appTerm
appTerm
appTerm
183
remove
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
189
def
160
ref
appTerm
betaConv
appThm
nil
47
remove
174
remove
appTerm
189
remove
appTerm
axiom
171
ref
appThm
eqMp
nil
99
ref
187
remove
185
ref
appTerm
nil
cons
cons
100
ref
101
ref
175
remove
appTerm
185
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
156
ref
subst
proveHyp
186
remove
nil
99
ref
18
ref
102
remove
appTerm
103
ref
appTerm
190
def
nil
cons
191
def
cons
100
ref
104
remove
nil
cons
192
def
cons
nil
cons
cons
nil
cons
cons
193
def
115
ref
subst
193
remove
167
ref
subst
115
ref
167
ref
190
remove
assume
133
remove
eqMp
eqMp
150
remove
deductAntisym
eqMp
eqMp
nil
136
ref
191
remove
cons
137
ref
192
remove
cons
nil
cons
cons
nil
cons
cons
149
ref
subst
deductAntisym
eqMp
194
def
subst
eqMp
eqMp
nil
136
ref
179
ref
cons
195
def
137
ref
184
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
149
ref
subst
proveHyp
eqMp
nil
136
ref
176
remove
cons
137
ref
179
ref
cons
nil
cons
cons
nil
cons
cons
149
ref
subst
deductAntisym
eqMp
subst
eqMp
subst
196
def
subst
eqMp
nil
99
ref
59
ref
"_1951"
12
ref
var
197
def
16
ref
62
ref
197
ref
varTerm
198
def
22
ref
appTerm
199
def
appTerm
65
ref
appTerm
200
def
appTerm
7
ref
24
ref
62
ref
198
ref
28
ref
appTerm
201
def
appTerm
9
ref
31
ref
198
ref
27
ref
appTerm
20
ref
appTerm
appTerm
202
def
absTerm
203
def
appTerm
absTerm
204
def
appTerm
205
def
appTerm
206
def
absTerm
207
def
appTerm
208
def
nil
cons
cons
100
ref
59
ref
197
ref
16
ref
7
ref
9
ref
18
ref
199
remove
20
ref
appTerm
appTerm
209
def
23
ref
appTerm
210
def
absTerm
211
def
appTerm
212
def
appTerm
7
ref
9
ref
7
ref
24
ref
18
ref
201
remove
20
ref
appTerm
appTerm
213
def
202
remove
appTerm
214
def
absTerm
215
def
appTerm
216
def
absTerm
217
def
appTerm
218
def
appTerm
219
def
absTerm
220
def
appTerm
221
def
nil
cons
222
def
cons
nil
cons
223
def
cons
nil
cons
cons
156
ref
subst
nil
"P"
34
remove
var
224
def
197
ref
101
ref
207
ref
198
ref
appTerm
225
def
appTerm
221
ref
appTerm
226
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
43
remove
18
ref
161
remove
appTerm
refl
170
remove
appThm
172
remove
eqMp
sym
227
def
subst
228
def
subst
197
ref
nil
10
ref
226
remove
nil
cons
cons
nil
cons
nil
cons
cons
132
ref
subst
nil
99
ref
225
ref
nil
cons
229
def
cons
223
ref
cons
nil
cons
cons
230
def
115
ref
subst
230
remove
167
ref
subst
225
ref
betaConv
225
remove
assume
eqMp
nil
99
ref
206
remove
nil
cons
231
def
cons
223
remove
cons
nil
cons
cons
232
def
156
ref
subst
proveHyp
232
ref
115
ref
subst
232
remove
167
ref
subst
220
ref
198
ref
appTerm
233
def
betaConv
234
def
sym
nil
136
ref
200
ref
nil
cons
cons
137
ref
205
remove
nil
cons
235
def
cons
nil
cons
cons
nil
cons
cons
236
def
149
ref
subst
nil
"P"
5
ref
var
237
def
211
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
25
remove
cons
nil
cons
238
def
42
ref
cons
227
ref
subst
239
def
subst
9
ref
nil
10
ref
210
remove
nil
cons
cons
nil
cons
nil
cons
cons
132
ref
subst
209
remove
refl
65
remove
20
ref
appTerm
betaConv
appThm
200
remove
assume
20
ref
refl
240
def
appThm
eqMp
eqMp
absThm
eqMp
proveHyp
nil
99
ref
212
remove
nil
cons
cons
100
ref
218
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
236
remove
138
ref
142
remove
152
ref
appTerm
betaConv
152
remove
139
remove
appTerm
betaConv
144
remove
appThm
151
remove
141
ref
appTerm
betaConv
trans
trans
appThm
153
remove
appThm
148
remove
154
remove
appThm
eqMp
sym
131
remove
eqMp
241
def
subst
nil
237
ref
217
remove
nil
cons
cons
nil
cons
nil
cons
cons
239
ref
subst
9
ref
nil
10
ref
216
remove
nil
cons
cons
nil
cons
nil
cons
cons
132
ref
subst
nil
237
ref
215
remove
nil
cons
cons
nil
cons
nil
cons
cons
239
ref
subst
24
ref
nil
10
ref
214
remove
nil
cons
cons
nil
cons
nil
cons
cons
132
ref
subst
213
remove
refl
203
remove
20
ref
appTerm
betaConv
appThm
204
ref
27
ref
appTerm
242
def
betaConv
nil
99
ref
235
remove
cons
100
ref
242
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
156
ref
subst
238
ref
237
ref
204
remove
nil
cons
cons
"x"
2
ref
var
27
ref
nil
cons
cons
nil
cons
243
def
cons
nil
cons
cons
173
ref
subst
eqMp
eqMp
240
ref
appThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
proveHyp
eqMp
eqMp
41
ref
224
ref
220
ref
nil
cons
cons
244
def
"x"
12
ref
var
245
def
198
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
18
ref
178
ref
appTerm
246
def
refl
51
remove
0
ref
123
remove
constTerm
247
def
100
ref
101
ref
97
ref
159
ref
101
ref
188
remove
appTerm
103
ref
appTerm
absTerm
appTerm
appTerm
103
ref
appTerm
absTerm
appTerm
absTerm
248
def
160
remove
appTerm
betaConv
appThm
nil
50
remove
248
remove
appTerm
axiom
171
remove
appThm
eqMp
249
def
sym
nil
"P"
14
ref
var
250
def
137
ref
101
ref
97
ref
159
ref
101
ref
164
remove
appTerm
251
def
141
ref
appTerm
absTerm
252
def
appTerm
253
def
appTerm
141
ref
appTerm
254
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
4
remove
cons
nil
cons
255
def
42
remove
cons
227
remove
subst
subst
137
ref
nil
10
ref
254
remove
nil
cons
cons
nil
cons
nil
cons
cons
132
ref
subst
nil
99
ref
253
remove
nil
cons
256
def
cons
257
def
100
ref
141
ref
nil
cons
258
def
cons
nil
cons
259
def
cons
nil
cons
cons
260
def
115
ref
subst
260
ref
167
ref
subst
nil
99
ref
165
remove
cons
259
ref
cons
nil
cons
cons
156
ref
subst
252
ref
163
ref
appTerm
261
def
betaConv
nil
257
ref
100
ref
261
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
156
ref
subst
157
remove
158
remove
252
remove
nil
cons
cons
159
ref
163
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
136
ref
256
remove
cons
262
def
137
ref
258
ref
cons
nil
cons
263
def
cons
nil
cons
cons
149
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
264
def
subst
proveHyp
eqMp
nil
136
ref
231
remove
cons
137
ref
222
ref
cons
nil
cons
265
def
cons
nil
cons
cons
149
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
136
ref
229
remove
cons
265
ref
cons
nil
cons
cons
149
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
99
ref
0
remove
58
remove
constTerm
266
def
245
ref
101
ref
207
ref
245
ref
varTerm
267
def
appTerm
appTerm
221
ref
appTerm
absTerm
appTerm
nil
cons
cons
100
ref
101
ref
208
remove
appTerm
221
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
156
ref
subst
proveHyp
41
ref
224
ref
207
remove
nil
cons
cons
265
remove
cons
nil
cons
cons
nil
257
remove
100
ref
101
ref
178
remove
appTerm
268
def
141
ref
appTerm
nil
cons
269
def
cons
nil
cons
cons
nil
cons
cons
270
def
115
ref
subst
270
remove
167
ref
subst
nil
99
ref
179
remove
cons
271
def
259
remove
cons
nil
cons
cons
272
def
115
ref
subst
272
remove
167
ref
subst
260
remove
156
ref
subst
100
ref
101
ref
97
remove
159
remove
251
remove
103
ref
appTerm
absTerm
appTerm
appTerm
103
remove
appTerm
absTerm
273
def
141
remove
appTerm
274
def
betaConv
nil
271
remove
100
ref
247
ref
273
ref
appTerm
275
def
nil
cons
276
def
cons
nil
cons
cons
nil
cons
cons
277
def
156
ref
subst
249
remove
nil
99
ref
246
remove
275
ref
appTerm
nil
cons
cons
100
ref
268
remove
275
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
156
ref
subst
proveHyp
277
remove
194
remove
subst
eqMp
eqMp
nil
99
ref
276
remove
cons
100
ref
274
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
156
ref
subst
proveHyp
255
ref
250
ref
273
remove
nil
cons
cons
"x"
3
remove
var
278
def
258
remove
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
195
remove
263
remove
cons
nil
cons
cons
149
ref
subst
deductAntisym
eqMp
eqMp
nil
262
remove
137
ref
269
remove
cons
nil
cons
cons
nil
cons
cons
149
ref
subst
deductAntisym
eqMp
279
def
subst
eqMp
eqMp
proveHyp
nil
99
ref
222
remove
cons
100
ref
59
ref
32
ref
appTerm
280
def
nil
cons
281
def
cons
nil
cons
282
def
cons
nil
cons
cons
156
ref
subst
nil
224
ref
197
ref
101
ref
233
ref
appTerm
280
ref
appTerm
283
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
228
ref
subst
197
remove
nil
10
ref
283
remove
nil
cons
cons
nil
cons
nil
cons
cons
132
ref
subst
nil
99
ref
233
ref
nil
cons
284
def
cons
282
ref
cons
nil
cons
cons
285
def
115
ref
subst
285
remove
167
ref
subst
234
remove
233
remove
assume
eqMp
nil
99
ref
219
ref
nil
cons
286
def
cons
282
ref
cons
nil
cons
cons
287
def
156
ref
subst
proveHyp
287
ref
115
ref
subst
287
remove
167
ref
subst
"_1949"
2
ref
var
288
def
"_1950"
2
ref
var
289
def
198
remove
289
ref
varTerm
appTerm
290
def
288
remove
varTerm
appTerm
absTerm
absTerm
291
def
refl
nil
99
ref
35
ref
291
ref
appTerm
291
ref
appTerm
nil
cons
cons
282
ref
cons
nil
cons
cons
156
ref
subst
proveHyp
nil
13
remove
291
ref
nil
cons
cons
nil
cons
nil
cons
cons
nil
99
ref
36
remove
291
ref
appTerm
292
def
nil
cons
293
def
cons
282
remove
cons
nil
cons
cons
294
def
115
ref
subst
294
remove
167
ref
subst
40
remove
sym
16
ref
refl
295
def
8
ref
9
ref
138
ref
292
remove
assume
240
ref
appThm
291
remove
20
ref
appTerm
betaConv
trans
296
def
nil
24
ref
22
ref
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
297
def
appThm
289
remove
290
remove
20
ref
appTerm
absTerm
298
def
22
ref
appTerm
betaConv
trans
appThm
23
ref
refl
appThm
absThm
appThm
appThm
8
ref
9
ref
8
ref
24
ref
138
ref
296
ref
28
ref
refl
299
def
appThm
298
ref
28
ref
appTerm
betaConv
trans
appThm
31
ref
refl
296
remove
70
ref
appThm
298
remove
27
ref
appTerm
betaConv
trans
appThm
appThm
absThm
appThm
absThm
appThm
appThm
sym
219
remove
assume
eqMp
eqMp
41
ref
224
ref
32
remove
nil
cons
cons
245
ref
19
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
264
ref
subst
proveHyp
eqMp
nil
136
ref
293
remove
cons
137
ref
281
remove
cons
nil
cons
300
def
cons
nil
cons
cons
149
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
136
ref
286
remove
cons
300
ref
cons
nil
cons
cons
149
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
136
ref
284
remove
cons
300
ref
cons
nil
cons
cons
149
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
99
ref
266
ref
245
ref
101
ref
220
remove
267
ref
appTerm
appTerm
280
ref
appTerm
absTerm
appTerm
nil
cons
cons
100
ref
101
ref
221
remove
appTerm
280
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
156
ref
subst
proveHyp
41
ref
244
remove
300
remove
cons
nil
cons
cons
279
ref
subst
eqMp
eqMp
proveHyp
eqMp
eqMp
defineConstList
301
def
pop
hdTl
pop
12
ref
constTerm
302
def
20
ref
appTerm
303
def
22
ref
appTerm
304
def
nil
cons
cons
nil
cons
nil
cons
cons
10
ref
18
ref
130
remove
23
ref
appTerm
appTerm
"Data.Bool.~"
const
14
remove
constTerm
305
def
129
ref
appTerm
appTerm
absTerm
306
def
129
ref
appTerm
307
def
betaConv
nil
247
remove
306
ref
appTerm
308
def
axiom
nil
99
ref
308
remove
nil
cons
cons
100
ref
307
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
156
ref
subst
proveHyp
255
remove
250
remove
306
remove
nil
cons
cons
278
remove
129
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
eqMp
eqMp
subst
absThm
appThm
301
ref
nil
136
ref
7
ref
9
ref
18
ref
304
ref
appTerm
23
remove
appTerm
absTerm
appTerm
nil
cons
cons
137
ref
7
ref
9
ref
7
ref
24
ref
18
ref
303
ref
28
ref
appTerm
appTerm
31
remove
303
remove
27
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
309
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
310
def
149
ref
subst
proveHyp
eqMp
nil
7
ref
9
ref
305
remove
304
remove
appTerm
absTerm
appTerm
thm
"Number.Natural.<="
"<="
12
ref
var
311
def
nil
cons
cons
nil
cons
311
ref
16
ref
7
ref
9
ref
18
ref
311
ref
varTerm
312
def
20
ref
appTerm
313
def
22
ref
appTerm
appTerm
30
ref
22
ref
appTerm
314
def
appTerm
absTerm
appTerm
appTerm
7
ref
9
ref
7
ref
24
ref
18
ref
313
ref
28
ref
appTerm
appTerm
29
ref
30
ref
28
ref
appTerm
appTerm
315
def
313
remove
27
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
316
def
refl
317
def
35
ref
312
ref
appTerm
318
def
39
remove
316
ref
appTerm
appTerm
assume
sym
appThm
316
ref
312
ref
appTerm
betaConv
319
def
trans
54
remove
317
remove
appThm
57
remove
316
ref
appTerm
betaConv
trans
60
remove
61
remove
16
ref
64
remove
9
ref
314
ref
absTerm
320
def
appTerm
appTerm
refl
8
ref
24
ref
66
remove
"_1946"
5
remove
var
321
def
24
ref
9
ref
315
ref
321
remove
varTerm
20
ref
appTerm
appTerm
absTerm
absTerm
absTerm
322
def
69
remove
appTerm
betaConv
70
ref
appThm
71
remove
9
ref
29
remove
30
remove
26
remove
72
remove
appTerm
appTerm
appTerm
73
remove
appTerm
absTerm
absTerm
27
ref
appTerm
betaConv
trans
appThm
absThm
appThm
appThm
absThm
appThm
nil
74
remove
322
remove
nil
cons
cons
75
remove
320
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
196
remove
subst
eqMp
nil
99
ref
59
ref
"_1945"
12
ref
var
323
def
16
ref
62
ref
323
ref
varTerm
324
def
22
ref
appTerm
325
def
appTerm
320
ref
appTerm
326
def
appTerm
7
ref
24
ref
62
remove
324
ref
28
ref
appTerm
327
def
appTerm
9
ref
315
ref
324
ref
27
ref
appTerm
20
ref
appTerm
appTerm
328
def
absTerm
329
def
appTerm
absTerm
330
def
appTerm
331
def
appTerm
332
def
absTerm
333
def
appTerm
334
def
nil
cons
cons
100
ref
59
ref
323
ref
16
remove
7
ref
9
ref
18
ref
325
remove
20
ref
appTerm
appTerm
335
def
314
ref
appTerm
336
def
absTerm
337
def
appTerm
338
def
appTerm
7
ref
9
ref
7
ref
24
ref
18
ref
327
remove
20
ref
appTerm
appTerm
339
def
328
remove
appTerm
340
def
absTerm
341
def
appTerm
342
def
absTerm
343
def
appTerm
344
def
appTerm
345
def
absTerm
346
def
appTerm
347
def
nil
cons
348
def
cons
nil
cons
349
def
cons
nil
cons
cons
156
ref
subst
nil
224
ref
323
ref
101
ref
333
ref
324
ref
appTerm
350
def
appTerm
347
ref
appTerm
351
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
228
ref
subst
323
ref
nil
10
ref
351
remove
nil
cons
cons
nil
cons
nil
cons
cons
132
ref
subst
nil
99
ref
350
ref
nil
cons
352
def
cons
349
ref
cons
nil
cons
cons
353
def
115
ref
subst
353
remove
167
ref
subst
350
ref
betaConv
350
remove
assume
eqMp
nil
99
ref
332
remove
nil
cons
354
def
cons
349
remove
cons
nil
cons
cons
355
def
156
ref
subst
proveHyp
355
ref
115
ref
subst
355
remove
167
ref
subst
346
ref
324
ref
appTerm
356
def
betaConv
357
def
sym
nil
136
ref
326
ref
nil
cons
cons
137
ref
331
remove
nil
cons
358
def
cons
nil
cons
cons
nil
cons
cons
359
def
149
ref
subst
nil
237
ref
337
remove
nil
cons
cons
nil
cons
nil
cons
cons
239
ref
subst
9
ref
nil
10
ref
336
remove
nil
cons
cons
nil
cons
nil
cons
cons
132
ref
subst
335
remove
refl
320
remove
20
ref
appTerm
betaConv
appThm
326
remove
assume
240
ref
appThm
eqMp
eqMp
absThm
eqMp
proveHyp
nil
99
ref
338
remove
nil
cons
cons
100
ref
344
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
359
remove
241
ref
subst
nil
237
ref
343
remove
nil
cons
cons
nil
cons
nil
cons
cons
239
ref
subst
9
ref
nil
10
ref
342
remove
nil
cons
cons
nil
cons
nil
cons
cons
132
ref
subst
nil
237
ref
341
remove
nil
cons
cons
nil
cons
nil
cons
cons
239
ref
subst
24
ref
nil
10
ref
340
remove
nil
cons
cons
nil
cons
nil
cons
cons
132
ref
subst
339
remove
refl
329
remove
20
ref
appTerm
betaConv
appThm
330
ref
27
ref
appTerm
360
def
betaConv
nil
99
ref
358
remove
cons
100
ref
360
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
156
ref
subst
238
remove
237
ref
330
remove
nil
cons
cons
243
remove
cons
nil
cons
cons
173
remove
subst
eqMp
eqMp
240
ref
appThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
proveHyp
eqMp
eqMp
41
ref
224
ref
346
ref
nil
cons
cons
361
def
245
ref
324
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
264
ref
subst
proveHyp
eqMp
nil
136
ref
354
remove
cons
137
ref
348
ref
cons
nil
cons
362
def
cons
nil
cons
cons
149
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
136
ref
352
remove
cons
362
ref
cons
nil
cons
cons
149
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
99
ref
266
ref
245
ref
101
ref
333
ref
267
ref
appTerm
appTerm
347
ref
appTerm
absTerm
appTerm
nil
cons
cons
100
ref
101
ref
334
remove
appTerm
347
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
156
ref
subst
proveHyp
41
ref
224
ref
333
remove
nil
cons
cons
362
remove
cons
nil
cons
cons
279
ref
subst
eqMp
eqMp
proveHyp
nil
99
ref
348
remove
cons
100
ref
59
remove
316
ref
appTerm
363
def
nil
cons
364
def
cons
nil
cons
365
def
cons
nil
cons
cons
156
ref
subst
nil
224
ref
323
ref
101
ref
356
ref
appTerm
363
ref
appTerm
366
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
228
remove
subst
323
remove
nil
10
ref
366
remove
nil
cons
cons
nil
cons
nil
cons
cons
132
ref
subst
nil
99
ref
356
ref
nil
cons
367
def
cons
365
ref
cons
nil
cons
cons
368
def
115
ref
subst
368
remove
167
ref
subst
357
remove
356
remove
assume
eqMp
nil
99
ref
345
ref
nil
cons
369
def
cons
365
ref
cons
nil
cons
cons
370
def
156
ref
subst
proveHyp
370
ref
115
ref
subst
370
remove
167
ref
subst
"_1943"
2
ref
var
371
def
"_1944"
2
ref
var
372
def
324
remove
372
ref
varTerm
appTerm
373
def
371
remove
varTerm
appTerm
absTerm
absTerm
374
def
refl
nil
99
ref
35
remove
374
ref
appTerm
374
ref
appTerm
nil
cons
cons
365
ref
cons
nil
cons
cons
156
ref
subst
proveHyp
nil
311
remove
374
ref
nil
cons
cons
nil
cons
nil
cons
cons
nil
99
ref
318
remove
374
ref
appTerm
375
def
nil
cons
376
def
cons
365
remove
cons
nil
cons
cons
377
def
115
remove
subst
377
remove
167
remove
subst
319
remove
sym
295
remove
8
ref
9
ref
138
ref
375
remove
assume
240
remove
appThm
374
remove
20
ref
appTerm
betaConv
trans
378
def
297
remove
appThm
372
remove
373
remove
20
ref
appTerm
absTerm
379
def
22
ref
appTerm
betaConv
trans
appThm
314
ref
refl
appThm
absThm
appThm
appThm
8
ref
9
ref
8
remove
24
ref
138
remove
378
ref
299
remove
appThm
379
ref
28
ref
appTerm
betaConv
trans
appThm
315
ref
refl
378
remove
70
remove
appThm
379
remove
27
ref
appTerm
betaConv
trans
appThm
appThm
absThm
appThm
absThm
appThm
appThm
sym
345
remove
assume
eqMp
eqMp
41
ref
224
remove
316
remove
nil
cons
cons
245
ref
312
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
264
remove
subst
proveHyp
eqMp
nil
136
ref
376
remove
cons
137
ref
364
remove
cons
nil
cons
380
def
cons
nil
cons
cons
149
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
136
ref
369
remove
cons
380
ref
cons
nil
cons
cons
149
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
136
ref
367
remove
cons
380
ref
cons
nil
cons
cons
149
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
99
remove
266
remove
245
remove
101
ref
346
remove
267
remove
appTerm
appTerm
363
ref
appTerm
absTerm
appTerm
nil
cons
cons
100
remove
101
remove
347
remove
appTerm
363
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
156
remove
subst
proveHyp
41
remove
361
remove
380
remove
cons
nil
cons
cons
279
remove
subst
eqMp
eqMp
proveHyp
eqMp
eqMp
defineConstList
381
def
pop
382
def
pop
381
ref
nil
136
remove
7
ref
9
ref
18
ref
382
remove
hdTl
pop
12
ref
constTerm
383
def
20
ref
appTerm
384
def
22
remove
appTerm
appTerm
314
remove
appTerm
absTerm
appTerm
385
def
nil
cons
cons
137
remove
7
ref
9
ref
7
ref
24
ref
18
ref
384
ref
28
remove
appTerm
appTerm
315
remove
384
remove
27
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
386
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
387
def
149
remove
subst
proveHyp
nil
385
remove
thm
nil
237
ref
9
ref
7
ref
24
ref
18
ref
"Number.Natural.>"
"_1967"
2
ref
var
388
def
"_1968"
2
ref
var
389
def
302
ref
389
ref
varTerm
390
def
appTerm
388
ref
varTerm
391
def
appTerm
392
def
absTerm
393
def
absTerm
394
def
defineConst
395
def
pop
12
ref
constTerm
396
def
20
ref
appTerm
27
ref
appTerm
appTerm
302
remove
27
ref
appTerm
20
ref
appTerm
appTerm
absTerm
appTerm
absTerm
397
def
nil
cons
cons
nil
cons
nil
cons
cons
239
ref
subst
388
remove
nil
10
ref
7
ref
389
ref
18
ref
396
remove
391
ref
appTerm
390
ref
appTerm
appTerm
392
remove
appTerm
398
def
absTerm
399
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
132
ref
subst
nil
237
ref
399
remove
nil
cons
cons
nil
cons
nil
cons
cons
239
ref
subst
389
remove
nil
10
ref
398
remove
nil
cons
cons
nil
cons
nil
cons
cons
132
ref
subst
395
remove
391
ref
refl
appThm
394
remove
391
remove
appTerm
betaConv
trans
390
ref
refl
appThm
393
remove
390
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
7
ref
397
remove
appTerm
thm
nil
237
ref
9
remove
7
ref
24
remove
18
ref
"Number.Natural.>="
"_1955"
2
ref
var
400
def
"_1956"
2
remove
var
401
def
383
ref
401
ref
varTerm
402
def
appTerm
400
ref
varTerm
403
def
appTerm
404
def
absTerm
405
def
absTerm
406
def
defineConst
407
def
pop
12
remove
constTerm
408
def
20
ref
appTerm
27
ref
appTerm
appTerm
383
remove
27
remove
appTerm
20
remove
appTerm
appTerm
absTerm
appTerm
absTerm
409
def
nil
cons
cons
nil
cons
nil
cons
cons
239
ref
subst
400
remove
nil
10
ref
7
ref
401
ref
18
remove
408
remove
403
ref
appTerm
402
ref
appTerm
appTerm
404
remove
appTerm
410
def
absTerm
411
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
132
ref
subst
nil
237
remove
411
remove
nil
cons
cons
nil
cons
nil
cons
cons
239
remove
subst
401
remove
nil
10
remove
410
remove
nil
cons
cons
nil
cons
nil
cons
cons
132
remove
subst
407
remove
403
ref
refl
appThm
406
remove
403
remove
appTerm
betaConv
trans
402
ref
refl
appThm
405
remove
402
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
7
remove
409
remove
appTerm
thm
301
remove
310
remove
241
ref
subst
proveHyp
nil
309
remove
thm
381
remove
387
remove
241
remove
subst
proveHyp
nil
386
remove
thm