6
version
nil
"P"
"->"
typeOp
0
def
"Parser.parser"
typeOp
1
def
"A"
varType
2
def
"B"
varType
3
def
nil
cons
4
def
cons
5
def
opType
6
def
"bool"
typeOp
nil
opType
7
def
nil
cons
8
def
cons
opType
9
def
var
10
def
"p"
6
ref
var
11
def
"Data.Bool.!"
const
12
def
0
ref
0
ref
"Parser.Stream.stream"
typeOp
13
def
2
ref
nil
cons
14
def
opType
15
def
8
ref
cons
opType
16
def
8
ref
cons
opType
17
def
constTerm
18
def
"xs"
15
ref
var
19
def
"Number.Natural.<="
const
0
ref
"Number.Natural.natural"
typeOp
nil
opType
20
def
0
ref
20
ref
8
ref
cons
opType
21
def
nil
cons
cons
opType
22
def
constTerm
23
def
"Parser.Stream.length"
const
24
def
0
ref
13
ref
4
ref
opType
25
def
20
ref
nil
cons
26
def
cons
opType
constTerm
27
def
"Parser.parse"
const
28
def
0
ref
6
ref
0
ref
15
ref
25
ref
nil
cons
29
def
cons
opType
30
def
nil
cons
31
def
cons
opType
constTerm
11
ref
varTerm
32
def
appTerm
33
def
19
ref
varTerm
34
def
appTerm
35
def
appTerm
appTerm
24
remove
0
ref
15
ref
26
ref
cons
opType
constTerm
36
def
34
ref
appTerm
37
def
appTerm
38
def
absTerm
39
def
appTerm
40
def
absTerm
41
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
6
ref
nil
cons
cons
nil
cons
42
def
nil
nil
cons
43
def
cons
44
def
"="
const
45
def
0
ref
7
ref
0
ref
7
ref
8
ref
cons
opType
46
def
nil
cons
cons
opType
47
def
constTerm
48
def
12
ref
0
ref
0
ref
2
ref
8
ref
cons
opType
49
def
8
ref
cons
opType
50
def
constTerm
51
def
"P"
49
ref
var
52
def
varTerm
53
def
appTerm
54
def
appTerm
refl
"p"
49
ref
var
55
def
45
ref
0
ref
49
ref
50
ref
nil
cons
cons
opType
constTerm
55
ref
varTerm
56
def
appTerm
"x"
2
ref
var
57
def
"Data.Bool.T"
const
7
ref
constTerm
58
def
absTerm
59
def
appTerm
absTerm
60
def
53
ref
appTerm
betaConv
61
def
appThm
nil
45
ref
0
ref
50
ref
0
ref
50
ref
8
ref
cons
opType
62
def
nil
cons
cons
opType
constTerm
63
def
51
ref
appTerm
60
remove
appTerm
axiom
53
ref
refl
64
def
appThm
65
def
eqMp
sym
66
def
subst
67
def
subst
11
ref
nil
"t"
7
ref
var
68
def
40
remove
nil
cons
69
def
cons
nil
cons
nil
cons
cons
48
ref
68
ref
varTerm
70
def
appTerm
58
ref
appTerm
assume
sym
nil
58
ref
axiom
71
def
eqMp
70
ref
assume
71
ref
deductAntisym
deductAntisym
72
def
subst
nil
"P"
16
ref
var
73
def
19
ref
"Data.Bool.==>"
const
47
ref
constTerm
74
def
18
ref
"ys"
15
ref
var
75
def
74
ref
"Parser.Stream.isProperSuffix"
const
0
ref
15
ref
16
ref
nil
cons
76
def
cons
opType
77
def
constTerm
78
def
75
ref
varTerm
79
def
appTerm
80
def
34
ref
appTerm
81
def
appTerm
82
def
23
ref
27
ref
33
ref
79
ref
appTerm
83
def
appTerm
84
def
appTerm
85
def
36
ref
79
ref
appTerm
86
def
appTerm
87
def
appTerm
absTerm
appTerm
appTerm
38
remove
appTerm
88
def
absTerm
89
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
15
ref
nil
cons
90
def
cons
nil
cons
91
def
43
ref
cons
92
def
66
ref
subst
93
def
subst
19
ref
nil
68
ref
88
ref
nil
cons
94
def
cons
nil
cons
nil
cons
cons
72
ref
subst
19
ref
"Data.Bool.\\/"
const
47
ref
constTerm
95
def
45
ref
77
ref
constTerm
96
def
34
ref
appTerm
97
def
"Parser.Stream.error"
const
98
def
15
ref
constTerm
99
def
appTerm
100
def
appTerm
95
ref
97
ref
"Parser.Stream.eof"
const
101
def
15
ref
constTerm
102
def
appTerm
103
def
appTerm
"Data.Bool.?"
const
104
def
50
ref
constTerm
105
def
57
ref
104
ref
17
ref
constTerm
106
def
"xt"
15
ref
var
107
def
97
ref
"Parser.Stream.cons"
const
108
def
0
ref
2
ref
0
ref
15
ref
90
ref
cons
opType
nil
cons
109
def
cons
opType
constTerm
110
def
57
ref
varTerm
111
def
appTerm
112
def
107
ref
varTerm
113
def
appTerm
114
def
appTerm
115
def
absTerm
116
def
appTerm
117
def
absTerm
118
def
appTerm
119
def
appTerm
120
def
appTerm
121
def
absTerm
122
def
34
ref
appTerm
123
def
betaConv
nil
18
ref
122
ref
appTerm
124
def
axiom
nil
"p"
7
ref
var
125
def
124
remove
nil
cons
cons
"q"
7
ref
var
126
def
123
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
48
ref
74
ref
125
ref
varTerm
127
def
appTerm
128
def
126
ref
varTerm
129
def
appTerm
130
def
appTerm
131
def
refl
125
ref
126
ref
48
ref
"Data.Bool./\\"
const
47
ref
constTerm
132
def
127
ref
appTerm
133
def
129
ref
appTerm
134
def
appTerm
135
def
127
ref
appTerm
absTerm
136
def
absTerm
137
def
127
ref
appTerm
betaConv
129
ref
refl
138
def
appThm
136
remove
129
ref
appTerm
betaConv
trans
appThm
nil
45
ref
0
ref
47
ref
0
ref
47
ref
8
ref
cons
opType
139
def
nil
cons
cons
opType
constTerm
140
def
74
ref
appTerm
137
remove
appTerm
axiom
127
ref
refl
141
def
appThm
138
ref
appThm
eqMp
142
def
sym
143
def
135
remove
refl
126
ref
45
ref
0
ref
139
ref
0
ref
139
remove
8
ref
cons
opType
nil
cons
cons
opType
constTerm
144
def
"f"
47
remove
var
145
def
145
ref
varTerm
146
def
127
ref
appTerm
129
ref
appTerm
absTerm
147
def
appTerm
145
ref
146
ref
58
ref
appTerm
58
ref
appTerm
absTerm
148
def
appTerm
absTerm
149
def
129
ref
appTerm
betaConv
appThm
45
ref
0
ref
46
ref
0
ref
46
ref
8
ref
cons
opType
150
def
nil
cons
cons
opType
constTerm
151
def
133
remove
appTerm
refl
125
ref
149
remove
absTerm
152
def
127
ref
appTerm
betaConv
appThm
nil
140
ref
132
ref
appTerm
152
ref
appTerm
axiom
153
def
141
ref
appThm
eqMp
138
ref
appThm
eqMp
154
def
sym
145
ref
146
ref
refl
nil
68
ref
127
ref
nil
cons
155
def
cons
nil
cons
nil
cons
cons
156
def
72
ref
subst
127
ref
assume
157
def
eqMp
appThm
nil
68
ref
129
ref
nil
cons
158
def
cons
nil
cons
nil
cons
cons
72
ref
subst
129
ref
assume
159
def
eqMp
appThm
absThm
eqMp
160
def
nil
"P"
7
ref
var
161
def
155
ref
cons
"Q"
7
ref
var
162
def
158
ref
cons
nil
cons
163
def
cons
nil
cons
cons
48
ref
refl
164
def
145
ref
146
remove
161
ref
varTerm
165
def
appTerm
166
def
162
ref
varTerm
167
def
appTerm
absTerm
168
def
125
ref
126
ref
127
ref
absTerm
absTerm
169
def
appTerm
betaConv
169
ref
165
ref
appTerm
betaConv
167
ref
refl
170
def
appThm
126
ref
165
ref
absTerm
167
ref
appTerm
betaConv
trans
trans
appThm
148
ref
169
ref
appTerm
betaConv
169
ref
58
ref
appTerm
betaConv
58
ref
refl
171
def
appThm
126
ref
58
ref
absTerm
58
ref
appTerm
betaConv
trans
trans
appThm
48
ref
132
ref
165
ref
appTerm
172
def
167
ref
appTerm
173
def
appTerm
refl
126
ref
144
remove
145
remove
166
remove
129
ref
appTerm
absTerm
appTerm
148
ref
appTerm
absTerm
167
ref
appTerm
betaConv
appThm
151
ref
172
remove
appTerm
refl
152
remove
165
ref
appTerm
betaConv
appThm
153
remove
165
ref
refl
174
def
appThm
eqMp
170
ref
appThm
eqMp
173
remove
assume
eqMp
175
def
169
remove
refl
appThm
eqMp
sym
71
ref
eqMp
176
def
subst
177
def
deductAntisym
eqMp
142
remove
130
ref
assume
eqMp
sym
157
ref
eqMp
164
ref
147
remove
125
ref
126
ref
129
ref
absTerm
178
def
absTerm
179
def
appTerm
betaConv
179
ref
127
ref
appTerm
betaConv
138
remove
appThm
178
ref
129
ref
appTerm
betaConv
trans
trans
appThm
148
remove
179
ref
appTerm
betaConv
179
ref
58
ref
appTerm
betaConv
171
remove
appThm
178
ref
58
ref
appTerm
betaConv
trans
trans
180
def
appThm
154
remove
134
remove
assume
eqMp
179
ref
refl
181
def
appThm
eqMp
sym
71
ref
eqMp
182
def
proveHyp
183
def
deductAntisym
184
def
subst
proveHyp
91
ref
73
ref
122
remove
nil
cons
cons
"x"
15
ref
var
185
def
34
ref
nil
cons
186
def
cons
nil
cons
187
def
cons
nil
cons
cons
nil
125
ref
54
ref
nil
cons
188
def
cons
126
ref
53
ref
111
ref
appTerm
189
def
nil
cons
190
def
cons
nil
cons
cons
nil
cons
cons
191
def
143
ref
subst
191
remove
182
remove
160
remove
deductAntisym
192
def
subst
48
ref
189
ref
appTerm
refl
59
remove
111
ref
appTerm
betaConv
appThm
61
remove
65
remove
54
remove
assume
eqMp
eqMp
111
ref
refl
193
def
appThm
eqMp
sym
71
ref
eqMp
eqMp
nil
161
ref
188
remove
cons
162
ref
190
ref
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
194
def
subst
eqMp
eqMp
195
def
nil
125
ref
121
remove
nil
cons
196
def
cons
197
def
126
ref
94
ref
cons
nil
cons
198
def
cons
nil
cons
cons
199
def
184
ref
subst
proveHyp
199
ref
143
ref
subst
199
remove
192
ref
subst
nil
125
ref
120
remove
nil
cons
200
def
cons
201
def
198
ref
cons
nil
cons
cons
202
def
143
ref
subst
202
remove
192
ref
subst
nil
52
ref
57
ref
74
ref
118
ref
111
ref
appTerm
203
def
appTerm
204
def
88
ref
appTerm
205
def
absTerm
206
def
nil
cons
cons
nil
cons
nil
cons
cons
66
ref
subst
57
ref
nil
68
ref
205
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
203
ref
nil
cons
207
def
cons
208
def
198
ref
cons
nil
cons
cons
209
def
143
ref
subst
209
remove
192
ref
subst
203
ref
betaConv
203
remove
assume
eqMp
210
def
nil
125
ref
117
ref
nil
cons
cons
211
def
198
ref
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
73
ref
107
ref
74
ref
116
ref
113
ref
appTerm
212
def
appTerm
213
def
88
ref
appTerm
214
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
107
ref
nil
68
ref
214
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
212
ref
nil
cons
215
def
cons
216
def
198
ref
cons
nil
cons
cons
217
def
143
ref
subst
217
remove
192
ref
subst
212
ref
betaConv
212
remove
assume
eqMp
218
def
nil
125
ref
115
ref
nil
cons
219
def
cons
220
def
198
ref
cons
nil
cons
cons
221
def
184
ref
subst
proveHyp
221
ref
143
ref
subst
221
remove
192
ref
subst
48
ref
"_32470"
15
ref
var
222
def
74
ref
18
ref
75
ref
74
ref
80
ref
222
remove
varTerm
223
def
appTerm
appTerm
87
ref
appTerm
absTerm
appTerm
appTerm
23
ref
27
ref
33
ref
223
ref
appTerm
appTerm
appTerm
36
ref
223
remove
appTerm
appTerm
appTerm
absTerm
224
def
34
ref
appTerm
225
def
appTerm
refl
226
def
224
remove
114
ref
appTerm
betaConv
appThm
164
ref
225
remove
betaConv
appThm
227
def
74
ref
18
ref
75
ref
74
ref
80
ref
114
ref
appTerm
228
def
appTerm
229
def
87
ref
appTerm
absTerm
230
def
appTerm
231
def
appTerm
23
ref
27
ref
33
ref
114
ref
appTerm
232
def
appTerm
appTerm
36
ref
114
ref
appTerm
233
def
appTerm
234
def
appTerm
refl
appThm
trans
89
ref
refl
235
def
115
remove
assume
236
def
appThm
eqMp
sym
nil
125
ref
231
remove
nil
cons
237
def
cons
238
def
126
ref
234
remove
nil
cons
239
def
cons
nil
cons
cons
nil
cons
cons
240
def
143
ref
subst
240
remove
192
ref
subst
23
ref
refl
241
def
27
ref
refl
242
def
nil
19
ref
113
ref
nil
cons
243
def
cons
244
def
nil
cons
nil
cons
cons
245
def
19
ref
45
ref
0
ref
25
ref
0
ref
25
ref
8
ref
cons
opType
nil
cons
cons
opType
constTerm
246
def
33
ref
112
remove
34
ref
appTerm
247
def
appTerm
appTerm
"Data.Option.case.none.some"
const
248
def
0
ref
25
ref
0
ref
0
ref
"Data.Pair.*"
typeOp
249
def
3
ref
90
ref
cons
opType
250
def
29
ref
cons
opType
251
def
0
ref
"Data.Option.option"
typeOp
252
def
250
ref
nil
cons
253
def
opType
254
def
29
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
255
def
98
ref
25
ref
constTerm
256
def
appTerm
"select"
const
257
def
0
ref
0
ref
251
ref
8
ref
cons
opType
258
def
251
ref
nil
cons
259
def
cons
opType
constTerm
260
def
"f"
251
ref
var
261
def
12
ref
0
ref
0
ref
3
ref
8
ref
cons
opType
262
def
8
ref
cons
opType
263
def
constTerm
264
def
"y"
3
ref
var
265
def
18
ref
75
ref
246
ref
261
ref
varTerm
"Data.Pair.,"
const
266
def
0
ref
3
ref
0
ref
15
ref
253
ref
cons
opType
nil
cons
cons
opType
constTerm
267
def
265
ref
varTerm
268
def
appTerm
79
ref
appTerm
269
def
appTerm
appTerm
108
ref
0
ref
3
ref
0
ref
25
ref
29
ref
cons
opType
nil
cons
270
def
cons
opType
constTerm
271
def
268
ref
appTerm
272
def
83
ref
appTerm
273
def
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
274
def
appTerm
275
def
"Parser.dest"
const
276
def
0
ref
6
ref
0
ref
2
ref
0
ref
15
ref
254
ref
nil
cons
277
def
cons
opType
nil
cons
278
def
cons
opType
nil
cons
cons
opType
constTerm
32
ref
appTerm
279
def
111
ref
appTerm
280
def
34
ref
appTerm
281
def
appTerm
appTerm
absTerm
282
def
34
ref
appTerm
283
def
betaConv
57
ref
18
ref
282
ref
appTerm
284
def
absTerm
285
def
111
ref
appTerm
286
def
betaConv
11
ref
132
ref
246
ref
33
ref
99
ref
appTerm
287
def
appTerm
288
def
256
ref
appTerm
289
def
appTerm
132
ref
246
ref
33
ref
102
ref
appTerm
290
def
appTerm
291
def
101
ref
25
ref
constTerm
292
def
appTerm
293
def
appTerm
51
ref
285
ref
appTerm
294
def
appTerm
295
def
appTerm
absTerm
296
def
32
ref
appTerm
297
def
betaConv
132
ref
12
ref
0
ref
9
ref
8
ref
cons
opType
constTerm
298
def
11
ref
289
ref
absTerm
299
def
appTerm
300
def
appTerm
301
def
refl
164
ref
132
ref
refl
302
def
298
ref
refl
303
def
11
ref
11
ref
293
ref
absTerm
304
def
32
ref
appTerm
betaConv
305
def
absThm
appThm
appThm
303
ref
11
ref
11
ref
294
ref
absTerm
306
def
32
ref
appTerm
betaConv
307
def
absThm
appThm
appThm
appThm
303
ref
11
ref
302
ref
305
remove
appThm
307
remove
appThm
absThm
appThm
appThm
nil
"p"
9
ref
var
308
def
304
ref
nil
cons
cons
"q"
9
remove
var
309
def
306
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
44
remove
"q"
49
ref
var
310
def
48
ref
132
ref
51
ref
57
ref
56
ref
111
ref
appTerm
311
def
absTerm
312
def
appTerm
appTerm
51
ref
57
ref
310
ref
varTerm
313
def
111
ref
appTerm
314
def
absTerm
appTerm
appTerm
315
def
appTerm
51
ref
57
ref
132
ref
311
ref
appTerm
314
remove
appTerm
absTerm
appTerm
316
def
appTerm
317
def
absTerm
318
def
313
ref
appTerm
319
def
betaConv
55
ref
12
ref
62
remove
constTerm
320
def
318
ref
appTerm
321
def
absTerm
322
def
56
ref
appTerm
323
def
betaConv
320
ref
refl
324
def
55
ref
324
remove
310
ref
317
remove
assume
sym
48
ref
316
remove
appTerm
315
remove
appTerm
325
def
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
nil
320
ref
55
ref
320
ref
310
remove
325
remove
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
125
ref
320
ref
322
ref
appTerm
nil
cons
cons
126
ref
323
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
"A"
49
ref
nil
cons
326
def
cons
nil
cons
327
def
"P"
50
remove
var
328
def
322
remove
nil
cons
cons
"x"
49
ref
var
329
def
56
ref
nil
cons
330
def
cons
nil
cons
331
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
321
remove
nil
cons
cons
126
ref
319
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
327
ref
328
ref
318
remove
nil
cons
cons
329
remove
313
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
332
def
subst
eqMp
appThm
164
ref
302
ref
303
ref
11
ref
299
ref
32
ref
appTerm
betaConv
333
def
absThm
appThm
appThm
303
ref
11
ref
11
ref
295
ref
absTerm
334
def
32
ref
appTerm
betaConv
335
def
absThm
appThm
appThm
appThm
303
ref
11
ref
302
ref
333
remove
appThm
335
remove
appThm
absThm
appThm
appThm
nil
308
ref
299
remove
nil
cons
cons
309
ref
334
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
332
ref
subst
eqMp
trans
nil
300
ref
axiom
nil
125
ref
300
remove
nil
cons
cons
126
ref
132
ref
298
ref
304
remove
appTerm
336
def
appTerm
298
ref
306
remove
appTerm
337
def
appTerm
338
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
192
ref
subst
proveHyp
nil
336
ref
axiom
nil
125
ref
336
remove
nil
cons
cons
126
ref
337
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
192
ref
subst
proveHyp
nil
337
remove
axiom
eqMp
eqMp
339
def
eqMp
nil
125
ref
298
ref
296
ref
appTerm
nil
cons
cons
126
ref
297
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
42
ref
10
ref
296
remove
nil
cons
cons
"x"
6
ref
var
32
ref
nil
cons
cons
nil
cons
340
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
341
def
nil
161
ref
289
remove
nil
cons
cons
162
ref
295
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
342
def
164
ref
168
remove
179
ref
appTerm
betaConv
179
remove
165
ref
appTerm
betaConv
170
ref
appThm
178
remove
167
ref
appTerm
betaConv
trans
trans
appThm
180
remove
appThm
175
remove
181
remove
appThm
eqMp
sym
71
ref
eqMp
343
def
subst
proveHyp
344
def
nil
161
ref
293
remove
nil
cons
cons
162
ref
294
remove
nil
cons
345
def
cons
nil
cons
cons
nil
cons
cons
346
def
343
ref
subst
proveHyp
nil
125
ref
345
remove
cons
126
ref
286
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
"A"
14
ref
cons
347
def
nil
cons
348
def
52
ref
285
remove
nil
cons
cons
57
ref
111
ref
nil
cons
349
def
cons
nil
cons
350
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
284
remove
nil
cons
cons
126
ref
283
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
282
remove
nil
cons
cons
187
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
351
def
subst
352
def
appThm
appThm
233
ref
refl
353
def
appThm
sym
19
ref
95
ref
45
ref
0
ref
254
ref
0
ref
254
ref
8
ref
cons
opType
nil
cons
cons
opType
constTerm
354
def
281
ref
appTerm
355
def
"Data.Option.none"
const
356
def
254
ref
constTerm
357
def
appTerm
appTerm
104
ref
263
remove
constTerm
358
def
265
ref
106
ref
75
ref
132
ref
355
remove
"Data.Option.some"
const
359
def
0
ref
250
ref
277
ref
cons
opType
constTerm
360
def
269
ref
appTerm
361
def
appTerm
appTerm
"Parser.Stream.isSuffix"
const
77
remove
constTerm
362
def
79
ref
appTerm
363
def
34
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
364
def
113
ref
appTerm
365
def
betaConv
57
ref
18
ref
364
ref
appTerm
366
def
absTerm
367
def
111
ref
appTerm
368
def
betaConv
11
ref
51
ref
367
ref
appTerm
369
def
absTerm
370
def
32
ref
appTerm
371
def
betaConv
nil
298
ref
370
ref
appTerm
372
def
axiom
nil
125
ref
372
remove
nil
cons
cons
126
ref
371
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
42
ref
10
ref
370
remove
nil
cons
cons
340
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
369
remove
nil
cons
cons
126
ref
368
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
367
remove
nil
cons
cons
350
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
366
remove
nil
cons
cons
126
ref
365
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
364
remove
nil
cons
cons
185
ref
243
ref
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
373
def
nil
125
ref
95
ref
354
ref
280
remove
113
ref
appTerm
374
def
appTerm
375
def
357
ref
appTerm
376
def
appTerm
358
ref
265
ref
106
ref
75
ref
132
ref
375
ref
361
ref
appTerm
377
def
appTerm
363
remove
113
ref
appTerm
378
def
appTerm
379
def
absTerm
380
def
appTerm
381
def
absTerm
382
def
appTerm
383
def
appTerm
nil
cons
384
def
cons
385
def
126
ref
23
ref
27
ref
275
ref
374
ref
appTerm
386
def
appTerm
appTerm
233
remove
appTerm
387
def
nil
cons
388
def
cons
nil
cons
389
def
cons
nil
cons
cons
390
def
184
ref
subst
proveHyp
390
ref
143
ref
subst
390
remove
192
ref
subst
nil
"P"
262
ref
var
391
def
265
ref
74
ref
382
ref
268
ref
appTerm
392
def
appTerm
393
def
387
ref
appTerm
394
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
4
ref
cons
395
def
nil
cons
396
def
43
ref
cons
397
def
66
ref
subst
398
def
subst
265
ref
nil
68
ref
394
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
392
ref
nil
cons
399
def
cons
400
def
389
ref
cons
nil
cons
cons
401
def
143
ref
subst
401
remove
192
ref
subst
392
ref
betaConv
392
remove
assume
eqMp
402
def
nil
125
ref
381
ref
nil
cons
cons
403
def
389
ref
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
73
ref
75
ref
74
ref
380
ref
79
ref
appTerm
404
def
appTerm
405
def
387
ref
appTerm
406
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
75
ref
nil
68
ref
406
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
404
ref
nil
cons
407
def
cons
408
def
389
ref
cons
nil
cons
cons
409
def
143
ref
subst
409
remove
192
ref
subst
404
ref
betaConv
404
remove
assume
eqMp
410
def
nil
125
ref
379
remove
nil
cons
411
def
cons
412
def
389
ref
cons
nil
cons
cons
413
def
184
ref
subst
proveHyp
413
ref
143
ref
subst
413
remove
192
ref
subst
nil
161
ref
377
ref
nil
cons
cons
162
ref
378
ref
nil
cons
414
def
cons
nil
cons
cons
nil
cons
cons
415
def
176
ref
subst
416
def
415
remove
343
ref
subst
417
def
241
ref
242
ref
275
ref
refl
418
def
377
remove
assume
419
def
appThm
nil
"a"
250
ref
var
420
def
269
ref
nil
cons
cons
421
def
261
remove
274
ref
nil
cons
cons
422
def
"b"
25
ref
var
423
def
256
ref
nil
cons
424
def
cons
nil
cons
cons
425
def
cons
nil
cons
cons
"A"
253
remove
cons
426
def
"B"
29
ref
cons
nil
cons
427
def
cons
43
ref
cons
428
def
"a"
2
ref
var
429
def
45
ref
0
ref
3
ref
262
remove
nil
cons
cons
opType
constTerm
430
def
248
ref
0
ref
3
ref
0
ref
0
ref
5
ref
opType
431
def
0
ref
252
ref
14
ref
opType
432
def
4
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
"b"
3
ref
var
433
def
varTerm
434
def
appTerm
"f"
431
ref
var
435
def
varTerm
436
def
appTerm
437
def
359
ref
0
ref
2
ref
432
ref
nil
cons
cons
opType
constTerm
438
def
429
ref
varTerm
439
def
appTerm
440
def
appTerm
appTerm
436
ref
439
ref
appTerm
appTerm
absTerm
441
def
439
ref
appTerm
442
def
betaConv
435
ref
51
ref
441
ref
appTerm
443
def
absTerm
444
def
436
ref
appTerm
445
def
betaConv
433
ref
12
ref
0
ref
0
ref
431
ref
8
ref
cons
opType
446
def
8
ref
cons
opType
constTerm
447
def
444
ref
appTerm
448
def
absTerm
449
def
434
ref
appTerm
450
def
betaConv
nil
264
ref
449
ref
appTerm
451
def
axiom
nil
125
ref
451
remove
nil
cons
cons
126
ref
450
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
391
ref
449
remove
nil
cons
cons
"x"
3
ref
var
452
def
434
ref
nil
cons
cons
nil
cons
453
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
448
remove
nil
cons
cons
126
ref
445
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
"A"
431
ref
nil
cons
cons
nil
cons
454
def
"P"
446
ref
var
455
def
444
remove
nil
cons
cons
"x"
431
ref
var
456
def
436
ref
nil
cons
cons
nil
cons
457
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
443
remove
nil
cons
cons
126
ref
442
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
441
remove
nil
cons
cons
57
ref
439
ref
nil
cons
cons
nil
cons
458
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
459
def
subst
460
def
subst
75
ref
246
ref
260
remove
"_32368"
251
ref
var
461
def
264
ref
265
ref
18
ref
75
ref
246
ref
461
remove
varTerm
269
ref
appTerm
appTerm
273
ref
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
462
def
appTerm
463
def
269
ref
appTerm
appTerm
273
ref
appTerm
absTerm
464
def
79
ref
appTerm
465
def
betaConv
265
ref
18
ref
464
ref
appTerm
466
def
absTerm
467
def
268
ref
appTerm
468
def
betaConv
462
ref
463
remove
appTerm
469
def
betaConv
462
ref
"_32366"
250
ref
var
470
def
271
ref
257
ref
0
ref
0
ref
0
ref
250
ref
4
ref
cons
opType
471
def
8
ref
cons
opType
471
ref
nil
cons
cons
opType
constTerm
"fn"
471
remove
var
472
def
264
ref
"a"
3
ref
var
473
def
18
ref
"b"
15
ref
var
474
def
430
ref
472
remove
varTerm
267
ref
473
ref
varTerm
475
def
appTerm
474
ref
varTerm
476
def
appTerm
477
def
appTerm
appTerm
475
remove
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
478
def
470
remove
varTerm
479
def
appTerm
appTerm
33
ref
257
ref
0
ref
0
ref
0
ref
250
ref
90
ref
cons
opType
480
def
8
ref
cons
opType
480
ref
nil
cons
cons
opType
constTerm
"fn"
480
remove
var
481
def
264
ref
473
ref
18
ref
474
ref
96
ref
481
remove
varTerm
477
remove
appTerm
appTerm
476
ref
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
482
def
479
remove
appTerm
appTerm
appTerm
absTerm
483
def
appTerm
betaConv
sym
nil
391
ref
265
ref
18
ref
75
ref
246
ref
483
ref
269
ref
appTerm
484
def
appTerm
273
remove
appTerm
485
def
absTerm
486
def
appTerm
487
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
398
ref
subst
265
ref
nil
68
ref
487
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
73
ref
486
remove
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
75
ref
nil
68
ref
485
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
484
remove
betaConv
246
ref
"_32363"
15
ref
var
488
def
272
remove
33
ref
488
ref
varTerm
appTerm
489
def
appTerm
absTerm
79
ref
appTerm
490
def
appTerm
refl
488
ref
271
ref
478
ref
269
ref
appTerm
491
def
appTerm
492
def
489
ref
appTerm
absTerm
493
def
482
ref
269
ref
appTerm
494
def
appTerm
betaConv
appThm
246
ref
refl
495
def
490
remove
betaConv
appThm
492
remove
33
ref
494
ref
appTerm
appTerm
refl
appThm
trans
45
ref
0
ref
30
ref
0
ref
30
remove
8
ref
cons
opType
nil
cons
cons
opType
constTerm
496
def
"_32362"
3
ref
var
497
def
488
remove
271
ref
497
remove
varTerm
appTerm
489
remove
appTerm
absTerm
absTerm
498
def
268
ref
appTerm
499
def
appTerm
refl
498
ref
491
ref
appTerm
betaConv
appThm
496
remove
refl
499
remove
betaConv
appThm
493
remove
refl
appThm
trans
498
remove
refl
nil
474
ref
79
ref
nil
cons
500
def
cons
501
def
473
remove
268
ref
nil
cons
502
def
cons
nil
cons
cons
503
def
nil
cons
cons
504
def
395
ref
"B"
90
ref
cons
nil
cons
505
def
cons
43
ref
cons
506
def
433
ref
45
ref
0
ref
2
ref
326
remove
cons
opType
constTerm
507
def
257
ref
0
ref
0
ref
0
ref
249
ref
5
remove
opType
508
def
14
ref
cons
opType
509
def
8
ref
cons
opType
510
def
509
ref
nil
cons
511
def
cons
opType
constTerm
"fn"
509
remove
var
512
def
51
ref
429
ref
264
ref
433
ref
507
ref
512
ref
varTerm
266
ref
0
ref
2
ref
0
ref
3
ref
508
ref
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
513
def
439
ref
appTerm
434
ref
appTerm
514
def
appTerm
appTerm
515
def
439
ref
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
516
def
appTerm
517
def
514
ref
appTerm
appTerm
439
ref
appTerm
absTerm
518
def
434
ref
appTerm
519
def
betaConv
429
ref
264
ref
518
ref
appTerm
520
def
absTerm
521
def
439
ref
appTerm
522
def
betaConv
516
ref
517
remove
appTerm
523
def
betaConv
104
ref
0
ref
510
ref
8
ref
cons
opType
constTerm
524
def
refl
512
remove
51
ref
refl
525
def
429
ref
264
ref
refl
526
def
433
ref
515
remove
refl
429
ref
433
ref
439
ref
absTerm
527
def
absTerm
528
def
439
ref
appTerm
betaConv
434
ref
refl
529
def
appThm
527
remove
434
ref
appTerm
betaConv
trans
appThm
absThm
appThm
absThm
appThm
absThm
appThm
"C"
14
ref
cons
nil
cons
"_1343"
0
ref
2
ref
0
ref
3
ref
14
ref
cons
opType
nil
cons
cons
opType
var
528
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
"f"
0
ref
2
ref
0
ref
3
ref
"C"
varType
530
def
nil
cons
531
def
cons
opType
532
def
nil
cons
533
def
cons
opType
534
def
var
535
def
429
ref
433
ref
"_1343"
534
ref
var
varTerm
439
ref
appTerm
434
ref
appTerm
536
def
absTerm
537
def
absTerm
538
def
nil
cons
cons
nil
cons
nil
cons
cons
535
ref
104
ref
0
ref
0
ref
0
ref
508
ref
531
ref
cons
opType
539
def
8
ref
cons
opType
540
def
8
ref
cons
opType
541
def
constTerm
542
def
"fn"
539
ref
var
543
def
51
ref
429
ref
264
ref
433
ref
45
ref
0
ref
530
ref
0
ref
530
ref
8
ref
cons
opType
544
def
nil
cons
cons
opType
constTerm
545
def
543
ref
varTerm
546
def
514
ref
appTerm
appTerm
547
def
535
remove
varTerm
548
def
439
ref
appTerm
434
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
549
def
548
ref
appTerm
550
def
betaConv
nil
12
ref
0
ref
0
ref
534
ref
8
ref
cons
opType
551
def
8
ref
cons
opType
constTerm
549
ref
appTerm
552
def
axiom
nil
125
ref
552
remove
nil
cons
cons
126
ref
550
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
"A"
534
ref
nil
cons
cons
nil
cons
"P"
551
remove
var
549
remove
nil
cons
cons
"x"
534
remove
var
548
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
nil
125
ref
542
ref
543
ref
51
ref
429
ref
264
ref
433
ref
547
ref
538
remove
439
ref
appTerm
553
def
434
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
554
def
absTerm
555
def
appTerm
556
def
nil
cons
cons
126
ref
542
remove
543
ref
51
ref
429
ref
264
ref
433
ref
547
ref
536
remove
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
557
def
appTerm
558
def
nil
cons
559
def
cons
nil
cons
560
def
cons
nil
cons
cons
184
ref
subst
nil
"P"
540
remove
var
561
def
543
ref
74
ref
555
ref
546
ref
appTerm
562
def
appTerm
558
ref
appTerm
563
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
539
ref
nil
cons
cons
nil
cons
564
def
43
ref
cons
66
ref
subst
subst
543
remove
nil
68
ref
563
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
562
ref
nil
cons
565
def
cons
560
ref
cons
nil
cons
cons
566
def
143
ref
subst
566
remove
192
ref
subst
562
ref
betaConv
562
remove
assume
eqMp
nil
125
ref
554
ref
nil
cons
567
def
cons
560
remove
cons
nil
cons
cons
568
def
184
ref
subst
proveHyp
568
ref
143
ref
subst
568
remove
192
ref
subst
557
ref
546
ref
appTerm
betaConv
sym
525
ref
429
ref
526
ref
433
ref
547
remove
refl
553
remove
betaConv
529
ref
appThm
537
remove
434
ref
appTerm
betaConv
trans
appThm
absThm
appThm
absThm
appThm
554
remove
assume
eqMp
eqMp
564
ref
561
ref
557
remove
nil
cons
cons
"x"
539
remove
var
569
def
546
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
48
ref
105
ref
53
ref
appTerm
570
def
appTerm
571
def
refl
55
ref
12
ref
150
ref
constTerm
572
def
126
ref
74
ref
51
ref
57
ref
74
ref
311
ref
appTerm
573
def
129
ref
appTerm
absTerm
appTerm
appTerm
129
ref
appTerm
absTerm
appTerm
absTerm
574
def
53
remove
appTerm
betaConv
appThm
nil
63
remove
105
ref
appTerm
574
remove
appTerm
axiom
64
remove
appThm
eqMp
575
def
sym
nil
"P"
46
ref
var
576
def
162
ref
74
ref
51
ref
57
ref
74
ref
189
ref
appTerm
577
def
167
ref
appTerm
578
def
absTerm
579
def
appTerm
580
def
appTerm
581
def
167
ref
appTerm
582
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
8
ref
cons
nil
cons
583
def
43
ref
cons
66
ref
subst
584
def
subst
162
ref
nil
68
ref
582
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
580
ref
nil
cons
585
def
cons
586
def
126
ref
167
ref
nil
cons
587
def
cons
nil
cons
588
def
cons
nil
cons
cons
589
def
143
ref
subst
589
ref
192
ref
subst
nil
125
ref
190
ref
cons
588
ref
cons
nil
cons
cons
590
def
184
ref
subst
591
def
579
ref
111
ref
appTerm
592
def
betaConv
nil
586
ref
126
ref
592
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
348
ref
52
ref
579
remove
nil
cons
cons
593
def
350
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
594
def
eqMp
eqMp
nil
161
ref
585
ref
cons
595
def
162
ref
587
ref
cons
nil
cons
596
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
597
def
subst
proveHyp
eqMp
nil
161
ref
567
remove
cons
162
ref
559
remove
cons
nil
cons
598
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
161
ref
565
remove
cons
598
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
12
ref
541
remove
constTerm
569
ref
74
ref
555
ref
569
remove
varTerm
appTerm
appTerm
558
ref
appTerm
absTerm
appTerm
nil
cons
cons
126
ref
74
ref
556
remove
appTerm
558
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
564
remove
561
remove
555
remove
nil
cons
cons
598
remove
cons
nil
cons
cons
nil
586
ref
126
ref
74
ref
570
ref
appTerm
599
def
167
ref
appTerm
nil
cons
600
def
cons
nil
cons
cons
nil
cons
cons
601
def
143
ref
subst
601
remove
192
ref
subst
nil
125
ref
570
remove
nil
cons
602
def
cons
603
def
588
ref
cons
nil
cons
cons
604
def
143
ref
subst
604
remove
192
ref
subst
589
remove
184
ref
subst
126
ref
74
ref
51
ref
57
ref
577
remove
129
ref
appTerm
absTerm
appTerm
appTerm
129
ref
appTerm
absTerm
605
def
167
ref
appTerm
606
def
betaConv
nil
603
remove
126
ref
572
ref
605
ref
appTerm
607
def
nil
cons
608
def
cons
nil
cons
cons
nil
cons
cons
609
def
184
ref
subst
575
remove
nil
125
ref
571
remove
607
ref
appTerm
nil
cons
cons
126
ref
599
remove
607
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
609
remove
nil
125
ref
48
ref
127
ref
appTerm
610
def
129
ref
appTerm
611
def
nil
cons
612
def
cons
613
def
126
ref
130
ref
nil
cons
614
def
cons
nil
cons
615
def
cons
nil
cons
cons
616
def
143
ref
subst
616
remove
192
ref
subst
143
ref
192
ref
611
remove
assume
617
def
157
remove
eqMp
eqMp
177
ref
deductAntisym
eqMp
618
def
eqMp
nil
161
ref
612
remove
cons
619
def
162
ref
614
ref
cons
nil
cons
620
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
621
def
subst
eqMp
eqMp
nil
125
ref
608
remove
cons
126
ref
606
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
583
ref
576
ref
605
remove
nil
cons
cons
"x"
7
ref
var
622
def
587
remove
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
161
ref
602
remove
cons
596
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
nil
595
ref
162
ref
600
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
623
def
subst
eqMp
eqMp
proveHyp
624
def
subst
eqMp
nil
125
ref
524
remove
516
ref
appTerm
nil
cons
cons
126
ref
523
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
"A"
511
remove
cons
nil
cons
"p"
510
remove
var
516
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
125
ref
105
ref
56
ref
appTerm
625
def
nil
cons
626
def
cons
627
def
126
ref
48
ref
56
ref
257
ref
0
ref
49
ref
14
ref
cons
opType
constTerm
56
ref
appTerm
appTerm
628
def
appTerm
629
def
58
ref
appTerm
630
def
nil
cons
631
def
cons
nil
cons
632
def
cons
nil
cons
cons
633
def
143
ref
subst
633
remove
192
ref
subst
105
ref
refl
nil
"t"
49
remove
var
330
ref
cons
nil
cons
nil
cons
cons
347
ref
"B"
8
ref
cons
nil
cons
634
def
cons
43
ref
cons
"t"
431
ref
var
635
def
45
ref
0
ref
431
ref
446
remove
nil
cons
cons
opType
constTerm
57
ref
635
remove
varTerm
636
def
111
ref
appTerm
absTerm
appTerm
636
ref
appTerm
absTerm
637
def
636
ref
appTerm
638
def
betaConv
nil
447
ref
637
ref
appTerm
639
def
axiom
nil
125
ref
639
remove
nil
cons
cons
126
ref
638
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
454
ref
455
ref
637
remove
nil
cons
cons
456
remove
636
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
subst
appThm
nil
68
ref
626
ref
cons
nil
cons
nil
cons
cons
640
def
72
ref
subst
625
ref
assume
eqMp
trans
sym
71
ref
eqMp
nil
125
ref
105
ref
312
remove
appTerm
nil
cons
cons
632
ref
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
52
ref
330
remove
cons
162
ref
631
remove
cons
nil
cons
641
def
cons
nil
cons
cons
nil
586
remove
126
ref
74
ref
105
ref
57
ref
189
ref
absTerm
642
def
appTerm
643
def
appTerm
167
ref
appTerm
644
def
nil
cons
645
def
cons
nil
cons
646
def
cons
nil
cons
cons
647
def
618
remove
nil
125
ref
614
ref
cons
648
def
126
ref
74
ref
129
ref
appTerm
649
def
127
ref
appTerm
nil
cons
650
def
cons
nil
cons
651
def
cons
nil
cons
cons
192
ref
subst
proveHyp
649
ref
refl
617
remove
appThm
sym
nil
125
ref
158
ref
cons
652
def
126
ref
158
ref
cons
nil
cons
653
def
cons
nil
cons
cons
654
def
143
ref
subst
654
remove
192
ref
subst
159
remove
eqMp
nil
161
ref
158
remove
cons
163
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
655
def
eqMp
nil
652
ref
126
ref
155
ref
cons
nil
cons
656
def
cons
nil
cons
cons
184
ref
subst
nil
161
ref
614
remove
cons
657
def
162
ref
650
remove
cons
nil
cons
658
def
cons
nil
cons
cons
659
def
343
ref
subst
eqMp
184
ref
659
remove
176
ref
subst
eqMp
deductAntisym
deductAntisym
660
def
subst
647
ref
143
ref
subst
647
remove
192
ref
subst
nil
52
ref
57
ref
74
ref
642
ref
111
ref
appTerm
661
def
appTerm
167
ref
appTerm
662
def
absTerm
663
def
nil
cons
cons
nil
cons
nil
cons
cons
66
ref
subst
57
ref
nil
68
ref
662
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
661
ref
nil
cons
664
def
cons
588
ref
cons
nil
cons
cons
665
def
143
ref
subst
665
remove
192
ref
subst
661
ref
betaConv
666
def
661
remove
assume
eqMp
591
remove
proveHyp
594
remove
eqMp
eqMp
nil
161
ref
664
remove
cons
596
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
51
ref
663
remove
appTerm
nil
cons
cons
646
remove
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
642
remove
nil
cons
cons
667
def
596
ref
cons
nil
cons
cons
623
ref
subst
eqMp
eqMp
nil
595
remove
162
ref
645
ref
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
125
ref
581
remove
644
ref
appTerm
nil
cons
cons
126
ref
74
ref
644
ref
appTerm
580
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
192
ref
subst
proveHyp
nil
125
ref
645
ref
cons
126
ref
585
ref
cons
nil
cons
cons
nil
cons
cons
668
def
143
ref
subst
668
remove
192
ref
subst
nil
593
remove
nil
cons
nil
cons
cons
66
ref
subst
57
ref
nil
68
ref
578
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
590
ref
143
ref
subst
590
remove
192
ref
subst
666
remove
sym
189
remove
assume
eqMp
348
ref
667
remove
350
ref
cons
nil
cons
cons
597
ref
subst
proveHyp
nil
125
ref
643
remove
nil
cons
cons
588
remove
cons
nil
cons
cons
184
ref
subst
644
remove
assume
eqMp
proveHyp
eqMp
nil
161
ref
190
remove
cons
596
remove
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
161
ref
645
remove
cons
162
ref
585
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
subst
nil
52
ref
57
ref
573
ref
630
ref
appTerm
669
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
66
ref
subst
57
ref
nil
68
ref
669
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
311
remove
nil
cons
670
def
cons
671
def
632
remove
cons
nil
cons
cons
672
def
143
ref
subst
672
remove
192
ref
subst
nil
68
ref
628
ref
nil
cons
673
def
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
671
remove
126
ref
673
remove
cons
674
def
nil
cons
cons
nil
cons
cons
184
ref
subst
57
ref
573
remove
628
ref
appTerm
absTerm
675
def
111
ref
appTerm
676
def
betaConv
55
remove
51
ref
675
ref
appTerm
677
def
absTerm
678
def
56
remove
appTerm
679
def
betaConv
nil
320
remove
678
ref
appTerm
680
def
axiom
nil
125
ref
680
remove
nil
cons
cons
126
ref
679
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
327
remove
328
remove
678
remove
nil
cons
cons
331
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
677
remove
nil
cons
cons
126
ref
676
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
675
remove
nil
cons
cons
350
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
eqMp
eqMp
eqMp
nil
161
ref
670
remove
cons
641
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
eqMp
eqMp
nil
161
ref
626
ref
cons
641
remove
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
125
ref
74
ref
625
ref
appTerm
681
def
630
remove
appTerm
nil
cons
cons
126
ref
48
ref
681
ref
628
remove
appTerm
appTerm
682
def
681
ref
58
ref
appTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
"q'"
7
ref
var
683
def
58
ref
nil
cons
684
def
cons
nil
cons
nil
cons
cons
625
ref
refl
nil
125
ref
48
ref
625
ref
appTerm
685
def
625
remove
appTerm
nil
cons
cons
126
ref
74
ref
681
ref
629
remove
683
ref
varTerm
686
def
appTerm
687
def
appTerm
appTerm
682
ref
681
remove
686
ref
appTerm
appTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
"p'"
7
ref
var
688
def
626
remove
cons
nil
cons
nil
cons
cons
683
ref
74
ref
685
remove
688
ref
varTerm
689
def
appTerm
appTerm
74
ref
74
ref
689
ref
appTerm
690
def
687
remove
appTerm
appTerm
682
remove
690
ref
686
ref
appTerm
691
def
appTerm
appTerm
appTerm
absTerm
692
def
686
ref
appTerm
693
def
betaConv
688
ref
572
ref
692
ref
appTerm
694
def
absTerm
695
def
689
ref
appTerm
696
def
betaConv
nil
674
remove
627
remove
nil
cons
cons
nil
cons
cons
nil
576
ref
688
ref
572
ref
683
ref
74
ref
610
remove
689
ref
appTerm
697
def
appTerm
74
ref
690
ref
48
ref
129
ref
appTerm
686
ref
appTerm
698
def
appTerm
699
def
appTerm
131
remove
691
ref
appTerm
700
def
appTerm
701
def
appTerm
702
def
absTerm
703
def
appTerm
704
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
584
ref
subst
688
remove
nil
68
ref
704
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
576
ref
703
remove
nil
cons
cons
nil
cons
nil
cons
cons
584
ref
subst
683
remove
nil
68
ref
702
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
697
remove
nil
cons
705
def
cons
706
def
126
ref
701
remove
nil
cons
707
def
cons
nil
cons
cons
nil
cons
cons
708
def
143
ref
subst
708
remove
192
ref
subst
nil
125
ref
699
ref
nil
cons
709
def
cons
126
ref
700
remove
nil
cons
710
def
cons
nil
cons
cons
nil
cons
cons
711
def
143
ref
subst
711
remove
192
ref
subst
nil
648
remove
126
ref
691
ref
nil
cons
712
def
cons
nil
cons
cons
nil
cons
cons
713
def
660
ref
subst
713
ref
143
ref
subst
713
remove
192
ref
subst
nil
125
ref
689
ref
nil
cons
714
def
cons
715
def
126
ref
686
ref
nil
cons
716
def
cons
nil
cons
717
def
cons
nil
cons
cons
718
def
143
ref
subst
718
ref
192
ref
subst
nil
706
ref
126
ref
128
ref
689
remove
appTerm
719
def
nil
cons
720
def
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
nil
125
ref
155
remove
cons
126
ref
714
ref
cons
nil
cons
cons
nil
cons
cons
721
def
621
ref
subst
eqMp
722
def
nil
125
ref
720
ref
cons
723
def
717
ref
cons
nil
cons
cons
724
def
184
ref
subst
proveHyp
nil
706
remove
126
ref
690
remove
127
ref
appTerm
725
def
nil
cons
726
def
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
721
ref
nil
613
remove
651
remove
cons
nil
cons
cons
727
def
143
ref
subst
727
remove
192
ref
subst
655
remove
eqMp
nil
619
remove
658
remove
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
728
def
subst
eqMp
729
def
nil
125
ref
726
ref
cons
730
def
126
ref
74
ref
719
ref
appTerm
731
def
686
ref
appTerm
nil
cons
732
def
cons
nil
cons
cons
nil
cons
cons
733
def
184
ref
subst
proveHyp
733
ref
143
ref
subst
733
remove
192
ref
subst
724
ref
143
ref
subst
724
remove
192
ref
subst
nil
715
ref
656
remove
cons
nil
cons
cons
184
ref
subst
725
remove
assume
eqMp
734
def
721
remove
184
ref
subst
719
remove
assume
eqMp
735
def
734
remove
proveHyp
proveHyp
nil
715
remove
126
ref
698
remove
nil
cons
736
def
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
699
remove
assume
eqMp
737
def
nil
125
ref
736
remove
cons
738
def
126
ref
649
ref
686
ref
appTerm
739
def
nil
cons
740
def
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
652
remove
717
ref
cons
nil
cons
cons
741
def
621
remove
subst
eqMp
742
def
nil
125
ref
740
ref
cons
743
def
717
remove
cons
nil
cons
cons
744
def
184
ref
subst
proveHyp
737
remove
nil
738
remove
126
ref
74
ref
686
ref
appTerm
129
ref
appTerm
745
def
nil
cons
746
def
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
741
ref
728
remove
subst
eqMp
747
def
nil
125
ref
746
ref
cons
748
def
126
ref
74
ref
739
ref
appTerm
749
def
686
remove
appTerm
nil
cons
750
def
cons
nil
cons
cons
nil
cons
cons
751
def
184
ref
subst
proveHyp
751
ref
143
ref
subst
751
remove
192
ref
subst
744
ref
143
ref
subst
744
remove
192
ref
subst
183
remove
741
remove
184
ref
subst
739
remove
assume
eqMp
proveHyp
eqMp
nil
161
ref
740
remove
cons
752
def
162
ref
716
ref
cons
nil
cons
753
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
nil
161
ref
746
remove
cons
754
def
162
ref
750
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
proveHyp
eqMp
nil
161
ref
720
remove
cons
755
def
753
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
nil
161
ref
726
remove
cons
756
def
162
ref
732
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
161
ref
714
ref
cons
753
remove
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
nil
657
remove
162
ref
712
ref
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
125
ref
74
ref
130
ref
appTerm
691
ref
appTerm
nil
cons
cons
126
ref
74
ref
691
ref
appTerm
130
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
192
ref
subst
proveHyp
nil
125
ref
712
ref
cons
615
remove
cons
nil
cons
cons
757
def
143
ref
subst
757
remove
192
ref
subst
143
ref
192
ref
722
remove
nil
723
remove
653
ref
cons
nil
cons
cons
758
def
184
ref
subst
proveHyp
729
remove
nil
730
remove
126
ref
731
remove
129
ref
appTerm
nil
cons
759
def
cons
nil
cons
cons
nil
cons
cons
760
def
184
ref
subst
proveHyp
760
ref
143
ref
subst
760
remove
192
ref
subst
758
ref
143
ref
subst
758
remove
192
ref
subst
735
remove
742
remove
nil
743
remove
653
ref
cons
nil
cons
cons
761
def
184
ref
subst
proveHyp
747
remove
nil
748
remove
126
ref
749
remove
129
remove
appTerm
nil
cons
762
def
cons
nil
cons
cons
nil
cons
cons
763
def
184
ref
subst
proveHyp
763
ref
143
ref
subst
763
remove
192
ref
subst
761
ref
143
ref
subst
761
remove
192
ref
subst
718
remove
184
ref
subst
691
remove
assume
eqMp
nil
125
ref
716
ref
cons
653
remove
cons
nil
cons
cons
184
ref
subst
745
remove
assume
eqMp
proveHyp
eqMp
nil
752
remove
163
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
nil
754
remove
162
ref
762
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
proveHyp
eqMp
nil
755
remove
163
remove
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
nil
756
remove
162
ref
759
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
177
remove
deductAntisym
eqMp
eqMp
nil
161
ref
712
remove
cons
620
remove
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
161
ref
709
remove
cons
162
ref
710
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
nil
161
ref
705
remove
cons
162
ref
707
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
subst
nil
125
ref
572
ref
695
ref
appTerm
nil
cons
cons
126
ref
696
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
583
ref
576
ref
695
remove
nil
cons
cons
622
ref
714
remove
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
694
remove
nil
cons
cons
126
ref
693
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
583
ref
576
ref
692
remove
nil
cons
cons
622
ref
716
remove
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
eqMp
subst
eqMp
640
remove
68
ref
48
ref
74
ref
70
ref
appTerm
764
def
58
ref
appTerm
appTerm
58
ref
appTerm
absTerm
765
def
70
ref
appTerm
766
def
betaConv
nil
572
ref
765
ref
appTerm
767
def
axiom
nil
125
ref
767
remove
nil
cons
cons
126
ref
766
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
583
ref
576
ref
765
remove
nil
cons
cons
622
ref
70
ref
nil
cons
cons
nil
cons
768
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
769
def
subst
trans
sym
71
ref
eqMp
770
def
subst
eqMp
eqMp
nil
125
ref
51
ref
521
ref
appTerm
nil
cons
cons
126
ref
522
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
521
remove
nil
cons
cons
458
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
520
remove
nil
cons
cons
126
ref
519
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
391
ref
518
remove
nil
cons
cons
453
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
sym
771
def
subst
subst
772
def
appThm
eqMp
504
remove
506
ref
433
ref
430
ref
257
ref
0
ref
0
ref
0
ref
508
ref
4
ref
cons
opType
773
def
8
ref
cons
opType
774
def
773
ref
nil
cons
775
def
cons
opType
constTerm
"fn"
773
remove
var
776
def
51
ref
429
ref
264
ref
433
ref
430
ref
776
ref
varTerm
514
ref
appTerm
appTerm
777
def
434
ref
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
778
def
appTerm
779
def
514
ref
appTerm
appTerm
434
ref
appTerm
absTerm
780
def
434
ref
appTerm
781
def
betaConv
429
ref
264
ref
780
ref
appTerm
782
def
absTerm
783
def
439
ref
appTerm
784
def
betaConv
778
ref
779
remove
appTerm
785
def
betaConv
104
ref
0
ref
774
ref
8
ref
cons
opType
constTerm
786
def
refl
776
remove
525
remove
429
ref
526
ref
433
ref
777
remove
refl
429
ref
433
ref
434
ref
absTerm
787
def
absTerm
788
def
439
ref
appTerm
betaConv
529
remove
appThm
787
remove
434
ref
appTerm
betaConv
trans
appThm
absThm
appThm
absThm
appThm
absThm
appThm
"C"
4
ref
cons
nil
cons
"_1343"
0
ref
2
ref
0
ref
3
ref
4
ref
cons
opType
nil
cons
cons
opType
var
788
remove
nil
cons
cons
nil
cons
nil
cons
cons
624
remove
subst
eqMp
nil
125
ref
786
remove
778
ref
appTerm
nil
cons
cons
126
ref
785
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
"A"
775
remove
cons
nil
cons
"p"
774
remove
var
778
remove
nil
cons
cons
nil
cons
nil
cons
cons
770
ref
subst
eqMp
eqMp
nil
125
ref
51
ref
783
ref
appTerm
nil
cons
cons
126
ref
784
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
783
remove
nil
cons
cons
458
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
782
remove
nil
cons
cons
126
ref
781
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
391
ref
780
remove
nil
cons
cons
453
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
sym
789
def
subst
subst
790
def
appThm
eqMp
sym
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
"A"
259
remove
cons
nil
cons
791
def
"P"
258
ref
var
462
ref
nil
cons
792
def
cons
"x"
251
remove
var
483
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
597
ref
subst
proveHyp
nil
125
ref
104
ref
0
ref
258
ref
8
ref
cons
opType
constTerm
462
remove
appTerm
nil
cons
cons
126
ref
469
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
"p"
258
remove
var
792
remove
cons
nil
cons
nil
cons
cons
791
remove
43
ref
cons
770
ref
subst
subst
eqMp
eqMp
nil
125
ref
264
ref
467
ref
appTerm
nil
cons
cons
126
ref
468
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
391
ref
467
remove
nil
cons
cons
452
ref
502
remove
cons
nil
cons
793
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
466
remove
nil
cons
cons
126
ref
465
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
464
remove
nil
cons
cons
185
ref
500
ref
cons
nil
cons
794
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
795
def
trans
796
def
trans
appThm
appThm
353
remove
appThm
sym
241
ref
nil
"xs"
25
ref
var
797
def
83
ref
nil
cons
cons
793
ref
cons
nil
cons
cons
798
def
397
ref
19
ref
45
ref
22
remove
constTerm
799
def
36
ref
247
ref
appTerm
appTerm
"Number.Natural.suc"
const
0
ref
20
ref
26
ref
cons
opType
constTerm
800
def
37
ref
appTerm
appTerm
absTerm
801
def
34
ref
appTerm
802
def
betaConv
57
ref
18
ref
801
ref
appTerm
803
def
absTerm
804
def
111
ref
appTerm
805
def
betaConv
nil
51
ref
804
ref
appTerm
806
def
axiom
nil
125
ref
806
remove
nil
cons
cons
126
ref
805
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
804
remove
nil
cons
cons
350
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
803
remove
nil
cons
cons
126
ref
802
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
801
remove
nil
cons
cons
187
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
807
def
subst
subst
appThm
245
ref
807
remove
subst
808
def
appThm
nil
"n"
20
ref
var
809
def
36
ref
113
ref
appTerm
810
def
nil
cons
811
def
cons
"m"
20
ref
var
812
def
84
remove
nil
cons
cons
nil
cons
813
def
cons
nil
cons
cons
809
ref
48
ref
23
ref
800
ref
812
ref
varTerm
814
def
appTerm
appTerm
800
ref
809
ref
varTerm
815
def
appTerm
appTerm
appTerm
23
ref
814
ref
appTerm
816
def
815
ref
appTerm
817
def
appTerm
absTerm
818
def
815
ref
appTerm
819
def
betaConv
812
ref
12
ref
0
ref
21
ref
8
ref
cons
opType
820
def
constTerm
821
def
818
ref
appTerm
822
def
absTerm
823
def
814
ref
appTerm
824
def
betaConv
nil
821
ref
823
ref
appTerm
825
def
axiom
nil
125
ref
825
remove
nil
cons
cons
126
ref
824
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
"A"
26
remove
cons
nil
cons
826
def
"P"
21
remove
var
827
def
823
remove
nil
cons
cons
"x"
20
ref
var
828
def
814
ref
nil
cons
cons
nil
cons
829
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
822
remove
nil
cons
cons
126
ref
819
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
826
ref
827
ref
818
remove
nil
cons
cons
828
ref
815
ref
nil
cons
cons
nil
cons
830
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
trans
sym
809
ref
132
ref
85
ref
815
ref
appTerm
appTerm
23
ref
815
ref
appTerm
831
def
810
ref
appTerm
appTerm
absTerm
832
def
86
ref
appTerm
betaConv
sym
nil
75
ref
243
remove
cons
833
def
"y"
2
ref
var
834
def
349
remove
cons
19
ref
500
remove
cons
nil
cons
835
def
cons
cons
nil
cons
cons
75
ref
48
ref
78
ref
34
ref
appTerm
836
def
110
ref
834
ref
varTerm
837
def
appTerm
79
ref
appTerm
appTerm
appTerm
362
ref
34
ref
appTerm
79
ref
appTerm
838
def
appTerm
absTerm
839
def
79
ref
appTerm
840
def
betaConv
834
ref
18
ref
839
ref
appTerm
841
def
absTerm
842
def
837
ref
appTerm
843
def
betaConv
19
ref
51
ref
842
ref
appTerm
844
def
absTerm
845
def
34
ref
appTerm
846
def
betaConv
nil
18
ref
845
ref
appTerm
847
def
axiom
nil
125
ref
847
remove
nil
cons
cons
126
ref
846
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
845
remove
nil
cons
cons
187
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
844
remove
nil
cons
cons
126
ref
843
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
842
remove
nil
cons
cons
57
ref
837
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
841
remove
nil
cons
cons
126
ref
840
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
839
remove
nil
cons
cons
794
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
848
def
nil
68
ref
414
ref
cons
nil
cons
nil
cons
cons
72
ref
subst
378
ref
assume
eqMp
trans
sym
71
ref
eqMp
849
def
nil
125
ref
228
remove
nil
cons
cons
850
def
126
ref
87
ref
nil
cons
851
def
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
230
ref
79
ref
appTerm
852
def
betaConv
nil
238
remove
126
ref
852
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
91
ref
73
ref
230
remove
nil
cons
cons
794
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
eqMp
nil
125
ref
851
remove
cons
126
ref
23
ref
86
ref
appTerm
810
ref
appTerm
nil
cons
cons
nil
cons
853
def
cons
nil
cons
cons
192
ref
subst
proveHyp
nil
125
ref
414
remove
cons
853
remove
cons
nil
cons
cons
184
ref
subst
nil
833
remove
835
remove
cons
nil
cons
cons
75
ref
74
ref
838
remove
appTerm
23
ref
37
remove
appTerm
86
ref
appTerm
appTerm
absTerm
854
def
79
ref
appTerm
855
def
betaConv
19
ref
18
ref
854
ref
appTerm
856
def
absTerm
857
def
34
ref
appTerm
858
def
betaConv
nil
18
ref
857
ref
appTerm
859
def
axiom
nil
125
ref
859
remove
nil
cons
cons
126
ref
858
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
857
remove
nil
cons
cons
187
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
856
remove
nil
cons
cons
126
ref
855
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
854
remove
nil
cons
cons
794
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
eqMp
826
ref
827
ref
832
ref
nil
cons
cons
828
ref
86
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
597
ref
subst
proveHyp
nil
125
ref
104
ref
820
remove
constTerm
860
def
832
remove
appTerm
nil
cons
cons
126
ref
85
remove
810
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
"p"
20
ref
var
861
def
811
remove
cons
813
remove
cons
nil
cons
cons
861
ref
74
ref
860
remove
809
ref
132
ref
817
remove
appTerm
831
ref
861
ref
varTerm
862
def
appTerm
appTerm
863
def
absTerm
864
def
appTerm
865
def
appTerm
866
def
816
remove
862
ref
appTerm
867
def
appTerm
868
def
absTerm
869
def
862
ref
appTerm
870
def
betaConv
812
ref
821
ref
869
ref
appTerm
871
def
absTerm
872
def
814
ref
appTerm
873
def
betaConv
nil
821
ref
812
ref
821
ref
809
ref
821
ref
861
ref
74
ref
863
ref
appTerm
867
ref
appTerm
absTerm
874
def
appTerm
875
def
absTerm
876
def
appTerm
877
def
absTerm
878
def
appTerm
879
def
axiom
nil
125
ref
879
ref
nil
cons
880
def
cons
881
def
126
ref
821
ref
872
ref
appTerm
nil
cons
882
def
cons
nil
cons
cons
nil
cons
cons
883
def
184
ref
subst
proveHyp
883
ref
143
ref
subst
883
remove
192
ref
subst
nil
827
ref
872
remove
nil
cons
cons
884
def
nil
cons
nil
cons
cons
826
ref
43
ref
cons
66
ref
subst
885
def
subst
812
remove
nil
68
ref
871
remove
nil
cons
886
def
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
827
ref
869
remove
nil
cons
cons
887
def
nil
cons
nil
cons
cons
885
ref
subst
861
remove
nil
68
ref
868
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
865
remove
nil
cons
888
def
cons
889
def
126
ref
867
ref
nil
cons
890
def
cons
nil
cons
891
def
cons
nil
cons
cons
892
def
143
ref
subst
892
remove
192
ref
subst
nil
881
ref
891
ref
cons
nil
cons
cons
893
def
184
ref
subst
nil
889
remove
126
ref
74
ref
879
remove
appTerm
867
remove
appTerm
894
def
nil
cons
895
def
cons
nil
cons
896
def
cons
nil
cons
cons
184
ref
subst
nil
827
ref
809
ref
74
ref
864
ref
815
ref
appTerm
897
def
appTerm
894
ref
appTerm
898
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
885
remove
subst
809
ref
nil
68
ref
898
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
897
ref
nil
cons
899
def
cons
896
ref
cons
nil
cons
cons
900
def
143
ref
subst
900
remove
192
ref
subst
897
ref
betaConv
897
remove
assume
eqMp
nil
125
ref
863
remove
nil
cons
901
def
cons
902
def
896
remove
cons
nil
cons
cons
903
def
184
ref
subst
proveHyp
903
ref
143
ref
subst
903
remove
192
ref
subst
893
ref
143
ref
subst
893
remove
192
ref
subst
nil
902
remove
891
remove
cons
nil
cons
cons
184
ref
subst
874
ref
862
ref
appTerm
904
def
betaConv
876
ref
815
ref
appTerm
905
def
betaConv
878
ref
814
remove
appTerm
906
def
betaConv
nil
881
remove
126
ref
906
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
826
ref
827
ref
878
remove
nil
cons
cons
829
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
877
remove
nil
cons
cons
126
ref
905
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
826
ref
827
ref
876
remove
nil
cons
cons
830
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
875
remove
nil
cons
cons
126
ref
904
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
826
ref
827
ref
874
remove
nil
cons
cons
828
ref
862
remove
nil
cons
cons
nil
cons
907
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
161
ref
880
remove
cons
908
def
162
ref
890
remove
cons
nil
cons
909
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
nil
161
ref
901
remove
cons
162
ref
895
remove
cons
nil
cons
910
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
161
ref
899
remove
cons
910
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
821
ref
828
ref
74
ref
864
ref
828
remove
varTerm
appTerm
appTerm
894
ref
appTerm
absTerm
appTerm
nil
cons
cons
126
ref
866
remove
894
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
826
ref
827
ref
864
remove
nil
cons
cons
910
remove
cons
nil
cons
cons
623
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
161
ref
888
remove
cons
909
remove
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
908
remove
162
ref
882
ref
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
nil
125
ref
882
remove
cons
126
ref
873
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
826
ref
884
remove
829
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
886
remove
cons
126
ref
870
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
826
ref
887
remove
907
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
eqMp
proveHyp
proveHyp
eqMp
nil
161
ref
411
remove
cons
911
def
162
ref
388
ref
cons
nil
cons
912
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
161
ref
407
remove
cons
913
def
912
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
18
ref
185
ref
74
ref
380
ref
185
ref
varTerm
914
def
appTerm
appTerm
915
def
387
ref
appTerm
absTerm
appTerm
nil
cons
cons
126
ref
74
ref
381
remove
appTerm
916
def
387
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
380
remove
nil
cons
cons
917
def
912
ref
cons
nil
cons
cons
623
ref
subst
eqMp
eqMp
eqMp
nil
161
ref
399
remove
cons
918
def
912
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
264
ref
452
ref
74
ref
382
ref
452
ref
varTerm
919
def
appTerm
appTerm
920
def
387
ref
appTerm
absTerm
appTerm
nil
cons
cons
126
ref
74
ref
383
ref
appTerm
921
def
387
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
391
ref
382
ref
nil
cons
cons
922
def
912
ref
cons
nil
cons
cons
623
ref
subst
eqMp
nil
125
ref
376
ref
nil
cons
923
def
cons
924
def
389
remove
cons
nil
cons
cons
925
def
143
ref
subst
925
remove
192
ref
subst
241
ref
242
ref
418
ref
376
remove
assume
926
def
appThm
nil
425
ref
nil
cons
cons
428
remove
435
ref
430
ref
437
remove
356
ref
432
ref
constTerm
927
def
appTerm
appTerm
434
ref
appTerm
absTerm
928
def
436
ref
appTerm
929
def
betaConv
433
ref
447
ref
928
ref
appTerm
930
def
absTerm
931
def
434
ref
appTerm
932
def
betaConv
nil
264
ref
931
ref
appTerm
933
def
axiom
nil
125
ref
933
remove
nil
cons
cons
126
ref
932
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
391
ref
931
remove
nil
cons
cons
453
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
930
remove
nil
cons
cons
126
ref
929
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
454
ref
455
ref
928
remove
nil
cons
cons
457
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
934
def
subst
935
def
subst
936
def
trans
appThm
397
ref
nil
799
ref
36
ref
99
ref
appTerm
937
def
appTerm
"Number.Natural.zero"
const
20
remove
constTerm
938
def
appTerm
axiom
939
def
subst
940
def
trans
appThm
808
remove
appThm
nil
809
ref
800
remove
810
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
nil
68
ref
23
ref
938
ref
appTerm
815
ref
appTerm
941
def
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
809
ref
941
remove
absTerm
942
def
815
ref
appTerm
943
def
betaConv
nil
821
ref
942
ref
appTerm
944
def
axiom
nil
125
ref
944
remove
nil
cons
cons
126
ref
943
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
826
ref
827
ref
942
remove
nil
cons
cons
830
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
eqMp
subst
trans
sym
71
ref
eqMp
eqMp
nil
161
ref
923
remove
cons
945
def
912
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
945
ref
162
ref
383
remove
nil
cons
cons
946
def
"R"
7
ref
var
947
def
388
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
125
ref
74
ref
167
ref
appTerm
948
def
947
ref
varTerm
949
def
appTerm
950
def
nil
cons
cons
126
ref
949
ref
nil
cons
951
def
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
nil
125
ref
74
ref
165
ref
appTerm
952
def
949
ref
appTerm
nil
cons
cons
126
ref
74
ref
950
remove
appTerm
949
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
"r"
7
ref
var
953
def
74
ref
952
ref
953
ref
varTerm
954
def
appTerm
appTerm
955
def
74
ref
948
remove
954
ref
appTerm
appTerm
954
ref
appTerm
appTerm
absTerm
956
def
949
remove
appTerm
957
def
betaConv
48
ref
95
ref
165
ref
appTerm
958
def
167
ref
appTerm
959
def
appTerm
refl
126
ref
572
ref
953
ref
955
remove
74
ref
649
remove
954
ref
appTerm
appTerm
954
ref
appTerm
960
def
appTerm
absTerm
appTerm
absTerm
167
remove
appTerm
betaConv
appThm
151
ref
958
remove
appTerm
refl
125
ref
126
ref
572
ref
953
remove
74
ref
128
ref
954
remove
appTerm
appTerm
960
remove
appTerm
absTerm
appTerm
absTerm
absTerm
961
def
165
ref
appTerm
betaConv
appThm
nil
140
remove
95
ref
appTerm
961
remove
appTerm
axiom
174
ref
appThm
eqMp
170
remove
appThm
eqMp
959
remove
assume
eqMp
nil
125
ref
572
ref
956
ref
appTerm
nil
cons
cons
126
ref
957
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
583
ref
576
ref
956
remove
nil
cons
cons
622
ref
951
remove
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
eqMp
eqMp
962
def
subst
proveHyp
proveHyp
eqMp
nil
161
ref
384
remove
cons
963
def
912
remove
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
161
ref
237
remove
cons
162
ref
239
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
161
ref
219
remove
cons
964
def
162
ref
94
ref
cons
nil
cons
965
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
161
ref
215
remove
cons
966
def
965
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
18
ref
185
ref
74
ref
116
ref
914
ref
appTerm
appTerm
967
def
88
ref
appTerm
absTerm
appTerm
nil
cons
cons
126
ref
74
ref
117
remove
appTerm
968
def
88
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
116
remove
nil
cons
cons
969
def
965
ref
cons
nil
cons
cons
623
ref
subst
eqMp
eqMp
eqMp
nil
161
ref
207
remove
cons
970
def
965
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
51
ref
206
remove
appTerm
nil
cons
cons
126
ref
74
ref
119
ref
appTerm
971
def
88
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
118
remove
nil
cons
cons
972
def
965
ref
cons
nil
cons
cons
623
ref
subst
eqMp
nil
125
ref
103
ref
nil
cons
973
def
cons
974
def
198
ref
cons
nil
cons
cons
975
def
143
ref
subst
975
remove
192
ref
subst
226
ref
"_32468"
15
ref
var
976
def
74
ref
18
ref
75
ref
74
ref
80
ref
976
remove
varTerm
977
def
appTerm
appTerm
87
ref
appTerm
absTerm
appTerm
appTerm
23
ref
27
ref
33
ref
977
ref
appTerm
appTerm
appTerm
36
ref
977
remove
appTerm
appTerm
appTerm
absTerm
102
ref
appTerm
betaConv
appThm
227
ref
74
ref
18
ref
75
ref
74
ref
80
ref
102
ref
appTerm
appTerm
87
ref
appTerm
absTerm
appTerm
978
def
appTerm
979
def
23
ref
27
ref
290
ref
appTerm
appTerm
36
ref
102
ref
appTerm
980
def
appTerm
appTerm
refl
appThm
trans
235
ref
103
remove
assume
981
def
appThm
eqMp
sym
979
remove
refl
241
ref
242
ref
344
remove
346
remove
176
ref
subst
proveHyp
982
def
appThm
397
ref
nil
799
remove
980
remove
appTerm
938
ref
appTerm
axiom
983
def
subst
trans
appThm
983
remove
appThm
nil
809
ref
938
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
68
ref
831
remove
815
ref
appTerm
984
def
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
809
remove
984
remove
absTerm
985
def
815
remove
appTerm
986
def
betaConv
nil
821
remove
985
ref
appTerm
987
def
axiom
nil
125
ref
987
remove
nil
cons
cons
126
ref
986
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
826
remove
827
remove
985
remove
nil
cons
cons
830
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
eqMp
subst
988
def
trans
appThm
nil
68
ref
978
remove
nil
cons
cons
nil
cons
nil
cons
cons
769
ref
subst
trans
sym
71
ref
eqMp
eqMp
eqMp
nil
161
ref
973
remove
cons
989
def
965
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
989
ref
162
ref
119
remove
nil
cons
cons
990
def
947
ref
94
remove
cons
nil
cons
991
def
cons
cons
nil
cons
cons
962
ref
subst
proveHyp
proveHyp
eqMp
nil
161
ref
200
ref
cons
992
def
965
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
125
ref
100
ref
nil
cons
993
def
cons
994
def
198
remove
cons
nil
cons
cons
995
def
143
ref
subst
995
remove
192
ref
subst
226
remove
"_32466"
15
ref
var
996
def
74
ref
18
ref
75
ref
74
ref
80
ref
996
remove
varTerm
997
def
appTerm
appTerm
87
ref
appTerm
absTerm
appTerm
appTerm
23
ref
27
ref
33
ref
997
ref
appTerm
appTerm
appTerm
36
remove
997
remove
appTerm
appTerm
appTerm
absTerm
99
ref
appTerm
betaConv
appThm
227
remove
74
ref
18
ref
75
ref
74
ref
80
ref
99
ref
appTerm
appTerm
87
remove
appTerm
absTerm
appTerm
998
def
appTerm
999
def
23
remove
27
remove
287
ref
appTerm
appTerm
937
remove
appTerm
appTerm
refl
appThm
trans
235
remove
100
remove
assume
1000
def
appThm
eqMp
sym
999
remove
refl
241
remove
242
remove
341
remove
342
remove
176
ref
subst
proveHyp
1001
def
appThm
940
remove
trans
appThm
939
remove
appThm
988
remove
trans
appThm
nil
68
ref
998
remove
nil
cons
cons
nil
cons
nil
cons
cons
769
remove
subst
trans
sym
71
ref
eqMp
eqMp
eqMp
nil
161
ref
993
remove
cons
1002
def
965
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
1002
ref
162
ref
200
remove
cons
1003
def
991
remove
cons
cons
nil
cons
cons
962
ref
subst
proveHyp
proveHyp
eqMp
nil
161
ref
196
remove
cons
1004
def
965
remove
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
absThm
eqMp
nil
125
ref
18
ref
89
remove
appTerm
nil
cons
cons
126
ref
69
remove
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
74
ref
refl
1005
def
18
ref
refl
1006
def
19
ref
1005
ref
1006
ref
75
ref
82
ref
refl
1007
def
39
ref
79
ref
appTerm
betaConv
appThm
absThm
appThm
appThm
39
ref
34
ref
appTerm
betaConv
1008
def
appThm
absThm
appThm
appThm
1006
ref
19
ref
1008
remove
absThm
appThm
appThm
nil
"p"
16
ref
var
1009
def
39
remove
nil
cons
cons
nil
cons
nil
cons
cons
1009
ref
74
ref
18
ref
19
ref
74
ref
18
ref
75
ref
82
ref
1009
ref
varTerm
1010
def
79
ref
appTerm
appTerm
absTerm
appTerm
appTerm
1010
ref
34
ref
appTerm
1011
def
appTerm
absTerm
appTerm
appTerm
18
ref
19
ref
1011
remove
absTerm
appTerm
appTerm
absTerm
1012
def
1010
ref
appTerm
1013
def
betaConv
nil
12
ref
0
ref
17
ref
8
ref
cons
opType
constTerm
1012
ref
appTerm
1014
def
axiom
nil
125
ref
1014
remove
nil
cons
cons
126
ref
1013
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
"A"
76
remove
cons
nil
cons
"P"
17
remove
var
1012
remove
nil
cons
cons
"x"
16
remove
var
1010
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
1015
def
subst
eqMp
eqMp
eqMp
absThm
eqMp
nil
298
ref
41
remove
appTerm
thm
nil
10
ref
11
ref
12
ref
0
ref
0
ref
532
ref
8
ref
cons
opType
1016
def
8
ref
cons
opType
constTerm
1017
def
"f"
532
ref
var
1018
def
18
ref
19
ref
45
ref
0
ref
13
remove
531
ref
opType
1019
def
0
ref
1019
ref
8
ref
cons
opType
nil
cons
cons
opType
constTerm
1020
def
28
remove
0
ref
1
remove
2
ref
531
ref
cons
opType
1021
def
0
ref
15
ref
1019
ref
nil
cons
1022
def
cons
opType
1023
def
nil
cons
cons
opType
constTerm
"Parser.map"
const
0
ref
6
ref
0
ref
532
ref
1021
ref
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
32
ref
appTerm
1018
ref
varTerm
1024
def
appTerm
1025
def
appTerm
1026
def
34
ref
appTerm
appTerm
"Parser.Stream.map"
const
1027
def
0
ref
532
ref
0
ref
25
ref
1022
ref
cons
opType
nil
cons
cons
opType
constTerm
1024
ref
appTerm
1028
def
35
ref
appTerm
appTerm
1029
def
absTerm
1030
def
appTerm
1031
def
absTerm
1032
def
appTerm
1033
def
absTerm
1034
def
nil
cons
cons
nil
cons
nil
cons
cons
67
ref
subst
11
ref
nil
68
ref
1033
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
"P"
1016
remove
var
1035
def
1032
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
533
remove
cons
nil
cons
1036
def
43
ref
cons
66
ref
subst
subst
1018
ref
nil
68
ref
1031
remove
nil
cons
1037
def
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
73
ref
19
ref
74
ref
18
ref
75
ref
82
ref
1020
ref
1026
ref
79
ref
appTerm
1038
def
appTerm
1028
ref
83
ref
appTerm
appTerm
1039
def
appTerm
absTerm
appTerm
1040
def
appTerm
1029
ref
appTerm
1041
def
absTerm
1042
def
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
19
ref
nil
68
ref
1041
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
1040
ref
nil
cons
1043
def
cons
126
ref
1029
ref
nil
cons
1044
def
cons
nil
cons
1045
def
cons
nil
cons
cons
1046
def
143
ref
subst
1046
remove
192
ref
subst
195
ref
nil
197
ref
1045
ref
cons
nil
cons
cons
1047
def
184
ref
subst
proveHyp
1047
ref
143
ref
subst
1047
remove
192
ref
subst
nil
201
ref
1045
ref
cons
nil
cons
cons
1048
def
143
ref
subst
1048
remove
192
ref
subst
nil
52
ref
57
ref
204
ref
1029
ref
appTerm
1049
def
absTerm
1050
def
nil
cons
cons
nil
cons
nil
cons
cons
66
ref
subst
57
ref
nil
68
ref
1049
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
208
ref
1045
ref
cons
nil
cons
cons
1051
def
143
ref
subst
1051
remove
192
ref
subst
210
ref
nil
211
ref
1045
ref
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
73
ref
107
ref
213
ref
1029
ref
appTerm
1052
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
107
ref
nil
68
ref
1052
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
216
ref
1045
ref
cons
nil
cons
cons
1053
def
143
ref
subst
1053
remove
192
ref
subst
218
ref
nil
220
ref
1045
ref
cons
nil
cons
cons
1054
def
184
ref
subst
proveHyp
1054
ref
143
ref
subst
1054
remove
192
ref
subst
48
ref
"_32324"
15
ref
var
1055
def
1020
ref
1026
ref
1055
remove
varTerm
1056
def
appTerm
appTerm
1028
ref
33
ref
1056
remove
appTerm
appTerm
appTerm
absTerm
1057
def
34
ref
appTerm
1058
def
appTerm
refl
1059
def
1057
ref
114
ref
appTerm
betaConv
appThm
164
ref
1058
remove
betaConv
1060
def
appThm
1061
def
1020
ref
1026
ref
114
ref
appTerm
appTerm
1028
ref
232
ref
appTerm
appTerm
refl
appThm
trans
1057
remove
refl
1062
def
236
ref
appThm
eqMp
sym
1020
ref
refl
1063
def
nil
244
ref
"p"
1021
ref
var
1025
ref
nil
cons
cons
nil
cons
1064
def
cons
nil
cons
cons
347
ref
"B"
531
ref
cons
nil
cons
1065
def
cons
43
ref
cons
1066
def
351
ref
subst
subst
248
ref
0
ref
1019
ref
0
ref
0
ref
249
ref
530
ref
90
ref
cons
opType
1067
def
1022
ref
cons
opType
1068
def
0
ref
252
remove
1067
ref
nil
cons
1069
def
opType
1070
def
1022
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
98
remove
1019
ref
constTerm
1071
def
appTerm
257
ref
0
ref
0
ref
1068
ref
8
ref
cons
opType
1072
def
1068
ref
nil
cons
1073
def
cons
opType
constTerm
1074
def
"f"
1068
ref
var
1075
def
12
ref
0
ref
544
ref
8
ref
cons
opType
constTerm
1076
def
"y"
530
ref
var
1077
def
18
ref
75
ref
1020
ref
1075
ref
varTerm
266
ref
0
ref
530
ref
0
ref
15
ref
1069
ref
cons
opType
nil
cons
cons
opType
constTerm
1078
def
1077
ref
varTerm
1079
def
appTerm
79
ref
appTerm
1080
def
appTerm
appTerm
108
remove
0
ref
530
ref
0
ref
1019
ref
1022
ref
cons
opType
nil
cons
cons
opType
constTerm
1081
def
1079
ref
appTerm
1082
def
1038
remove
appTerm
1083
def
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
1084
def
appTerm
1085
def
refl
1086
def
245
ref
19
ref
45
ref
0
ref
1070
ref
0
ref
1070
ref
8
ref
cons
opType
nil
cons
cons
opType
constTerm
1087
def
276
remove
0
ref
1021
remove
0
ref
2
ref
0
ref
15
ref
1070
ref
nil
cons
1088
def
cons
opType
1089
def
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
1025
remove
appTerm
111
ref
appTerm
34
ref
appTerm
appTerm
248
remove
0
ref
1070
ref
0
ref
0
ref
250
ref
1088
ref
cons
opType
1090
def
0
ref
254
ref
1088
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
356
remove
1070
ref
constTerm
1091
def
appTerm
257
ref
0
ref
0
ref
1090
ref
8
ref
cons
opType
1092
def
1090
ref
nil
cons
1093
def
cons
opType
constTerm
1094
def
"f"
1090
ref
var
1095
def
264
ref
265
ref
18
ref
75
ref
1087
ref
1095
ref
varTerm
269
ref
appTerm
appTerm
359
remove
0
ref
1067
ref
1088
ref
cons
opType
constTerm
1096
def
1078
ref
1024
ref
268
ref
appTerm
1097
def
appTerm
1098
def
79
ref
appTerm
1099
def
appTerm
1100
def
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
1101
def
appTerm
1102
def
281
ref
appTerm
appTerm
absTerm
1103
def
34
ref
appTerm
1104
def
betaConv
57
ref
18
ref
1103
ref
appTerm
1105
def
absTerm
1106
def
111
ref
appTerm
1107
def
betaConv
1018
remove
51
ref
1106
ref
appTerm
1108
def
absTerm
1109
def
1024
ref
appTerm
1110
def
betaConv
11
ref
1017
remove
1109
ref
appTerm
1111
def
absTerm
1112
def
32
ref
appTerm
1113
def
betaConv
nil
298
ref
1112
ref
appTerm
1114
def
axiom
nil
125
ref
1114
remove
nil
cons
cons
126
ref
1113
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
42
ref
10
ref
1112
remove
nil
cons
cons
340
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1111
remove
nil
cons
cons
126
ref
1110
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1036
remove
1035
remove
1109
remove
nil
cons
cons
"x"
532
remove
var
1024
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1108
remove
nil
cons
cons
126
ref
1107
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
1106
remove
nil
cons
cons
350
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1105
remove
nil
cons
cons
126
ref
1104
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
1103
remove
nil
cons
cons
187
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
appThm
trans
appThm
1028
ref
refl
1115
def
352
ref
appThm
appThm
sym
373
ref
nil
385
ref
126
ref
1020
ref
1085
ref
1102
ref
374
ref
appTerm
appTerm
appTerm
1028
ref
386
ref
appTerm
appTerm
1116
def
nil
cons
1117
def
cons
nil
cons
1118
def
cons
nil
cons
cons
1119
def
184
ref
subst
proveHyp
1119
ref
143
ref
subst
1119
remove
192
ref
subst
nil
391
ref
265
ref
393
remove
1116
ref
appTerm
1120
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
398
ref
subst
265
ref
nil
68
ref
1120
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
400
remove
1118
ref
cons
nil
cons
cons
1121
def
143
ref
subst
1121
remove
192
ref
subst
402
remove
nil
403
remove
1118
ref
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
73
ref
75
ref
405
remove
1116
ref
appTerm
1122
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
75
ref
nil
68
ref
1122
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
408
remove
1118
ref
cons
nil
cons
cons
1123
def
143
ref
subst
1123
remove
192
ref
subst
410
remove
nil
412
remove
1118
ref
cons
nil
cons
cons
1124
def
184
ref
subst
proveHyp
1124
ref
143
ref
subst
1124
remove
192
ref
subst
416
remove
417
remove
48
ref
"_32332"
254
ref
var
1125
def
1020
ref
1085
ref
1102
ref
1125
remove
varTerm
1126
def
appTerm
appTerm
appTerm
1028
ref
275
ref
1126
remove
appTerm
appTerm
appTerm
absTerm
1127
def
374
ref
appTerm
1128
def
appTerm
refl
1129
def
1127
ref
361
ref
appTerm
betaConv
appThm
164
ref
1128
remove
betaConv
appThm
1130
def
1020
ref
1085
ref
1102
ref
361
ref
appTerm
appTerm
appTerm
1028
ref
275
ref
361
ref
appTerm
appTerm
appTerm
refl
appThm
trans
1127
remove
refl
1131
def
419
remove
appThm
eqMp
sym
1063
ref
1086
ref
nil
421
ref
1095
remove
1101
remove
nil
cons
cons
"b"
1070
remove
var
1091
remove
nil
cons
cons
nil
cons
cons
1132
def
cons
nil
cons
cons
426
ref
"B"
1088
remove
cons
nil
cons
cons
43
ref
cons
1133
def
459
ref
subst
subst
75
ref
1087
ref
1094
remove
"_32344"
1090
ref
var
1134
def
264
ref
265
ref
18
ref
75
ref
1087
ref
1134
remove
varTerm
269
ref
appTerm
appTerm
1100
ref
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
1135
def
appTerm
1136
def
269
ref
appTerm
appTerm
1100
ref
appTerm
absTerm
1137
def
79
ref
appTerm
1138
def
betaConv
265
ref
18
ref
1137
ref
appTerm
1139
def
absTerm
1140
def
268
ref
appTerm
1141
def
betaConv
1135
ref
1136
remove
appTerm
1142
def
betaConv
1135
ref
"_32342"
250
ref
var
1143
def
1096
ref
1078
ref
1024
ref
478
remove
1143
remove
varTerm
1144
def
appTerm
appTerm
appTerm
482
remove
1144
remove
appTerm
appTerm
appTerm
absTerm
1145
def
appTerm
betaConv
sym
nil
391
ref
265
ref
18
ref
75
ref
1087
ref
1145
ref
269
remove
appTerm
1146
def
appTerm
1100
remove
appTerm
1147
def
absTerm
1148
def
appTerm
1149
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
398
ref
subst
265
ref
nil
68
ref
1149
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
73
ref
1148
remove
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
75
ref
nil
68
ref
1147
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
1146
remove
betaConv
1087
ref
"_32339"
15
ref
var
1150
def
1096
ref
1098
remove
1150
ref
varTerm
1151
def
appTerm
appTerm
absTerm
79
ref
appTerm
1152
def
appTerm
refl
1150
ref
1096
ref
1078
ref
1024
ref
491
ref
appTerm
appTerm
1153
def
1151
ref
appTerm
appTerm
absTerm
1154
def
494
ref
appTerm
betaConv
appThm
1087
remove
refl
1152
remove
betaConv
appThm
1096
ref
1153
remove
494
remove
appTerm
appTerm
refl
appThm
trans
45
ref
0
ref
1089
ref
0
ref
1089
remove
8
ref
cons
opType
nil
cons
cons
opType
constTerm
1155
def
"_32338"
3
ref
var
1156
def
1150
remove
1096
remove
1078
ref
1024
remove
1156
remove
varTerm
appTerm
appTerm
1151
remove
appTerm
appTerm
absTerm
absTerm
1157
def
268
ref
appTerm
1158
def
appTerm
refl
1157
ref
491
remove
appTerm
betaConv
appThm
1155
remove
refl
1158
remove
betaConv
appThm
1154
remove
refl
appThm
trans
1157
remove
refl
772
remove
appThm
eqMp
790
remove
appThm
eqMp
sym
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
"A"
1093
remove
cons
nil
cons
1159
def
"P"
1092
ref
var
1135
ref
nil
cons
1160
def
cons
"x"
1090
remove
var
1145
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
597
ref
subst
proveHyp
nil
125
ref
104
ref
0
ref
1092
ref
8
ref
cons
opType
constTerm
1135
remove
appTerm
nil
cons
cons
126
ref
1142
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
"p"
1092
remove
var
1160
remove
cons
nil
cons
nil
cons
cons
1159
remove
43
ref
cons
770
ref
subst
subst
eqMp
eqMp
nil
125
ref
264
ref
1140
ref
appTerm
nil
cons
cons
126
ref
1141
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
391
ref
1140
remove
nil
cons
cons
793
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1139
remove
nil
cons
cons
126
ref
1138
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
1137
remove
nil
cons
cons
794
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
trans
appThm
nil
"a"
1067
ref
var
1099
remove
nil
cons
cons
1075
remove
1084
remove
nil
cons
cons
"b"
1019
ref
var
1071
remove
nil
cons
1161
def
cons
nil
cons
cons
1162
def
cons
nil
cons
cons
"A"
1069
remove
cons
"B"
1022
ref
cons
nil
cons
cons
43
ref
cons
1163
def
459
remove
subst
subst
nil
1077
ref
1097
ref
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
1020
ref
1074
remove
"_32356"
1068
ref
var
1164
def
1076
ref
1077
ref
18
ref
75
ref
1020
ref
1164
remove
varTerm
1080
ref
appTerm
appTerm
1083
ref
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
1165
def
appTerm
1166
def
1080
ref
appTerm
appTerm
1083
ref
appTerm
absTerm
1167
def
79
ref
appTerm
1168
def
betaConv
1077
ref
18
ref
1167
ref
appTerm
1169
def
absTerm
1170
def
1079
ref
appTerm
1171
def
betaConv
1165
ref
1166
remove
appTerm
1172
def
betaConv
1165
ref
"_32354"
1067
ref
var
1173
def
1081
ref
257
ref
0
ref
0
ref
0
ref
1067
ref
531
ref
cons
opType
1174
def
8
ref
cons
opType
1174
ref
nil
cons
cons
opType
constTerm
"fn"
1174
remove
var
1175
def
1076
ref
"a"
530
ref
var
1176
def
18
ref
474
ref
545
remove
1175
remove
varTerm
1078
remove
1176
ref
varTerm
1177
def
appTerm
476
ref
appTerm
1178
def
appTerm
appTerm
1177
remove
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
1179
def
1173
remove
varTerm
1180
def
appTerm
appTerm
1026
ref
257
ref
0
ref
0
ref
0
ref
1067
remove
90
ref
cons
opType
1181
def
8
ref
cons
opType
1181
ref
nil
cons
cons
opType
constTerm
"fn"
1181
remove
var
1182
def
1076
ref
1176
ref
18
ref
474
remove
96
ref
1182
remove
varTerm
1178
remove
appTerm
appTerm
476
remove
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
1183
def
1180
remove
appTerm
appTerm
appTerm
absTerm
1184
def
appTerm
betaConv
sym
nil
"P"
544
remove
var
1185
def
1077
ref
18
ref
75
ref
1020
ref
1184
ref
1080
ref
appTerm
1186
def
appTerm
1083
remove
appTerm
1187
def
absTerm
1188
def
appTerm
1189
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
531
remove
cons
1190
def
nil
cons
1191
def
43
ref
cons
66
ref
subst
subst
1077
remove
nil
68
ref
1189
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
73
ref
1188
remove
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
75
ref
nil
68
ref
1187
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
1186
remove
betaConv
1020
ref
"_32351"
15
ref
var
1192
def
1082
remove
1026
ref
1192
ref
varTerm
appTerm
1193
def
appTerm
absTerm
79
ref
appTerm
1194
def
appTerm
refl
1192
ref
1081
ref
1179
remove
1080
ref
appTerm
1195
def
appTerm
1196
def
1193
ref
appTerm
absTerm
1197
def
1183
remove
1080
remove
appTerm
1198
def
appTerm
betaConv
appThm
1063
ref
1194
remove
betaConv
appThm
1196
remove
1026
ref
1198
remove
appTerm
appTerm
refl
appThm
trans
45
ref
0
ref
1023
ref
0
ref
1023
remove
8
ref
cons
opType
nil
cons
cons
opType
constTerm
1199
def
"_32350"
530
ref
var
1200
def
1192
remove
1081
ref
1200
remove
varTerm
appTerm
1193
remove
appTerm
absTerm
absTerm
1201
def
1079
ref
appTerm
1202
def
appTerm
refl
1201
ref
1195
remove
appTerm
betaConv
appThm
1199
remove
refl
1202
remove
betaConv
appThm
1197
remove
refl
appThm
trans
1201
remove
refl
nil
501
remove
1176
remove
1079
remove
nil
cons
1203
def
cons
nil
cons
cons
nil
cons
cons
1204
def
1190
remove
505
remove
cons
43
ref
cons
1205
def
771
ref
subst
subst
appThm
eqMp
1204
remove
1205
remove
789
ref
subst
subst
appThm
eqMp
sym
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
"A"
1073
remove
cons
nil
cons
1206
def
"P"
1072
ref
var
1165
ref
nil
cons
1207
def
cons
"x"
1068
remove
var
1184
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
597
ref
subst
proveHyp
nil
125
ref
104
ref
0
ref
1072
ref
8
ref
cons
opType
constTerm
1165
remove
appTerm
nil
cons
cons
126
ref
1172
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
"p"
1072
remove
var
1207
remove
cons
nil
cons
nil
cons
cons
1206
remove
43
ref
cons
770
ref
subst
subst
eqMp
eqMp
nil
125
ref
1076
remove
1170
ref
appTerm
nil
cons
cons
126
ref
1171
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1191
remove
1185
remove
1170
remove
nil
cons
cons
"x"
530
remove
var
1203
remove
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1169
remove
nil
cons
cons
126
ref
1168
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
1167
remove
nil
cons
cons
794
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
trans
trans
appThm
1115
ref
796
remove
appThm
798
remove
395
ref
1065
remove
cons
43
ref
cons
1208
def
19
ref
246
ref
1027
remove
0
ref
431
ref
31
ref
cons
opType
constTerm
436
ref
appTerm
1209
def
247
ref
appTerm
appTerm
271
ref
436
ref
111
ref
appTerm
appTerm
1209
ref
34
ref
appTerm
appTerm
appTerm
absTerm
1210
def
34
ref
appTerm
1211
def
betaConv
57
ref
18
ref
1210
ref
appTerm
1212
def
absTerm
1213
def
111
ref
appTerm
1214
def
betaConv
435
ref
51
ref
1213
ref
appTerm
1215
def
absTerm
1216
def
436
ref
appTerm
1217
def
betaConv
nil
132
ref
447
ref
435
ref
246
ref
1209
ref
99
ref
appTerm
appTerm
256
ref
appTerm
absTerm
1218
def
appTerm
1219
def
appTerm
132
ref
447
ref
435
ref
246
ref
1209
remove
102
ref
appTerm
appTerm
292
ref
appTerm
absTerm
1220
def
appTerm
1221
def
appTerm
447
ref
1216
ref
appTerm
1222
def
appTerm
1223
def
appTerm
axiom
1224
def
nil
161
ref
1219
remove
nil
cons
1225
def
cons
162
ref
1223
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
1226
def
343
ref
subst
proveHyp
1227
def
nil
161
ref
1221
remove
nil
cons
1228
def
cons
162
ref
1222
remove
nil
cons
1229
def
cons
nil
cons
cons
nil
cons
cons
1230
def
343
ref
subst
proveHyp
nil
125
ref
1229
remove
cons
126
ref
1217
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
454
ref
455
ref
1216
remove
nil
cons
cons
457
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1215
remove
nil
cons
cons
126
ref
1214
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
1213
remove
nil
cons
cons
350
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1212
remove
nil
cons
cons
126
ref
1211
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
1210
remove
nil
cons
cons
187
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
subst
trans
appThm
sym
1081
remove
1097
remove
appTerm
refl
849
remove
nil
850
remove
126
ref
1039
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
75
ref
229
ref
1039
ref
appTerm
absTerm
1231
def
79
ref
appTerm
1232
def
betaConv
48
ref
"_32326"
15
ref
var
1233
def
18
ref
75
ref
74
ref
80
ref
1233
remove
varTerm
appTerm
appTerm
1039
remove
appTerm
absTerm
appTerm
absTerm
1234
def
34
ref
appTerm
1235
def
appTerm
refl
1234
ref
114
ref
appTerm
betaConv
appThm
164
ref
1235
remove
betaConv
appThm
18
ref
1231
ref
appTerm
1236
def
refl
appThm
trans
1234
remove
refl
236
ref
appThm
eqMp
1040
remove
assume
eqMp
nil
125
ref
1236
remove
nil
cons
cons
126
ref
1232
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
1231
remove
nil
cons
cons
794
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
eqMp
appThm
eqMp
eqMp
proveHyp
proveHyp
eqMp
nil
911
remove
162
ref
1117
ref
cons
nil
cons
1237
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
913
remove
1237
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
18
ref
185
ref
915
remove
1116
ref
appTerm
absTerm
appTerm
nil
cons
cons
126
ref
916
remove
1116
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
917
remove
1237
ref
cons
nil
cons
cons
623
ref
subst
eqMp
eqMp
eqMp
nil
918
remove
1237
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
264
ref
452
ref
920
ref
1116
ref
appTerm
absTerm
appTerm
nil
cons
cons
126
ref
921
ref
1116
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
922
ref
1237
ref
cons
nil
cons
cons
623
ref
subst
eqMp
nil
924
ref
1118
remove
cons
nil
cons
cons
1238
def
143
ref
subst
1238
remove
192
ref
subst
1129
remove
"_32328"
254
ref
var
1239
def
1020
ref
1085
ref
1102
ref
1239
remove
varTerm
1240
def
appTerm
appTerm
appTerm
1028
ref
275
ref
1240
remove
appTerm
appTerm
appTerm
absTerm
357
ref
appTerm
betaConv
appThm
1130
remove
1020
ref
1085
remove
1102
remove
357
ref
appTerm
appTerm
appTerm
1028
ref
275
ref
357
ref
appTerm
1241
def
appTerm
appTerm
refl
appThm
trans
1131
remove
926
ref
appThm
eqMp
sym
1063
ref
1086
remove
nil
1132
remove
nil
cons
cons
1133
remove
934
ref
subst
subst
appThm
nil
1162
remove
nil
cons
cons
1163
remove
934
remove
subst
subst
trans
appThm
1115
ref
936
ref
appThm
1208
ref
1218
ref
436
ref
appTerm
1242
def
betaConv
1224
remove
1226
remove
176
ref
subst
proveHyp
nil
125
ref
1225
remove
cons
126
ref
1242
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
454
ref
455
ref
1218
remove
nil
cons
cons
457
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
1243
def
trans
appThm
nil
"x"
1019
ref
var
1244
def
1161
remove
cons
nil
cons
nil
cons
cons
"A"
1022
remove
cons
nil
cons
43
ref
cons
nil
68
ref
507
ref
111
ref
appTerm
111
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
193
remove
eqMp
1245
def
subst
1246
def
subst
1247
def
trans
sym
71
ref
eqMp
eqMp
eqMp
nil
945
ref
1237
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
945
ref
946
ref
947
ref
1117
remove
cons
nil
cons
cons
cons
nil
cons
cons
962
ref
subst
proveHyp
proveHyp
eqMp
nil
963
ref
1237
remove
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
nil
964
ref
162
ref
1044
ref
cons
nil
cons
1248
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
966
ref
1248
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
18
ref
185
ref
967
ref
1029
ref
appTerm
absTerm
appTerm
nil
cons
cons
126
ref
968
ref
1029
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
969
ref
1248
ref
cons
nil
cons
cons
623
ref
subst
eqMp
eqMp
eqMp
nil
970
ref
1248
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
51
ref
1050
remove
appTerm
nil
cons
cons
126
ref
971
ref
1029
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
972
ref
1248
ref
cons
nil
cons
cons
623
ref
subst
eqMp
nil
974
ref
1045
ref
cons
nil
cons
cons
1249
def
143
ref
subst
1249
remove
192
ref
subst
1059
ref
"_32320"
15
ref
var
1250
def
1020
ref
1026
ref
1250
remove
varTerm
1251
def
appTerm
appTerm
1028
ref
33
ref
1251
remove
appTerm
appTerm
appTerm
absTerm
102
ref
appTerm
betaConv
appThm
1061
ref
1020
ref
1026
ref
102
ref
appTerm
appTerm
1028
ref
290
ref
appTerm
appTerm
refl
appThm
trans
1062
ref
981
ref
appThm
eqMp
sym
1063
ref
nil
1064
remove
nil
cons
cons
1252
def
1066
ref
982
ref
subst
subst
appThm
1115
ref
982
ref
appThm
1208
remove
1220
ref
436
ref
appTerm
1253
def
betaConv
1227
remove
1230
remove
176
ref
subst
proveHyp
nil
125
ref
1228
remove
cons
126
ref
1253
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
454
ref
455
ref
1220
remove
nil
cons
cons
457
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
trans
appThm
nil
1244
remove
101
remove
1019
remove
constTerm
nil
cons
cons
nil
cons
nil
cons
cons
1246
remove
subst
trans
sym
71
ref
eqMp
eqMp
eqMp
nil
989
ref
1248
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
989
ref
990
ref
947
ref
1044
remove
cons
nil
cons
1254
def
cons
cons
nil
cons
cons
962
ref
subst
proveHyp
proveHyp
eqMp
nil
992
ref
1248
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
994
ref
1045
remove
cons
nil
cons
cons
1255
def
143
ref
subst
1255
remove
192
ref
subst
1059
remove
"_32316"
15
ref
var
1256
def
1020
ref
1026
ref
1256
remove
varTerm
1257
def
appTerm
appTerm
1028
ref
33
ref
1257
remove
appTerm
appTerm
appTerm
absTerm
99
ref
appTerm
betaConv
appThm
1061
remove
1020
remove
1026
remove
99
ref
appTerm
appTerm
1028
remove
287
ref
appTerm
appTerm
refl
appThm
trans
1062
remove
1000
ref
appThm
eqMp
sym
1063
remove
1252
remove
1066
remove
1001
ref
subst
subst
appThm
1115
remove
1001
ref
appThm
1243
remove
trans
appThm
1247
remove
trans
sym
71
ref
eqMp
eqMp
eqMp
nil
1002
ref
1248
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
1002
ref
1003
ref
1254
remove
cons
cons
nil
cons
cons
962
ref
subst
proveHyp
proveHyp
eqMp
nil
1004
ref
1248
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
161
ref
1043
remove
cons
1248
remove
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
18
ref
1042
remove
appTerm
nil
cons
cons
126
ref
1037
remove
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1005
ref
1006
ref
19
ref
1005
ref
1006
ref
75
ref
1007
ref
1030
ref
79
ref
appTerm
betaConv
appThm
absThm
appThm
appThm
1060
ref
appThm
absThm
appThm
appThm
1006
ref
19
ref
1060
remove
absThm
appThm
appThm
nil
1009
ref
1030
remove
nil
cons
cons
nil
cons
nil
cons
cons
1015
ref
subst
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
298
ref
1034
remove
appTerm
thm
nil
10
ref
11
ref
12
ref
0
ref
0
ref
0
ref
3
ref
"Data.List.list"
typeOp
1258
def
14
remove
opType
1259
def
nil
cons
1260
def
cons
opType
1261
def
8
ref
cons
opType
1262
def
8
ref
cons
opType
constTerm
1263
def
"e"
1261
ref
var
1264
def
12
ref
0
ref
0
ref
1258
ref
4
ref
opType
1265
def
8
ref
cons
1266
def
opType
1267
def
8
ref
cons
opType
1268
def
constTerm
1269
def
"l"
1265
ref
var
1270
def
74
ref
"Parser.inverse"
const
0
ref
6
ref
1262
ref
nil
cons
cons
opType
1271
def
constTerm
32
ref
appTerm
1264
ref
varTerm
1272
def
appTerm
1273
def
appTerm
1274
def
246
ref
33
ref
"Parser.Stream.fromList"
const
1275
def
0
ref
1259
ref
90
remove
cons
opType
constTerm
1276
def
"Data.List.concat"
const
0
ref
1258
remove
1260
ref
opType
1277
def
1260
ref
cons
opType
constTerm
1278
def
"Data.List.map"
const
1279
def
0
ref
1261
ref
0
ref
1265
ref
1277
ref
nil
cons
1280
def
cons
opType
nil
cons
cons
opType
constTerm
1272
ref
appTerm
1281
def
1270
ref
varTerm
1282
def
appTerm
appTerm
appTerm
appTerm
appTerm
1275
remove
0
ref
1265
ref
29
ref
cons
opType
constTerm
1283
def
1282
ref
appTerm
appTerm
1284
def
appTerm
1285
def
absTerm
1286
def
appTerm
1287
def
absTerm
1288
def
appTerm
1289
def
absTerm
1290
def
nil
cons
cons
nil
cons
nil
cons
cons
67
ref
subst
11
ref
nil
68
ref
1289
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
"P"
1262
remove
var
1291
def
1288
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
1261
ref
nil
cons
cons
nil
cons
1292
def
43
ref
cons
66
ref
subst
1293
def
subst
1264
ref
nil
68
ref
1287
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
"P"
1267
ref
var
1294
def
1286
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
1265
ref
nil
cons
1295
def
cons
1296
def
nil
cons
1297
def
43
ref
cons
66
ref
subst
1298
def
subst
1270
ref
nil
68
ref
1285
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
1273
ref
nil
cons
1299
def
cons
1300
def
126
ref
1284
ref
nil
cons
1301
def
cons
nil
cons
cons
nil
cons
cons
1302
def
143
ref
subst
1302
remove
192
ref
subst
1270
ref
1284
remove
absTerm
1303
def
1282
ref
appTerm
1304
def
betaConv
1305
def
495
ref
33
ref
refl
1306
def
nil
"l"
1259
ref
var
1307
def
1278
ref
1281
ref
"Data.List.[]"
const
1308
def
1265
ref
constTerm
1309
def
appTerm
appTerm
1310
def
nil
cons
cons
nil
cons
nil
cons
cons
1307
ref
96
ref
1276
ref
1307
ref
varTerm
1311
def
appTerm
appTerm
"Parser.Stream.append"
const
1312
def
0
ref
1259
ref
109
remove
cons
opType
constTerm
1313
def
1311
ref
appTerm
102
ref
appTerm
appTerm
absTerm
1314
def
1311
ref
appTerm
1315
def
betaConv
nil
12
ref
0
ref
0
ref
1259
ref
8
ref
cons
1316
def
opType
1317
def
8
ref
cons
opType
1318
def
constTerm
1319
def
1314
ref
appTerm
1320
def
axiom
nil
125
ref
1320
remove
nil
cons
cons
126
ref
1315
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
"A"
1260
ref
cons
nil
cons
1321
def
"P"
1317
ref
var
1322
def
1314
remove
nil
cons
cons
"x"
1259
ref
var
1323
def
1311
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
1324
def
subst
1313
ref
refl
1325
def
1278
ref
refl
1326
def
nil
"f"
1261
ref
var
1272
ref
nil
cons
1327
def
cons
nil
cons
1328
def
nil
cons
cons
1329
def
395
remove
"B"
1260
ref
cons
nil
cons
cons
43
ref
cons
1330
def
435
ref
45
ref
0
ref
1265
ref
1267
ref
nil
cons
cons
opType
constTerm
1331
def
1279
remove
0
ref
431
remove
0
ref
1259
ref
1295
ref
cons
opType
nil
cons
cons
opType
constTerm
436
ref
appTerm
1332
def
1308
ref
1259
ref
constTerm
1333
def
appTerm
appTerm
1309
ref
appTerm
absTerm
1334
def
436
ref
appTerm
1335
def
betaConv
nil
447
ref
1334
ref
appTerm
1336
def
axiom
nil
125
ref
1336
remove
nil
cons
cons
126
ref
1335
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
454
ref
455
ref
1334
remove
nil
cons
cons
457
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
subst
appThm
nil
45
ref
0
ref
1259
ref
1317
ref
nil
cons
1337
def
cons
opType
constTerm
1338
def
1278
ref
1308
remove
1277
ref
constTerm
appTerm
appTerm
1333
ref
appTerm
axiom
trans
appThm
102
ref
refl
1339
def
appThm
nil
19
ref
102
ref
nil
cons
1340
def
cons
nil
cons
nil
cons
cons
19
ref
96
ref
1313
ref
1333
ref
appTerm
34
ref
appTerm
appTerm
34
ref
appTerm
absTerm
1341
def
34
ref
appTerm
1342
def
betaConv
nil
132
ref
18
ref
1341
ref
appTerm
1343
def
appTerm
51
ref
"h"
2
ref
var
1344
def
1319
ref
"t"
1259
ref
var
1345
def
18
ref
19
ref
96
ref
1313
ref
"Data.List.::"
const
1346
def
0
ref
2
ref
0
ref
1259
ref
1260
remove
cons
opType
nil
cons
1347
def
cons
opType
constTerm
1348
def
1344
ref
varTerm
1349
def
appTerm
1345
ref
varTerm
1350
def
appTerm
1351
def
appTerm
34
ref
appTerm
appTerm
110
remove
1349
ref
appTerm
1313
ref
1350
ref
appTerm
34
ref
appTerm
1352
def
appTerm
appTerm
absTerm
1353
def
appTerm
1354
def
absTerm
1355
def
appTerm
1356
def
absTerm
1357
def
appTerm
1358
def
appTerm
axiom
1359
def
nil
161
ref
1343
remove
nil
cons
1360
def
cons
162
ref
1358
remove
nil
cons
1361
def
cons
nil
cons
cons
nil
cons
cons
1362
def
176
ref
subst
proveHyp
nil
125
ref
1360
remove
cons
126
ref
1342
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
1341
remove
nil
cons
cons
187
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
1363
def
subst
trans
trans
1364
def
appThm
982
ref
trans
appThm
nil
1270
ref
1309
ref
nil
cons
1365
def
cons
nil
cons
nil
cons
cons
397
ref
1324
ref
subst
1366
def
subst
nil
797
ref
292
ref
nil
cons
1367
def
cons
nil
cons
nil
cons
cons
1368
def
397
ref
1363
ref
subst
subst
trans
appThm
nil
"x"
25
ref
var
1369
def
1367
ref
cons
nil
cons
nil
cons
cons
"A"
29
remove
cons
nil
cons
43
ref
cons
1245
ref
subst
1370
def
subst
1371
def
trans
sym
71
ref
eqMp
nil
125
ref
246
ref
33
ref
1276
ref
1310
remove
appTerm
1372
def
appTerm
appTerm
1283
ref
1309
ref
appTerm
appTerm
1373
def
nil
cons
cons
126
ref
264
ref
"h"
3
ref
var
1374
def
1269
ref
"t"
1265
ref
var
1375
def
74
ref
246
ref
33
ref
1276
ref
1278
ref
1281
ref
1375
ref
varTerm
1376
def
appTerm
1377
def
appTerm
1378
def
appTerm
appTerm
appTerm
1283
ref
1376
ref
appTerm
appTerm
appTerm
246
ref
33
ref
1276
ref
1278
ref
1281
ref
1346
ref
0
ref
3
ref
0
ref
1265
ref
1295
ref
cons
opType
nil
cons
cons
opType
constTerm
1379
def
1374
ref
varTerm
1380
def
appTerm
1376
ref
appTerm
1381
def
appTerm
appTerm
1382
def
appTerm
appTerm
appTerm
1283
remove
1381
ref
appTerm
appTerm
appTerm
1383
def
absTerm
1384
def
appTerm
1385
def
absTerm
1386
def
appTerm
1387
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
192
ref
subst
proveHyp
nil
391
ref
1386
remove
nil
cons
cons
nil
cons
nil
cons
cons
398
ref
subst
1374
ref
nil
68
ref
1385
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
1294
ref
1384
remove
nil
cons
cons
nil
cons
nil
cons
cons
1298
ref
subst
1375
ref
nil
68
ref
1383
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
1005
ref
495
ref
1306
ref
nil
1307
ref
1378
ref
nil
cons
1388
def
cons
nil
cons
nil
cons
cons
1324
ref
subst
appThm
appThm
nil
1270
ref
1376
ref
nil
cons
cons
nil
cons
nil
cons
cons
1366
ref
subst
appThm
appThm
495
ref
1306
ref
nil
1307
ref
1382
remove
nil
cons
cons
nil
cons
nil
cons
cons
1324
ref
subst
1325
ref
1326
ref
1329
remove
1330
remove
1345
ref
1331
ref
1332
ref
1351
ref
appTerm
appTerm
1379
ref
436
ref
1349
ref
appTerm
appTerm
1332
remove
1350
ref
appTerm
appTerm
appTerm
absTerm
1389
def
1350
ref
appTerm
1390
def
betaConv
1344
ref
1319
ref
1389
ref
appTerm
1391
def
absTerm
1392
def
1349
ref
appTerm
1393
def
betaConv
435
remove
51
ref
1392
ref
appTerm
1394
def
absTerm
1395
def
436
remove
appTerm
1396
def
betaConv
nil
447
remove
1395
ref
appTerm
1397
def
axiom
nil
125
ref
1397
remove
nil
cons
cons
126
ref
1396
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
454
remove
455
remove
1395
remove
nil
cons
cons
457
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1394
remove
nil
cons
cons
126
ref
1393
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
1392
remove
nil
cons
cons
57
ref
1349
ref
nil
cons
cons
nil
cons
1398
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1391
remove
nil
cons
cons
126
ref
1390
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1321
ref
1322
ref
1389
remove
nil
cons
cons
1323
ref
1350
ref
nil
cons
cons
nil
cons
1399
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
1400
def
subst
appThm
nil
"t"
1277
ref
var
1401
def
1377
remove
nil
cons
cons
"h"
1259
ref
var
1402
def
1272
ref
1380
ref
appTerm
1403
def
nil
cons
1404
def
cons
nil
cons
cons
nil
cons
cons
1401
ref
1338
ref
1278
ref
1346
remove
0
ref
1259
ref
0
ref
1277
ref
1280
ref
cons
opType
nil
cons
cons
opType
constTerm
1402
ref
varTerm
1405
def
appTerm
1401
ref
varTerm
1406
def
appTerm
appTerm
appTerm
"Data.List.@"
const
0
ref
1259
ref
1347
remove
cons
opType
constTerm
1407
def
1405
ref
appTerm
1278
ref
1406
ref
appTerm
appTerm
appTerm
absTerm
1408
def
1406
ref
appTerm
1409
def
betaConv
1402
ref
12
ref
0
ref
0
ref
1277
ref
8
ref
cons
opType
1410
def
8
ref
cons
opType
constTerm
1408
ref
appTerm
1411
def
absTerm
1412
def
1405
ref
appTerm
1413
def
betaConv
nil
1319
ref
1412
ref
appTerm
1414
def
axiom
nil
125
ref
1414
remove
nil
cons
cons
126
ref
1413
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1321
ref
1322
ref
1412
remove
nil
cons
cons
1323
ref
1405
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1411
remove
nil
cons
cons
126
ref
1409
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
"A"
1280
remove
cons
nil
cons
"P"
1410
remove
var
1408
remove
nil
cons
cons
"x"
1277
remove
var
1406
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
1415
def
subst
trans
appThm
1339
ref
appThm
trans
appThm
appThm
nil
1270
ref
1381
ref
nil
cons
cons
nil
cons
nil
cons
cons
1366
remove
subst
1368
remove
397
ref
1353
ref
34
ref
appTerm
1416
def
betaConv
1355
ref
1350
ref
appTerm
1417
def
betaConv
1357
ref
1349
ref
appTerm
1418
def
betaConv
1359
remove
1362
remove
343
ref
subst
proveHyp
nil
125
ref
1361
remove
cons
126
ref
1418
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
1357
remove
nil
cons
cons
1398
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1356
remove
nil
cons
cons
126
ref
1417
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1321
ref
1322
ref
1355
remove
nil
cons
cons
1399
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1354
remove
nil
cons
cons
126
ref
1416
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
1353
remove
nil
cons
cons
187
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
1419
def
subst
subst
trans
appThm
appThm
sym
nil
125
ref
246
ref
33
ref
1313
ref
1378
ref
appTerm
102
ref
appTerm
1420
def
appTerm
1421
def
appTerm
1312
remove
0
ref
1265
ref
270
remove
cons
opType
constTerm
1376
ref
appTerm
292
ref
appTerm
1422
def
appTerm
1423
def
nil
cons
1424
def
cons
126
ref
246
ref
33
ref
1313
ref
1407
ref
1403
ref
appTerm
1378
remove
appTerm
appTerm
102
ref
appTerm
appTerm
appTerm
1425
def
271
ref
1380
ref
appTerm
1426
def
1422
remove
appTerm
appTerm
nil
cons
1427
def
cons
nil
cons
cons
nil
cons
cons
1428
def
143
ref
subst
1428
remove
192
ref
subst
1425
remove
refl
1426
ref
refl
1423
remove
assume
sym
appThm
appThm
sym
495
ref
1306
ref
nil
"zs"
15
ref
var
1429
def
1340
ref
cons
1430
def
"ys"
1259
ref
var
1431
def
1388
remove
cons
"xs"
1259
ref
var
1432
def
1404
remove
cons
nil
cons
cons
cons
nil
cons
cons
1429
ref
96
ref
1313
ref
1407
remove
1432
ref
varTerm
1433
def
appTerm
1431
ref
varTerm
1434
def
appTerm
appTerm
1429
ref
varTerm
1435
def
appTerm
appTerm
1313
ref
1433
ref
appTerm
1313
ref
1434
ref
appTerm
1435
ref
appTerm
appTerm
appTerm
absTerm
1436
def
1435
ref
appTerm
1437
def
betaConv
1431
ref
18
ref
1436
ref
appTerm
1438
def
absTerm
1439
def
1434
ref
appTerm
1440
def
betaConv
1432
ref
1319
ref
1439
ref
appTerm
1441
def
absTerm
1442
def
1433
ref
appTerm
1443
def
betaConv
nil
1319
ref
1442
ref
appTerm
1444
def
axiom
nil
125
ref
1444
remove
nil
cons
cons
126
ref
1443
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1321
ref
1322
ref
1442
remove
nil
cons
cons
1323
ref
1433
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1441
remove
nil
cons
cons
126
ref
1440
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1321
ref
1322
ref
1439
remove
nil
cons
cons
1323
ref
1434
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1438
remove
nil
cons
cons
126
ref
1437
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
1436
remove
nil
cons
cons
185
ref
1435
ref
nil
cons
1445
def
cons
nil
cons
1446
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
1447
def
subst
appThm
appThm
1426
remove
1421
remove
appTerm
1448
def
refl
appThm
sym
nil
1300
remove
126
ref
246
ref
33
ref
1313
ref
1403
remove
appTerm
1420
ref
appTerm
appTerm
appTerm
1448
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
nil
452
ref
1380
remove
nil
cons
cons
19
ref
1420
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
19
ref
1274
remove
246
ref
33
ref
1313
ref
1272
ref
919
ref
appTerm
1449
def
appTerm
34
ref
appTerm
1450
def
appTerm
appTerm
271
remove
919
ref
appTerm
35
ref
appTerm
1451
def
appTerm
1452
def
appTerm
absTerm
1453
def
34
ref
appTerm
1454
def
betaConv
11
ref
18
ref
1453
ref
appTerm
1455
def
absTerm
1456
def
32
ref
appTerm
1457
def
betaConv
452
ref
298
ref
1456
ref
appTerm
1458
def
absTerm
1459
def
919
ref
appTerm
1460
def
betaConv
1264
ref
264
ref
1459
ref
appTerm
1461
def
absTerm
1462
def
1272
ref
appTerm
1463
def
betaConv
303
ref
11
ref
1263
ref
refl
1264
ref
526
ref
452
ref
1006
ref
19
ref
1005
ref
1264
ref
48
ref
1273
ref
appTerm
264
ref
452
ref
18
ref
19
ref
354
ref
"Parser.apply"
const
0
ref
6
remove
278
remove
cons
opType
constTerm
32
ref
appTerm
1464
def
1450
remove
appTerm
appTerm
360
ref
267
ref
919
ref
appTerm
34
ref
appTerm
1465
def
appTerm
1466
def
appTerm
1467
def
absTerm
1468
def
appTerm
1469
def
absTerm
1470
def
appTerm
1471
def
appTerm
absTerm
1472
def
1272
ref
appTerm
1473
def
betaConv
11
ref
1263
ref
1472
ref
appTerm
1474
def
absTerm
1475
def
32
ref
appTerm
1476
def
betaConv
nil
298
ref
1475
ref
appTerm
1477
def
axiom
nil
125
ref
1477
remove
nil
cons
cons
126
ref
1476
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
42
ref
10
ref
1475
remove
nil
cons
cons
340
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1474
remove
nil
cons
cons
126
ref
1473
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1292
ref
1291
ref
1472
remove
nil
cons
cons
"x"
1261
remove
var
1327
remove
cons
nil
cons
1478
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
appThm
1452
ref
refl
appThm
absThm
appThm
absThm
appThm
absThm
appThm
absThm
appThm
sym
nil
10
ref
11
ref
1263
ref
1264
ref
264
ref
452
ref
18
ref
19
ref
74
ref
1471
ref
appTerm
1452
ref
appTerm
1479
def
absTerm
1480
def
appTerm
1481
def
absTerm
1482
def
appTerm
1483
def
absTerm
1484
def
appTerm
1485
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
67
ref
subst
11
ref
nil
68
ref
1485
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
1291
ref
1484
remove
nil
cons
cons
nil
cons
nil
cons
cons
1293
ref
subst
1264
ref
nil
68
ref
1483
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
391
ref
1482
remove
nil
cons
cons
nil
cons
nil
cons
cons
398
ref
subst
452
ref
nil
68
ref
1481
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
73
ref
1480
remove
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
19
ref
nil
68
ref
1479
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
1471
remove
nil
cons
1486
def
cons
1487
def
126
ref
1452
ref
nil
cons
1488
def
cons
nil
cons
1489
def
cons
nil
cons
cons
1490
def
143
ref
subst
1490
remove
192
ref
subst
1468
ref
34
ref
appTerm
1491
def
betaConv
1470
ref
919
ref
appTerm
1492
def
betaConv
nil
1487
remove
126
ref
1492
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
396
ref
391
ref
1470
remove
nil
cons
cons
452
ref
919
ref
nil
cons
1493
def
cons
nil
cons
1494
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1469
remove
nil
cons
cons
126
ref
1491
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
1468
remove
nil
cons
cons
187
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1467
ref
nil
cons
cons
1489
remove
cons
nil
cons
cons
184
ref
subst
proveHyp
1307
ref
95
ref
1338
ref
1311
ref
appTerm
1495
def
1333
ref
appTerm
appTerm
105
ref
1344
ref
104
ref
1318
ref
constTerm
1496
def
1345
ref
1495
remove
1351
ref
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
1497
def
1449
ref
appTerm
1498
def
betaConv
nil
1319
ref
1497
ref
appTerm
1499
def
axiom
nil
125
ref
1499
remove
nil
cons
cons
126
ref
1498
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1321
ref
1322
ref
1497
remove
nil
cons
cons
1323
ref
1449
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
95
ref
1338
remove
1449
remove
appTerm
1500
def
1333
ref
appTerm
1501
def
appTerm
105
ref
1344
ref
1496
remove
1345
ref
1500
remove
1351
ref
appTerm
1502
def
absTerm
1503
def
appTerm
1504
def
absTerm
1505
def
appTerm
1506
def
appTerm
nil
cons
1507
def
cons
126
ref
74
ref
1467
remove
appTerm
1452
remove
appTerm
1508
def
nil
cons
1509
def
cons
nil
cons
1510
def
cons
nil
cons
cons
1511
def
184
ref
subst
proveHyp
1511
ref
143
ref
subst
1511
remove
192
ref
subst
nil
52
ref
1344
ref
74
ref
1505
ref
1349
ref
appTerm
1512
def
appTerm
1508
ref
appTerm
1513
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
66
ref
subst
1344
ref
nil
68
ref
1513
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
1512
ref
nil
cons
1514
def
cons
1510
ref
cons
nil
cons
cons
1515
def
143
ref
subst
1515
remove
192
ref
subst
1512
ref
betaConv
1512
remove
assume
eqMp
nil
125
ref
1504
ref
nil
cons
cons
1510
ref
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
1322
ref
1345
ref
74
ref
1503
ref
1350
ref
appTerm
1516
def
appTerm
1508
ref
appTerm
1517
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
1321
ref
43
ref
cons
66
ref
subst
subst
1345
ref
nil
68
ref
1517
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
1516
ref
nil
cons
1518
def
cons
1510
ref
cons
nil
cons
cons
1519
def
143
ref
subst
1519
remove
192
ref
subst
1516
ref
betaConv
1516
remove
assume
eqMp
nil
125
ref
1502
ref
nil
cons
1520
def
cons
1510
ref
cons
nil
cons
cons
1521
def
184
ref
subst
proveHyp
1521
ref
143
ref
subst
1521
remove
192
ref
subst
1005
ref
354
ref
refl
1522
def
1464
ref
refl
1523
def
1325
ref
1502
remove
assume
appThm
34
ref
refl
1524
def
appThm
1419
remove
trans
1525
def
appThm
nil
19
ref
1352
ref
nil
cons
cons
1398
remove
cons
nil
cons
cons
1526
def
19
ref
354
ref
1464
ref
247
ref
appTerm
appTerm
281
remove
appTerm
absTerm
1527
def
34
ref
appTerm
1528
def
betaConv
57
ref
18
ref
1527
ref
appTerm
1529
def
absTerm
1530
def
111
ref
appTerm
1531
def
betaConv
11
ref
132
ref
354
ref
1464
ref
99
ref
appTerm
1532
def
appTerm
357
ref
appTerm
1533
def
appTerm
132
ref
354
ref
1464
ref
102
ref
appTerm
1534
def
appTerm
357
ref
appTerm
1535
def
appTerm
51
ref
1530
ref
appTerm
1536
def
appTerm
1537
def
appTerm
absTerm
1538
def
32
ref
appTerm
1539
def
betaConv
132
ref
298
ref
11
ref
1533
ref
absTerm
1540
def
appTerm
1541
def
appTerm
refl
164
ref
302
ref
303
ref
11
ref
11
ref
1535
ref
absTerm
1542
def
32
ref
appTerm
betaConv
1543
def
absThm
appThm
appThm
303
ref
11
ref
11
ref
1536
ref
absTerm
1544
def
32
ref
appTerm
betaConv
1545
def
absThm
appThm
appThm
appThm
303
ref
11
ref
302
ref
1543
remove
appThm
1545
remove
appThm
absThm
appThm
appThm
nil
308
ref
1542
ref
nil
cons
cons
309
ref
1544
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
332
ref
subst
eqMp
appThm
164
ref
302
ref
303
ref
11
ref
1540
ref
32
ref
appTerm
betaConv
1546
def
absThm
appThm
appThm
303
ref
11
ref
11
ref
1537
ref
absTerm
1547
def
32
ref
appTerm
betaConv
1548
def
absThm
appThm
appThm
appThm
303
remove
11
ref
302
ref
1546
remove
appThm
1548
remove
appThm
absThm
appThm
appThm
nil
308
remove
1540
remove
nil
cons
cons
309
remove
1547
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
332
remove
subst
eqMp
trans
nil
1541
ref
axiom
nil
125
ref
1541
remove
nil
cons
cons
126
ref
132
ref
298
ref
1542
remove
appTerm
1549
def
appTerm
298
ref
1544
remove
appTerm
1550
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
192
ref
subst
proveHyp
nil
1549
ref
axiom
nil
125
ref
1549
remove
nil
cons
cons
126
ref
1550
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
192
ref
subst
proveHyp
nil
1550
remove
axiom
eqMp
eqMp
eqMp
nil
125
ref
298
ref
1538
ref
appTerm
nil
cons
cons
126
ref
1539
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
42
ref
10
ref
1538
remove
nil
cons
cons
340
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
1551
def
nil
161
ref
1533
remove
nil
cons
cons
162
ref
1537
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
1552
def
343
ref
subst
proveHyp
1553
def
nil
161
ref
1535
remove
nil
cons
cons
162
ref
1536
remove
nil
cons
1554
def
cons
nil
cons
cons
nil
cons
cons
1555
def
343
ref
subst
proveHyp
nil
125
ref
1554
remove
cons
126
ref
1531
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
1530
remove
nil
cons
cons
350
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1529
remove
nil
cons
cons
126
ref
1528
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
1527
remove
nil
cons
cons
187
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
1556
def
subst
trans
appThm
1466
ref
refl
1557
def
appThm
appThm
495
ref
1306
ref
1525
remove
appThm
1526
remove
351
remove
subst
trans
appThm
1451
ref
refl
1558
def
appThm
appThm
sym
nil
125
ref
354
ref
279
remove
1349
remove
appTerm
1352
remove
appTerm
1559
def
appTerm
1466
ref
appTerm
1560
def
nil
cons
1561
def
cons
126
ref
246
ref
275
ref
1559
remove
appTerm
appTerm
1451
ref
appTerm
nil
cons
1562
def
cons
nil
cons
cons
nil
cons
cons
1563
def
143
ref
subst
1563
remove
192
ref
subst
418
ref
1560
remove
assume
appThm
nil
420
ref
1465
remove
nil
cons
1564
def
cons
1565
def
425
ref
cons
nil
cons
cons
460
ref
subst
nil
75
ref
186
ref
cons
265
ref
1493
ref
cons
nil
cons
cons
nil
cons
cons
795
ref
subst
trans
trans
eqMp
nil
161
ref
1561
remove
cons
162
ref
1562
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
161
ref
1520
remove
cons
162
ref
1509
ref
cons
nil
cons
1566
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
161
ref
1518
remove
cons
1566
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
1319
ref
1323
ref
74
ref
1503
ref
1323
remove
varTerm
appTerm
appTerm
1508
ref
appTerm
absTerm
appTerm
nil
cons
cons
126
ref
74
ref
1504
remove
appTerm
1508
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1321
remove
1322
remove
1503
remove
nil
cons
cons
1566
ref
cons
nil
cons
cons
623
ref
subst
eqMp
eqMp
eqMp
nil
161
ref
1514
remove
cons
1566
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
51
ref
57
ref
74
ref
1505
ref
111
ref
appTerm
appTerm
1508
ref
appTerm
absTerm
appTerm
nil
cons
cons
126
ref
74
ref
1506
ref
appTerm
1508
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
1505
remove
nil
cons
cons
1566
ref
cons
nil
cons
cons
623
ref
subst
eqMp
nil
125
ref
1501
ref
nil
cons
1567
def
cons
1510
remove
cons
nil
cons
cons
1568
def
143
ref
subst
1568
remove
192
ref
subst
1005
ref
1522
ref
1523
remove
1325
ref
1501
remove
assume
appThm
1524
ref
appThm
1363
remove
trans
1569
def
appThm
appThm
1557
ref
appThm
appThm
495
ref
1306
remove
1569
remove
appThm
appThm
1558
remove
appThm
appThm
sym
19
ref
95
ref
354
ref
1464
ref
34
ref
appTerm
1570
def
appTerm
1571
def
357
ref
appTerm
1572
def
appTerm
358
ref
265
ref
106
ref
75
ref
132
ref
1571
ref
361
ref
appTerm
1573
def
appTerm
81
ref
appTerm
1574
def
absTerm
1575
def
appTerm
1576
def
absTerm
1577
def
appTerm
1578
def
appTerm
1579
def
absTerm
1580
def
34
ref
appTerm
1581
def
betaConv
11
ref
18
ref
1580
ref
appTerm
1582
def
absTerm
1583
def
32
ref
appTerm
1584
def
betaConv
nil
298
ref
1583
ref
appTerm
1585
def
axiom
nil
125
ref
1585
remove
nil
cons
cons
126
ref
1584
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
42
ref
10
ref
1583
remove
nil
cons
cons
340
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1582
remove
nil
cons
cons
126
ref
1581
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
1580
remove
nil
cons
cons
187
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1579
remove
nil
cons
1586
def
cons
126
ref
74
ref
1571
remove
1466
remove
appTerm
appTerm
246
ref
35
ref
appTerm
1587
def
1451
remove
appTerm
1588
def
appTerm
1589
def
nil
cons
1590
def
cons
nil
cons
1591
def
cons
nil
cons
cons
1592
def
184
ref
subst
proveHyp
1592
ref
143
ref
subst
1592
remove
192
ref
subst
nil
391
ref
265
ref
74
ref
1577
ref
268
ref
appTerm
1593
def
appTerm
1589
ref
appTerm
1594
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
398
ref
subst
265
ref
nil
68
ref
1594
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
1593
ref
nil
cons
1595
def
cons
1591
ref
cons
nil
cons
cons
1596
def
143
ref
subst
1596
remove
192
ref
subst
1593
ref
betaConv
1593
remove
assume
eqMp
nil
125
ref
1576
ref
nil
cons
cons
1591
ref
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
73
ref
75
ref
74
ref
1575
ref
79
ref
appTerm
1597
def
appTerm
1589
ref
appTerm
1598
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
75
ref
nil
68
ref
1598
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
1597
ref
nil
cons
1599
def
cons
1591
ref
cons
nil
cons
cons
1600
def
143
ref
subst
1600
remove
192
ref
subst
1597
ref
betaConv
1597
remove
assume
eqMp
nil
125
ref
1574
remove
nil
cons
1601
def
cons
1591
ref
cons
nil
cons
cons
1602
def
184
ref
subst
proveHyp
1602
ref
143
ref
subst
1602
remove
192
ref
subst
nil
161
ref
1573
ref
nil
cons
cons
162
ref
81
remove
nil
cons
1603
def
cons
nil
cons
cons
nil
cons
cons
1604
def
176
ref
subst
1604
remove
343
ref
subst
1005
ref
1522
ref
1573
ref
assume
appThm
1557
ref
appThm
nil
"b"
250
remove
var
1564
remove
cons
421
remove
nil
cons
cons
nil
cons
cons
426
remove
nil
cons
43
ref
cons
1605
def
"b"
2
ref
var
1606
def
48
ref
45
ref
0
ref
432
ref
0
ref
432
remove
8
ref
cons
opType
nil
cons
cons
opType
constTerm
1607
def
440
ref
appTerm
1608
def
438
remove
1606
remove
varTerm
1609
def
appTerm
appTerm
appTerm
507
ref
439
ref
appTerm
1610
def
1609
ref
appTerm
appTerm
absTerm
1611
def
1609
ref
appTerm
1612
def
betaConv
429
ref
51
ref
1611
ref
appTerm
1613
def
absTerm
1614
def
439
ref
appTerm
1615
def
betaConv
nil
51
ref
1614
ref
appTerm
1616
def
axiom
nil
125
ref
1616
remove
nil
cons
cons
126
ref
1615
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
1614
remove
nil
cons
cons
458
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1613
remove
nil
cons
cons
126
ref
1612
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
1611
remove
nil
cons
cons
57
ref
1609
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
subst
nil
"b'"
15
ref
var
186
remove
cons
"a'"
3
ref
var
1493
remove
cons
503
remove
cons
cons
nil
cons
cons
506
remove
"b'"
3
ref
var
1617
def
48
ref
45
ref
0
ref
508
ref
0
ref
508
ref
8
ref
cons
opType
1618
def
nil
cons
cons
opType
constTerm
1619
def
514
ref
appTerm
513
remove
"a'"
2
ref
var
1620
def
varTerm
1621
def
appTerm
1617
remove
varTerm
1622
def
appTerm
appTerm
appTerm
132
ref
1610
remove
1621
ref
appTerm
appTerm
430
ref
434
ref
appTerm
1622
ref
appTerm
appTerm
appTerm
absTerm
1623
def
1622
ref
appTerm
1624
def
betaConv
1620
remove
264
ref
1623
ref
appTerm
1625
def
absTerm
1626
def
1621
ref
appTerm
1627
def
betaConv
433
ref
51
ref
1626
ref
appTerm
1628
def
absTerm
1629
def
434
ref
appTerm
1630
def
betaConv
429
ref
264
ref
1629
ref
appTerm
1631
def
absTerm
1632
def
439
ref
appTerm
1633
def
betaConv
nil
51
ref
1632
ref
appTerm
1634
def
axiom
nil
125
ref
1634
remove
nil
cons
cons
126
ref
1633
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
1632
remove
nil
cons
cons
458
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1631
remove
nil
cons
cons
126
ref
1630
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
391
ref
1629
remove
nil
cons
cons
453
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1628
remove
nil
cons
cons
126
ref
1627
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
1626
remove
nil
cons
cons
57
ref
1621
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1625
remove
nil
cons
cons
126
ref
1624
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
391
ref
1623
remove
nil
cons
cons
452
ref
1622
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
1635
def
subst
subst
trans
trans
appThm
1588
ref
refl
1636
def
appThm
sym
nil
125
ref
132
ref
430
ref
268
ref
appTerm
919
ref
appTerm
1637
def
appTerm
96
ref
79
ref
appTerm
1638
def
34
ref
appTerm
1639
def
appTerm
nil
cons
1640
def
cons
126
ref
1588
remove
nil
cons
1641
def
cons
nil
cons
cons
nil
cons
cons
1642
def
143
ref
subst
1642
remove
192
ref
subst
nil
161
ref
1637
remove
nil
cons
cons
162
ref
1639
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
343
ref
subst
nil
125
ref
1603
ref
cons
126
ref
"Data.Bool.F"
const
7
ref
constTerm
1643
def
nil
cons
1644
def
cons
nil
cons
1645
def
cons
nil
cons
cons
184
ref
subst
nil
68
ref
1603
remove
cons
nil
cons
nil
cons
cons
68
ref
48
ref
764
remove
1643
ref
appTerm
appTerm
"Data.Bool.~"
const
46
remove
constTerm
1646
def
70
ref
appTerm
1647
def
appTerm
absTerm
1648
def
70
ref
appTerm
1649
def
betaConv
nil
572
ref
1648
ref
appTerm
1650
def
axiom
nil
125
ref
1650
remove
nil
cons
cons
126
ref
1649
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
583
ref
576
ref
1648
remove
nil
cons
cons
768
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
1646
ref
refl
1651
def
78
remove
refl
1639
remove
assume
appThm
1524
remove
appThm
19
ref
1646
ref
836
remove
34
ref
appTerm
1652
def
appTerm
1653
def
absTerm
1654
def
34
ref
appTerm
1655
def
betaConv
nil
18
ref
1654
ref
appTerm
1656
def
axiom
nil
125
ref
1656
remove
nil
cons
cons
126
ref
1655
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
1654
remove
nil
cons
cons
187
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1653
remove
nil
cons
cons
126
ref
48
ref
1652
ref
appTerm
1643
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
161
ref
1652
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
125
ref
1646
ref
165
ref
appTerm
1657
def
nil
cons
1658
def
cons
126
ref
48
ref
165
ref
appTerm
1643
ref
appTerm
nil
cons
1659
def
cons
nil
cons
cons
nil
cons
cons
1660
def
143
ref
subst
1660
remove
192
ref
subst
nil
125
ref
165
ref
nil
cons
1661
def
cons
1645
remove
cons
nil
cons
cons
660
remove
subst
48
ref
1657
ref
appTerm
refl
125
ref
128
remove
1643
ref
appTerm
absTerm
1662
def
165
ref
appTerm
betaConv
appThm
nil
151
remove
1646
ref
appTerm
1662
remove
appTerm
axiom
174
remove
appThm
eqMp
1657
remove
assume
eqMp
nil
125
ref
952
remove
1643
ref
appTerm
nil
cons
cons
126
ref
74
ref
1643
ref
appTerm
1663
def
165
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
192
ref
subst
proveHyp
nil
125
ref
1644
ref
cons
126
ref
1661
ref
cons
nil
cons
cons
nil
cons
cons
1664
def
143
ref
subst
1664
remove
192
ref
subst
125
ref
127
remove
absTerm
1665
def
165
remove
appTerm
1666
def
betaConv
nil
48
ref
1643
ref
appTerm
1667
def
572
ref
1665
ref
appTerm
1668
def
appTerm
axiom
1643
ref
assume
eqMp
nil
125
ref
1668
remove
nil
cons
cons
126
ref
1666
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
583
ref
576
ref
1665
remove
nil
cons
cons
622
ref
1661
ref
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
1669
def
eqMp
nil
161
ref
1644
ref
cons
162
ref
1661
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
161
ref
1658
remove
cons
162
ref
1659
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
1670
def
subst
eqMp
trans
appThm
nil
48
ref
1646
ref
1643
ref
appTerm
appTerm
58
ref
appTerm
axiom
trans
trans
sym
71
ref
eqMp
eqMp
nil
161
ref
1641
ref
cons
nil
cons
nil
cons
cons
1669
remove
subst
proveHyp
proveHyp
eqMp
nil
161
ref
1640
remove
cons
162
ref
1641
ref
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
proveHyp
proveHyp
eqMp
nil
161
ref
1601
remove
cons
162
ref
1590
ref
cons
nil
cons
1671
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
161
ref
1599
remove
cons
1671
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
18
ref
185
ref
74
ref
1575
ref
914
ref
appTerm
appTerm
1589
ref
appTerm
absTerm
appTerm
nil
cons
cons
126
ref
74
ref
1576
remove
appTerm
1589
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
1575
remove
nil
cons
cons
1671
ref
cons
nil
cons
cons
623
ref
subst
eqMp
eqMp
eqMp
nil
161
ref
1595
remove
cons
1671
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
264
ref
"x'"
3
ref
var
1672
def
74
ref
1577
ref
1672
remove
varTerm
appTerm
appTerm
1589
ref
appTerm
absTerm
appTerm
nil
cons
cons
126
ref
74
ref
1578
ref
appTerm
1589
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
391
ref
1577
remove
nil
cons
cons
1671
ref
cons
nil
cons
cons
623
ref
subst
eqMp
nil
125
ref
1572
ref
nil
cons
1673
def
cons
1591
remove
cons
nil
cons
cons
1674
def
143
ref
subst
1674
remove
192
ref
subst
1005
ref
1522
ref
1572
remove
assume
appThm
1557
remove
appThm
nil
1565
remove
nil
cons
nil
cons
cons
1605
remove
1651
remove
1607
remove
927
ref
appTerm
440
remove
appTerm
1675
def
assume
sym
1608
remove
927
remove
appTerm
1676
def
assume
sym
deductAntisym
appThm
429
ref
1646
ref
1676
remove
appTerm
absTerm
1677
def
439
ref
appTerm
1678
def
betaConv
nil
51
ref
1677
ref
appTerm
1679
def
axiom
nil
125
ref
1679
remove
nil
cons
cons
126
ref
1678
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
1677
remove
nil
cons
cons
458
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
eqMp
nil
125
ref
1646
ref
1675
ref
appTerm
nil
cons
cons
126
ref
48
ref
1675
ref
appTerm
1643
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
161
ref
1675
remove
nil
cons
cons
nil
cons
nil
cons
cons
1670
ref
subst
eqMp
subst
subst
trans
appThm
1636
remove
appThm
nil
68
ref
1641
remove
cons
nil
cons
nil
cons
cons
68
ref
48
ref
1663
remove
70
ref
appTerm
appTerm
58
ref
appTerm
absTerm
1680
def
70
ref
appTerm
1681
def
betaConv
nil
572
ref
1680
ref
appTerm
1682
def
axiom
nil
125
ref
1682
remove
nil
cons
cons
126
ref
1681
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
583
ref
576
ref
1680
remove
nil
cons
cons
768
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
trans
sym
71
ref
eqMp
eqMp
nil
161
ref
1673
remove
cons
1683
def
1671
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
1683
remove
162
ref
1578
remove
nil
cons
cons
947
ref
1590
remove
cons
nil
cons
cons
cons
nil
cons
cons
962
ref
subst
proveHyp
proveHyp
eqMp
nil
161
ref
1586
remove
cons
1671
remove
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
161
ref
1567
remove
cons
1684
def
1566
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
1684
remove
162
ref
1506
remove
nil
cons
cons
947
ref
1509
remove
cons
nil
cons
cons
cons
nil
cons
cons
962
ref
subst
proveHyp
proveHyp
eqMp
nil
161
ref
1507
remove
cons
1566
remove
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
161
ref
1486
remove
cons
162
ref
1488
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
1685
def
nil
125
ref
298
ref
11
ref
1263
ref
1264
ref
264
ref
452
ref
1455
ref
absTerm
1686
def
appTerm
1687
def
absTerm
1688
def
appTerm
1689
def
absTerm
1690
def
appTerm
1691
def
nil
cons
1692
def
cons
1693
def
126
ref
1263
ref
1462
ref
appTerm
nil
cons
1694
def
cons
nil
cons
cons
nil
cons
cons
1695
def
184
ref
subst
proveHyp
1695
ref
143
ref
subst
1695
remove
192
ref
subst
nil
1291
ref
1462
remove
nil
cons
cons
1696
def
nil
cons
nil
cons
cons
1293
ref
subst
1264
ref
nil
68
ref
1461
remove
nil
cons
1697
def
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
391
ref
1459
remove
nil
cons
cons
1698
def
nil
cons
nil
cons
cons
398
ref
subst
452
ref
nil
68
ref
1458
remove
nil
cons
1699
def
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
10
ref
1456
remove
nil
cons
cons
1700
def
nil
cons
nil
cons
cons
67
ref
subst
11
ref
nil
68
ref
1455
remove
nil
cons
1701
def
cons
nil
cons
nil
cons
cons
72
ref
subst
1686
ref
919
remove
appTerm
1702
def
betaConv
1688
ref
1272
ref
appTerm
1703
def
betaConv
1690
ref
32
ref
appTerm
1704
def
betaConv
nil
1693
remove
126
ref
1704
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
42
ref
10
ref
1690
remove
nil
cons
cons
340
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1689
remove
nil
cons
cons
126
ref
1703
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1292
ref
1291
ref
1688
remove
nil
cons
cons
1478
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1687
remove
nil
cons
cons
126
ref
1702
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
391
ref
1686
remove
nil
cons
cons
1494
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
161
ref
1692
remove
cons
162
ref
1694
ref
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
nil
125
ref
1694
remove
cons
126
ref
1463
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1292
ref
1696
remove
1478
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1697
remove
cons
126
ref
1460
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
1698
remove
1494
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1699
remove
cons
126
ref
1457
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
42
ref
1700
remove
340
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1701
remove
cons
126
ref
1454
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
1453
remove
nil
cons
cons
187
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
eqMp
eqMp
nil
161
ref
1424
remove
cons
162
ref
1427
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
125
ref
132
ref
1373
remove
appTerm
1387
remove
appTerm
nil
cons
cons
126
ref
1269
ref
1303
ref
appTerm
nil
cons
1705
def
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1005
ref
302
remove
1303
ref
1309
ref
appTerm
betaConv
appThm
526
remove
1374
ref
1269
ref
refl
1706
def
1375
ref
1005
ref
1303
ref
1376
remove
appTerm
betaConv
appThm
1303
ref
1381
remove
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
1706
ref
1270
ref
1305
remove
absThm
appThm
appThm
nil
"p"
1267
remove
var
1303
remove
nil
cons
1707
def
cons
nil
cons
nil
cons
cons
397
ref
"p"
1317
ref
var
1708
def
74
ref
132
ref
1708
remove
varTerm
1709
def
1333
ref
appTerm
appTerm
51
ref
1344
remove
1319
ref
1345
remove
74
ref
1709
ref
1350
remove
appTerm
appTerm
1709
ref
1351
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
1319
ref
1307
ref
1709
ref
1311
ref
appTerm
absTerm
appTerm
appTerm
absTerm
1710
def
1709
ref
appTerm
1711
def
betaConv
nil
12
ref
0
ref
1318
ref
8
ref
cons
opType
constTerm
1710
ref
appTerm
1712
def
axiom
nil
125
ref
1712
remove
nil
cons
cons
126
ref
1711
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
"A"
1337
remove
cons
nil
cons
"P"
1318
remove
var
1710
remove
nil
cons
cons
"x"
1317
remove
var
1709
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
subst
eqMp
eqMp
nil
125
ref
1705
remove
cons
126
ref
1304
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1297
ref
1294
ref
1707
remove
cons
"x"
1265
ref
var
1713
def
1282
ref
nil
cons
1714
def
cons
nil
cons
1715
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
eqMp
nil
161
ref
1299
remove
cons
1716
def
162
ref
1301
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
298
ref
1290
remove
appTerm
thm
1685
remove
nil
1691
remove
thm
nil
10
ref
11
ref
1263
ref
1264
ref
18
ref
19
ref
1269
ref
"ys"
1265
ref
var
1717
def
572
ref
"ye"
7
ref
var
1718
def
74
ref
132
ref
"Parser.strongInverse"
const
1271
remove
constTerm
32
ref
appTerm
1272
ref
appTerm
1719
def
appTerm
45
ref
0
ref
249
ref
1266
remove
opType
1720
def
0
ref
1720
ref
8
ref
cons
opType
1721
def
nil
cons
1722
def
cons
opType
constTerm
1723
def
"Parser.Stream.toList"
const
1724
def
0
ref
25
ref
1720
ref
nil
cons
1725
def
cons
opType
constTerm
1726
def
35
remove
appTerm
appTerm
266
ref
0
ref
1265
ref
0
ref
7
ref
1725
ref
cons
opType
1727
def
nil
cons
cons
opType
constTerm
1728
def
1717
ref
varTerm
1729
def
appTerm
1730
def
1718
ref
varTerm
1731
def
appTerm
1732
def
appTerm
1733
def
appTerm
1734
def
appTerm
95
ref
1731
ref
appTerm
1735
def
97
ref
1276
ref
1278
ref
1281
ref
1729
ref
appTerm
appTerm
appTerm
1736
def
appTerm
appTerm
1737
def
appTerm
1738
def
absTerm
1739
def
appTerm
1740
def
absTerm
1741
def
appTerm
1742
def
absTerm
1743
def
appTerm
1744
def
absTerm
1745
def
appTerm
1746
def
absTerm
1747
def
nil
cons
cons
nil
cons
nil
cons
cons
67
ref
subst
11
ref
nil
68
ref
1746
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
1291
ref
1745
remove
nil
cons
cons
nil
cons
nil
cons
cons
1293
remove
subst
1264
ref
nil
68
ref
1744
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
73
ref
1743
remove
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
19
ref
nil
68
ref
1742
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
1294
ref
1741
remove
nil
cons
cons
nil
cons
nil
cons
cons
1298
ref
subst
1717
ref
nil
68
ref
1740
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
576
ref
1739
remove
nil
cons
cons
nil
cons
nil
cons
cons
584
ref
subst
1718
remove
nil
68
ref
1738
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
1734
remove
nil
cons
1748
def
cons
126
ref
1737
ref
nil
cons
1749
def
cons
nil
cons
1750
def
cons
nil
cons
cons
1751
def
143
ref
subst
1751
remove
192
ref
subst
nil
161
ref
1719
ref
nil
cons
cons
162
ref
1733
ref
nil
cons
1752
def
cons
nil
cons
cons
nil
cons
cons
1753
def
176
ref
subst
1753
remove
343
ref
subst
nil
125
ref
1752
remove
cons
1750
remove
cons
nil
cons
cons
184
ref
subst
1717
ref
74
ref
1733
remove
appTerm
1737
remove
appTerm
1754
def
absTerm
1755
def
1729
ref
appTerm
1756
def
betaConv
19
ref
1269
ref
1755
ref
appTerm
1757
def
absTerm
1758
def
34
ref
appTerm
1759
def
betaConv
1760
def
nil
73
ref
19
ref
74
ref
18
ref
75
ref
82
remove
1269
ref
1717
ref
74
ref
1723
ref
1726
ref
83
remove
appTerm
appTerm
1761
def
1732
ref
appTerm
appTerm
1735
ref
1638
remove
1736
ref
appTerm
1762
def
appTerm
appTerm
absTerm
appTerm
1763
def
appTerm
absTerm
appTerm
1764
def
appTerm
1757
ref
appTerm
1765
def
absTerm
1766
def
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
19
ref
nil
68
ref
1765
ref
nil
cons
1767
def
cons
nil
cons
nil
cons
cons
72
ref
subst
195
ref
nil
197
ref
126
ref
1767
ref
cons
nil
cons
1768
def
cons
nil
cons
cons
1769
def
184
ref
subst
proveHyp
1769
ref
143
ref
subst
1769
remove
192
ref
subst
nil
201
ref
1768
ref
cons
nil
cons
cons
1770
def
143
ref
subst
1770
remove
192
ref
subst
nil
52
ref
57
ref
204
ref
1765
ref
appTerm
1771
def
absTerm
1772
def
nil
cons
cons
nil
cons
nil
cons
cons
66
ref
subst
57
ref
nil
68
ref
1771
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
208
ref
1768
ref
cons
nil
cons
cons
1773
def
143
ref
subst
1773
remove
192
ref
subst
210
ref
nil
211
ref
1768
ref
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
73
ref
107
ref
213
ref
1765
ref
appTerm
1774
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
107
ref
nil
68
ref
1774
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
216
ref
1768
ref
cons
nil
cons
cons
1775
def
143
ref
subst
1775
remove
192
ref
subst
218
ref
nil
220
ref
1768
ref
cons
nil
cons
cons
1776
def
184
ref
subst
proveHyp
1776
ref
143
ref
subst
1776
remove
192
ref
subst
48
ref
"_32398"
15
ref
var
1777
def
74
ref
18
ref
75
ref
74
ref
80
remove
1777
remove
varTerm
1778
def
appTerm
appTerm
1763
ref
appTerm
absTerm
appTerm
appTerm
1269
ref
1717
ref
74
ref
1723
ref
1726
ref
33
ref
1778
ref
appTerm
appTerm
appTerm
1732
ref
appTerm
appTerm
1735
ref
96
ref
1778
remove
appTerm
1736
ref
appTerm
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
1779
def
34
ref
appTerm
1780
def
appTerm
refl
1779
remove
114
ref
appTerm
betaConv
appThm
164
ref
1780
remove
betaConv
appThm
74
ref
18
ref
75
ref
229
remove
1763
ref
appTerm
absTerm
appTerm
appTerm
1269
ref
1717
ref
74
ref
1723
ref
1726
ref
232
ref
appTerm
appTerm
1732
ref
appTerm
appTerm
1735
ref
96
ref
114
ref
appTerm
1781
def
1736
ref
appTerm
appTerm
1782
def
appTerm
absTerm
appTerm
appTerm
refl
appThm
trans
1766
ref
refl
236
ref
appThm
eqMp
sym
1005
ref
1006
ref
75
ref
1005
ref
848
remove
appThm
1763
ref
refl
appThm
absThm
appThm
appThm
1706
ref
1717
ref
1005
ref
1723
ref
refl
1783
def
1726
ref
refl
1784
def
352
ref
appThm
appThm
1732
ref
refl
1785
def
appThm
appThm
1782
ref
refl
1786
def
appThm
absThm
appThm
appThm
sym
nil
125
ref
18
ref
75
ref
74
ref
378
ref
appTerm
1787
def
1763
remove
appTerm
absTerm
appTerm
1788
def
nil
cons
1789
def
cons
126
ref
1269
ref
1717
ref
74
ref
1723
ref
1726
ref
386
ref
appTerm
appTerm
1732
ref
appTerm
appTerm
1782
ref
appTerm
1790
def
absTerm
1791
def
appTerm
nil
cons
1792
def
cons
nil
cons
cons
nil
cons
cons
1793
def
143
ref
subst
1793
remove
192
ref
subst
nil
1294
ref
1791
remove
nil
cons
cons
nil
cons
nil
cons
cons
1298
ref
subst
1717
ref
nil
68
ref
1790
ref
nil
cons
1794
def
cons
nil
cons
nil
cons
cons
72
ref
subst
373
remove
nil
385
remove
126
ref
1794
ref
cons
nil
cons
1795
def
cons
nil
cons
cons
1796
def
184
ref
subst
proveHyp
1796
ref
143
ref
subst
1796
remove
192
ref
subst
nil
391
ref
"z"
3
ref
var
1797
def
74
ref
382
remove
1797
ref
varTerm
1798
def
appTerm
1799
def
appTerm
1790
ref
appTerm
1800
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
398
remove
subst
1797
remove
nil
68
ref
1800
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
1799
ref
nil
cons
1801
def
cons
1795
ref
cons
nil
cons
cons
1802
def
143
ref
subst
1802
remove
192
ref
subst
1799
ref
betaConv
1799
remove
assume
eqMp
nil
125
ref
106
remove
75
ref
132
ref
375
ref
360
ref
267
remove
1798
ref
appTerm
1803
def
79
ref
appTerm
appTerm
1804
def
appTerm
appTerm
378
remove
appTerm
absTerm
1805
def
appTerm
1806
def
nil
cons
cons
1795
ref
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
73
ref
1429
ref
74
ref
1805
ref
1435
ref
appTerm
1807
def
appTerm
1790
ref
appTerm
1808
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
1429
remove
nil
68
ref
1808
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
1807
ref
nil
cons
1809
def
cons
1795
ref
cons
nil
cons
cons
1810
def
143
ref
subst
1810
remove
192
ref
subst
1807
ref
betaConv
1807
remove
assume
eqMp
nil
125
ref
132
ref
375
remove
360
ref
1803
ref
1435
ref
appTerm
1811
def
appTerm
1812
def
appTerm
1813
def
appTerm
362
remove
1435
ref
appTerm
113
ref
appTerm
1814
def
appTerm
nil
cons
1815
def
cons
1795
ref
cons
nil
cons
cons
1816
def
184
ref
subst
proveHyp
1816
ref
143
ref
subst
1816
remove
192
ref
subst
nil
161
ref
1813
ref
nil
cons
cons
162
ref
1814
ref
nil
cons
1817
def
cons
nil
cons
cons
nil
cons
cons
1818
def
176
ref
subst
1818
remove
343
ref
subst
1005
ref
1783
ref
1784
ref
418
remove
1813
remove
assume
1819
def
appThm
nil
420
remove
1811
remove
nil
cons
cons
425
remove
cons
nil
cons
cons
460
remove
subst
nil
75
ref
1445
remove
cons
265
ref
1798
ref
nil
cons
1820
def
cons
nil
cons
cons
nil
cons
cons
795
remove
subst
trans
trans
appThm
nil
797
remove
33
ref
1435
ref
appTerm
1821
def
nil
cons
cons
452
ref
1820
ref
cons
nil
cons
1822
def
cons
nil
cons
cons
397
ref
19
ref
45
ref
0
ref
249
remove
1316
remove
opType
1823
def
0
ref
1823
ref
8
ref
cons
opType
nil
cons
cons
opType
constTerm
1824
def
1724
remove
0
ref
15
ref
1823
ref
nil
cons
1825
def
cons
opType
constTerm
1826
def
247
ref
appTerm
appTerm
257
ref
0
ref
0
ref
0
ref
1823
remove
1825
ref
cons
opType
1827
def
8
ref
cons
opType
1827
ref
nil
cons
cons
opType
constTerm
"f"
1827
remove
var
1828
def
572
ref
"e"
7
ref
var
1829
def
1319
remove
1307
ref
1824
ref
1828
remove
varTerm
266
remove
0
ref
1259
remove
0
ref
7
ref
1825
remove
cons
opType
nil
cons
cons
opType
constTerm
1830
def
1311
ref
appTerm
1829
ref
varTerm
1831
def
appTerm
appTerm
appTerm
1830
ref
1348
remove
111
ref
appTerm
1311
remove
appTerm
appTerm
1831
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
1826
ref
34
ref
appTerm
appTerm
appTerm
absTerm
1832
def
34
ref
appTerm
1833
def
betaConv
57
ref
18
ref
1832
ref
appTerm
1834
def
absTerm
1835
def
111
ref
appTerm
1836
def
betaConv
nil
132
ref
1824
ref
1826
ref
99
ref
appTerm
appTerm
1830
remove
1333
remove
appTerm
1837
def
58
ref
appTerm
appTerm
1838
def
appTerm
132
ref
1824
remove
1826
remove
102
ref
appTerm
appTerm
1837
remove
1643
ref
appTerm
appTerm
1839
def
appTerm
51
ref
1835
ref
appTerm
1840
def
appTerm
1841
def
appTerm
axiom
1842
def
nil
161
ref
1838
remove
nil
cons
cons
162
ref
1841
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
1843
def
343
ref
subst
proveHyp
1844
def
nil
161
ref
1839
remove
nil
cons
cons
162
ref
1840
remove
nil
cons
1845
def
cons
nil
cons
cons
nil
cons
cons
1846
def
343
ref
subst
proveHyp
nil
125
ref
1845
remove
cons
126
ref
1836
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
ref
1835
remove
nil
cons
cons
350
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1834
remove
nil
cons
cons
126
ref
1833
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
1832
remove
nil
cons
cons
187
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
subst
trans
appThm
1785
ref
appThm
appThm
1786
ref
appThm
sym
"x"
1720
ref
var
1847
def
104
ref
1268
remove
constTerm
1848
def
"a"
1265
ref
var
1849
def
104
ref
150
remove
constTerm
1850
def
"b"
7
ref
var
1851
def
1723
ref
1847
ref
varTerm
appTerm
1728
ref
1849
ref
varTerm
1852
def
appTerm
1851
ref
varTerm
1853
def
appTerm
1854
def
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
1855
def
1726
ref
1821
remove
appTerm
1856
def
appTerm
1857
def
betaConv
1296
remove
634
remove
cons
43
ref
cons
1858
def
nil
12
ref
0
ref
1618
remove
8
ref
cons
opType
constTerm
"x"
508
remove
var
1859
def
105
remove
429
remove
358
remove
433
ref
1619
remove
1859
remove
varTerm
appTerm
514
remove
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
axiom
subst
nil
125
ref
12
ref
0
ref
1721
ref
8
ref
cons
opType
1860
def
constTerm
1855
ref
appTerm
nil
cons
cons
126
ref
1857
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
"A"
1725
ref
cons
nil
cons
1861
def
"P"
1721
ref
var
1855
remove
nil
cons
cons
1847
ref
1856
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1848
remove
1849
ref
1850
ref
1851
ref
1723
ref
1856
ref
appTerm
1862
def
1854
ref
appTerm
absTerm
appTerm
absTerm
1863
def
appTerm
1864
def
nil
cons
cons
126
ref
74
ref
1723
ref
257
ref
0
ref
0
ref
0
ref
1720
ref
1725
remove
cons
opType
1865
def
8
ref
cons
opType
1866
def
1865
ref
nil
cons
1867
def
cons
opType
constTerm
1868
def
"f"
1865
ref
var
1869
def
572
ref
1829
ref
1269
ref
1270
ref
1723
ref
1869
remove
varTerm
1728
ref
1282
ref
appTerm
1831
ref
appTerm
1870
def
appTerm
appTerm
1728
ref
1379
remove
1798
ref
appTerm
1871
def
1282
ref
appTerm
appTerm
1872
def
1831
ref
appTerm
1873
def
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
1856
remove
appTerm
appTerm
1732
ref
appTerm
appTerm
1782
ref
appTerm
1874
def
nil
cons
1875
def
cons
nil
cons
1876
def
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
1294
ref
"ws"
1265
ref
var
1877
def
74
ref
1863
ref
1877
ref
varTerm
1878
def
appTerm
1879
def
appTerm
1874
ref
appTerm
1880
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
1298
ref
subst
1877
remove
nil
68
ref
1880
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
1879
ref
nil
cons
1881
def
cons
1876
ref
cons
nil
cons
cons
1882
def
143
ref
subst
1882
remove
192
ref
subst
1879
ref
betaConv
1879
remove
assume
eqMp
nil
125
ref
1850
remove
1851
ref
1862
ref
1728
ref
1878
ref
appTerm
1883
def
1853
ref
appTerm
appTerm
absTerm
1884
def
appTerm
1885
def
nil
cons
cons
1876
ref
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
576
ref
"we"
7
ref
var
1886
def
74
ref
1884
ref
1886
ref
varTerm
1887
def
appTerm
1888
def
appTerm
1874
ref
appTerm
1889
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
584
ref
subst
1886
remove
nil
68
ref
1889
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
125
ref
1888
ref
nil
cons
1890
def
cons
1876
ref
cons
nil
cons
cons
1891
def
143
ref
subst
1891
remove
192
ref
subst
1888
ref
betaConv
1888
remove
assume
eqMp
nil
125
ref
1862
ref
1883
remove
1887
ref
appTerm
1892
def
appTerm
1893
def
nil
cons
1894
def
cons
1876
remove
cons
nil
cons
cons
1895
def
184
ref
subst
proveHyp
1895
ref
143
ref
subst
1895
remove
192
ref
subst
1005
ref
1783
ref
1868
ref
refl
"_32438"
1865
ref
var
1896
def
572
ref
refl
1829
ref
1706
ref
1270
ref
nil
"b"
1720
ref
var
1873
ref
nil
cons
cons
"a"
1720
ref
var
1896
ref
varTerm
1870
ref
appTerm
1897
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
1861
remove
43
ref
cons
1898
def
507
remove
refl
439
remove
refl
appThm
1609
remove
refl
appThm
subst
subst
absThm
appThm
absThm
appThm
absThm
appThm
1893
remove
assume
1899
def
appThm
nil
1829
ref
1887
ref
nil
cons
1900
def
cons
1270
ref
1878
ref
nil
cons
1901
def
cons
nil
cons
cons
nil
cons
cons
1270
ref
1723
ref
1868
remove
1896
remove
572
ref
1829
ref
1269
ref
1270
ref
1723
ref
1897
remove
appTerm
1873
ref
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
1902
def
appTerm
1903
def
1870
ref
appTerm
appTerm
1873
ref
appTerm
absTerm
1904
def
1282
ref
appTerm
1905
def
betaConv
1829
ref
1269
ref
1904
ref
appTerm
1906
def
absTerm
1907
def
1831
ref
appTerm
1908
def
betaConv
1902
ref
1903
remove
appTerm
1909
def
betaConv
1902
ref
"_32436"
1720
ref
var
1910
def
1728
ref
1871
ref
257
ref
0
ref
0
ref
0
ref
1720
remove
1295
remove
cons
opType
1911
def
8
ref
cons
opType
1911
ref
nil
cons
cons
opType
constTerm
"fn"
1911
remove
var
1912
def
1269
ref
1849
ref
572
ref
1851
ref
1331
ref
1912
remove
varTerm
1854
ref
appTerm
appTerm
1852
remove
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
1913
def
1910
remove
varTerm
1914
def
appTerm
appTerm
appTerm
257
remove
0
ref
1860
remove
1722
remove
cons
opType
constTerm
"fn"
1721
remove
var
1915
def
1269
ref
1849
ref
572
ref
1851
ref
48
ref
1915
remove
varTerm
1854
remove
appTerm
appTerm
1853
remove
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
1916
def
1914
remove
appTerm
appTerm
absTerm
1917
def
appTerm
betaConv
sym
nil
576
ref
1829
ref
1269
ref
1270
ref
1723
ref
1917
ref
1870
ref
appTerm
1918
def
appTerm
1873
remove
appTerm
1919
def
absTerm
1920
def
appTerm
1921
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
584
remove
subst
1829
remove
nil
68
ref
1921
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
1294
ref
1920
remove
nil
cons
cons
nil
cons
nil
cons
cons
1298
ref
subst
1270
remove
nil
68
ref
1919
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
1918
remove
betaConv
1723
ref
"_32433"
7
ref
var
1922
def
1872
remove
1922
ref
varTerm
1923
def
appTerm
absTerm
1831
ref
appTerm
1924
def
appTerm
refl
1922
ref
1728
ref
1871
ref
1913
remove
1870
ref
appTerm
1925
def
appTerm
appTerm
1926
def
1923
ref
appTerm
absTerm
1927
def
1916
remove
1870
remove
appTerm
1928
def
appTerm
betaConv
appThm
1783
ref
1924
remove
betaConv
appThm
1926
remove
1928
remove
appTerm
refl
appThm
trans
45
remove
0
ref
1727
ref
0
ref
1727
remove
8
ref
cons
opType
nil
cons
cons
opType
constTerm
1929
def
"_32432"
1265
ref
var
1930
def
1922
remove
1728
remove
1871
ref
1930
remove
varTerm
appTerm
appTerm
1923
remove
appTerm
absTerm
absTerm
1931
def
1282
remove
appTerm
1932
def
appTerm
refl
1931
ref
1925
remove
appTerm
betaConv
appThm
1929
remove
refl
1932
remove
betaConv
appThm
1927
remove
refl
appThm
trans
1931
remove
refl
nil
1851
ref
1831
remove
nil
cons
1933
def
cons
1849
ref
1714
remove
cons
nil
cons
cons
nil
cons
cons
1934
def
1858
ref
771
remove
subst
subst
appThm
eqMp
1934
remove
1858
ref
789
remove
subst
subst
appThm
eqMp
sym
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
"A"
1867
remove
cons
nil
cons
1935
def
"P"
1866
ref
var
1902
ref
nil
cons
1936
def
cons
"x"
1865
remove
var
1917
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
597
remove
subst
proveHyp
nil
125
ref
104
remove
0
ref
1866
ref
8
ref
cons
opType
constTerm
1902
remove
appTerm
nil
cons
cons
126
ref
1909
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
"p"
1866
remove
var
1936
remove
cons
nil
cons
nil
cons
cons
1935
remove
43
ref
cons
770
remove
subst
subst
eqMp
eqMp
nil
125
ref
572
ref
1907
ref
appTerm
nil
cons
cons
126
ref
1908
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
583
ref
576
ref
1907
remove
nil
cons
cons
622
ref
1933
remove
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
1906
remove
nil
cons
cons
126
ref
1905
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1297
ref
1294
ref
1904
remove
nil
cons
cons
1715
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
trans
appThm
1785
ref
appThm
nil
"b'"
7
ref
var
1731
ref
nil
cons
1937
def
cons
1938
def
"a'"
1265
ref
var
1729
ref
nil
cons
1939
def
cons
1940
def
1851
ref
1900
ref
cons
1849
ref
1871
remove
1878
ref
appTerm
1941
def
nil
cons
cons
nil
cons
cons
cons
cons
nil
cons
cons
1858
remove
1635
remove
subst
1942
def
subst
trans
appThm
1786
ref
appThm
sym
nil
125
ref
132
ref
1331
ref
1941
ref
appTerm
1729
ref
appTerm
1943
def
appTerm
48
ref
1887
ref
appTerm
1944
def
1731
ref
appTerm
1945
def
appTerm
nil
cons
1946
def
cons
126
ref
1782
ref
nil
cons
1947
def
cons
nil
cons
1948
def
cons
nil
cons
cons
1949
def
143
ref
subst
1949
remove
192
ref
subst
nil
161
ref
1943
ref
nil
cons
cons
162
ref
1945
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
1950
def
176
ref
subst
1950
remove
343
ref
subst
48
ref
"_32440"
1265
ref
var
1951
def
1735
ref
1781
ref
1276
ref
1278
ref
1281
ref
1951
remove
varTerm
appTerm
appTerm
appTerm
appTerm
appTerm
absTerm
1952
def
1729
ref
appTerm
1953
def
appTerm
refl
1954
def
1952
ref
1941
ref
appTerm
betaConv
appThm
164
ref
1953
remove
betaConv
appThm
1955
def
1735
ref
1781
ref
1276
ref
1278
ref
1281
ref
1941
remove
appTerm
appTerm
1956
def
appTerm
1957
def
appTerm
1958
def
appTerm
refl
appThm
trans
1952
remove
refl
1959
def
1943
remove
assume
sym
appThm
eqMp
sym
48
ref
"_32452"
7
ref
var
1960
def
95
ref
1960
remove
varTerm
appTerm
1958
ref
appTerm
absTerm
1961
def
1731
ref
appTerm
1962
def
appTerm
refl
1961
ref
1887
ref
appTerm
betaConv
appThm
164
ref
1962
remove
betaConv
appThm
95
ref
1887
ref
appTerm
1963
def
1958
ref
appTerm
1964
def
refl
1965
def
appThm
trans
1961
remove
refl
1945
remove
assume
sym
1966
def
appThm
eqMp
sym
75
ref
1787
ref
1269
ref
1717
ref
74
ref
1761
ref
1730
ref
1887
ref
appTerm
1967
def
appTerm
appTerm
1963
ref
1762
ref
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
1968
def
1435
ref
appTerm
1969
def
betaConv
48
ref
"_32456"
7
ref
var
1970
def
18
ref
75
ref
1787
remove
1269
ref
1717
ref
74
ref
1761
remove
1730
remove
1970
remove
varTerm
1971
def
appTerm
appTerm
appTerm
95
ref
1971
remove
appTerm
1762
remove
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
1972
def
1731
ref
appTerm
1973
def
appTerm
refl
1972
ref
1887
ref
appTerm
betaConv
appThm
164
ref
1973
remove
betaConv
appThm
18
ref
1968
ref
appTerm
1974
def
refl
appThm
trans
1972
remove
refl
1966
remove
appThm
eqMp
1788
remove
assume
eqMp
nil
125
ref
1974
remove
nil
cons
cons
126
ref
1969
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
1968
remove
nil
cons
cons
1446
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
74
ref
1814
ref
appTerm
1269
ref
1717
ref
74
ref
1862
remove
1967
ref
appTerm
appTerm
1963
ref
96
ref
1435
ref
appTerm
1975
def
1736
ref
appTerm
appTerm
1976
def
appTerm
absTerm
appTerm
appTerm
nil
cons
cons
126
ref
1964
ref
nil
cons
1977
def
cons
nil
cons
1978
def
cons
nil
cons
cons
184
ref
subst
proveHyp
1005
ref
1005
ref
nil
68
ref
1817
remove
cons
nil
cons
nil
cons
cons
72
ref
subst
1814
remove
assume
eqMp
appThm
1706
remove
1717
ref
1005
ref
1783
ref
1899
remove
appThm
1967
ref
refl
appThm
appThm
1976
ref
refl
appThm
absThm
appThm
appThm
nil
68
ref
1269
ref
1717
ref
74
ref
1723
ref
1892
ref
appTerm
1979
def
1967
remove
appTerm
appTerm
1976
remove
appTerm
absTerm
1980
def
appTerm
nil
cons
1981
def
cons
nil
cons
nil
cons
cons
68
ref
48
ref
74
ref
58
ref
appTerm
70
ref
appTerm
appTerm
70
ref
appTerm
absTerm
1982
def
70
ref
appTerm
1983
def
betaConv
nil
572
ref
1982
ref
appTerm
1984
def
axiom
nil
125
ref
1984
remove
nil
cons
cons
126
ref
1983
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
583
ref
576
ref
1982
remove
nil
cons
cons
768
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
1985
def
subst
trans
appThm
1965
ref
appThm
sym
nil
125
ref
1981
ref
cons
1986
def
1978
ref
cons
nil
cons
cons
1987
def
143
ref
subst
1987
remove
192
ref
subst
1980
ref
1878
ref
appTerm
1988
def
betaConv
nil
1986
remove
126
ref
1988
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
1297
ref
1294
ref
1980
remove
nil
cons
cons
1713
ref
1901
ref
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
74
ref
1979
remove
1892
ref
appTerm
appTerm
1963
remove
1975
remove
1276
ref
1278
ref
1281
ref
1878
remove
appTerm
1989
def
appTerm
1990
def
appTerm
1991
def
appTerm
1992
def
appTerm
1993
def
appTerm
nil
cons
cons
1978
remove
cons
nil
cons
cons
184
ref
subst
proveHyp
1005
ref
nil
125
ref
1993
ref
nil
cons
cons
1847
remove
1892
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
1898
remove
1005
ref
1245
ref
appThm
141
remove
appThm
156
remove
1985
ref
subst
trans
subst
subst
appThm
1965
remove
appThm
sym
nil
125
ref
1646
remove
1887
ref
appTerm
nil
cons
1994
def
cons
1995
def
126
ref
74
ref
1993
remove
appTerm
1964
remove
appTerm
nil
cons
1996
def
cons
nil
cons
1997
def
cons
nil
cons
cons
1998
def
143
ref
subst
1998
remove
192
ref
subst
1005
ref
95
ref
refl
1999
def
nil
1995
remove
126
ref
1944
remove
1643
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
nil
161
ref
1900
ref
cons
2000
def
nil
cons
nil
cons
cons
1670
remove
subst
eqMp
appThm
2001
def
1992
ref
refl
2002
def
appThm
nil
68
ref
1992
ref
nil
cons
2003
def
cons
nil
cons
nil
cons
cons
2004
def
68
ref
48
ref
95
ref
1643
ref
appTerm
2005
def
70
ref
appTerm
appTerm
70
ref
appTerm
absTerm
2006
def
70
ref
appTerm
2007
def
betaConv
nil
572
ref
2006
ref
appTerm
2008
def
axiom
nil
125
ref
2008
remove
nil
cons
cons
126
ref
2007
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
583
ref
576
ref
2006
remove
nil
cons
cons
768
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
2009
def
subst
trans
appThm
2001
remove
1958
ref
refl
2010
def
appThm
nil
68
ref
1958
remove
nil
cons
2011
def
cons
nil
cons
nil
cons
cons
2012
def
2009
ref
subst
trans
appThm
sym
nil
125
ref
2003
ref
cons
126
ref
2011
ref
cons
nil
cons
2013
def
cons
nil
cons
cons
2014
def
143
ref
subst
2014
remove
192
ref
subst
1264
remove
48
ref
1719
ref
appTerm
132
ref
1273
remove
appTerm
18
ref
19
ref
264
ref
265
ref
18
ref
75
ref
74
ref
1573
remove
appTerm
97
remove
1313
ref
1272
ref
268
remove
appTerm
appTerm
79
ref
appTerm
2015
def
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
2016
def
appTerm
2017
def
appTerm
appTerm
absTerm
2018
def
1272
ref
appTerm
2019
def
betaConv
11
ref
1263
remove
2018
ref
appTerm
2020
def
absTerm
2021
def
32
remove
appTerm
2022
def
betaConv
nil
298
ref
2021
ref
appTerm
2023
def
axiom
nil
125
ref
2023
remove
nil
cons
cons
126
ref
2022
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
42
remove
10
ref
2021
remove
nil
cons
cons
340
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
2020
remove
nil
cons
cons
126
ref
2019
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1292
remove
1291
remove
2018
remove
nil
cons
cons
1478
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
1719
remove
assume
eqMp
nil
1716
remove
162
ref
2017
remove
nil
cons
2024
def
cons
nil
cons
cons
nil
cons
cons
343
ref
subst
proveHyp
75
ref
74
ref
354
remove
1464
ref
114
ref
appTerm
2025
def
appTerm
2026
def
1804
remove
appTerm
appTerm
1781
ref
1313
ref
1272
remove
1798
ref
appTerm
2027
def
appTerm
2028
def
79
ref
appTerm
appTerm
appTerm
absTerm
2029
def
1435
ref
appTerm
2030
def
betaConv
265
remove
18
ref
75
ref
74
ref
2026
ref
361
remove
appTerm
appTerm
1781
ref
2015
remove
appTerm
appTerm
absTerm
appTerm
absTerm
2031
def
1798
remove
appTerm
2032
def
betaConv
2016
ref
114
ref
appTerm
2033
def
betaConv
nil
125
ref
2024
remove
cons
126
ref
2033
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
91
ref
73
ref
2016
remove
nil
cons
cons
185
ref
114
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
264
ref
2031
ref
appTerm
nil
cons
cons
126
ref
2032
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
391
ref
2031
remove
nil
cons
cons
1822
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
18
ref
2029
ref
appTerm
nil
cons
cons
126
ref
2030
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
2029
remove
nil
cons
cons
1446
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
74
ref
2026
remove
1812
remove
appTerm
appTerm
1781
ref
2028
ref
1435
remove
appTerm
appTerm
appTerm
nil
cons
cons
2013
ref
cons
nil
cons
cons
184
ref
subst
proveHyp
1005
ref
1005
ref
1522
remove
245
remove
1556
remove
subst
2034
def
1819
remove
trans
360
ref
refl
1803
ref
refl
1992
remove
assume
2035
def
appThm
appThm
2036
def
trans
appThm
2036
remove
appThm
nil
"x"
254
ref
var
360
remove
1803
remove
1991
ref
appTerm
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
277
remove
cons
nil
cons
43
ref
cons
1245
ref
subst
subst
trans
appThm
1781
ref
refl
2028
ref
refl
2037
def
2035
remove
appThm
appThm
appThm
nil
68
ref
1781
ref
2028
ref
1991
remove
appTerm
2038
def
appTerm
2039
def
nil
cons
2040
def
cons
nil
cons
nil
cons
cons
1985
ref
subst
trans
appThm
2010
ref
appThm
sym
nil
125
ref
2040
ref
cons
2013
remove
cons
nil
cons
cons
2041
def
143
ref
subst
2041
remove
192
ref
subst
48
ref
"_32464"
15
ref
var
2042
def
96
ref
2042
remove
varTerm
appTerm
1957
ref
appTerm
absTerm
2043
def
114
ref
appTerm
2044
def
appTerm
refl
2043
ref
2038
ref
appTerm
betaConv
appThm
164
ref
2044
remove
betaConv
appThm
96
ref
2038
remove
appTerm
1957
remove
appTerm
refl
appThm
trans
2043
remove
refl
2039
remove
assume
appThm
eqMp
sym
96
ref
refl
2037
remove
nil
1307
ref
1990
ref
nil
cons
2045
def
cons
nil
cons
nil
cons
cons
1324
ref
subst
appThm
appThm
nil
1307
remove
1956
remove
nil
cons
cons
nil
cons
nil
cons
cons
1324
remove
subst
1325
remove
1326
remove
nil
1375
remove
1901
remove
cons
1374
remove
1820
remove
cons
1328
remove
cons
cons
nil
cons
cons
1400
remove
subst
appThm
nil
1401
remove
1989
remove
nil
cons
cons
1402
remove
2027
remove
nil
cons
2046
def
cons
nil
cons
cons
nil
cons
cons
1415
remove
subst
trans
appThm
1339
remove
appThm
nil
1430
remove
1431
remove
2045
remove
cons
1432
remove
2046
remove
cons
nil
cons
cons
cons
nil
cons
cons
1447
remove
subst
trans
trans
appThm
nil
185
ref
2028
remove
1313
remove
1990
remove
appTerm
102
ref
appTerm
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
92
remove
1245
remove
subst
2047
def
subst
trans
sym
71
ref
eqMp
eqMp
eqMp
nil
161
ref
2040
remove
cons
162
ref
2011
remove
cons
nil
cons
2048
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
proveHyp
eqMp
nil
161
ref
2003
remove
cons
2048
remove
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
161
ref
1994
ref
cons
162
ref
1996
ref
cons
nil
cons
2049
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
125
ref
1900
ref
cons
1997
remove
cons
nil
cons
cons
2050
def
143
ref
subst
2050
remove
192
ref
subst
1005
ref
1999
ref
nil
68
ref
1900
ref
cons
nil
cons
nil
cons
cons
72
ref
subst
1887
ref
assume
eqMp
appThm
2051
def
2002
remove
appThm
2004
remove
68
ref
48
ref
95
ref
58
ref
appTerm
2052
def
70
ref
appTerm
appTerm
58
ref
appTerm
absTerm
2053
def
70
ref
appTerm
2054
def
betaConv
nil
572
ref
2053
ref
appTerm
2055
def
axiom
nil
125
ref
2055
remove
nil
cons
cons
126
ref
2054
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
583
ref
576
ref
2053
remove
nil
cons
cons
768
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
2056
def
subst
trans
appThm
2051
remove
2010
remove
appThm
2012
remove
2056
ref
subst
trans
appThm
nil
68
ref
684
ref
cons
nil
cons
nil
cons
cons
1985
remove
subst
trans
sym
71
ref
eqMp
eqMp
nil
2000
ref
2049
remove
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
68
ref
95
ref
70
ref
appTerm
1647
remove
appTerm
absTerm
2057
def
1887
remove
appTerm
2058
def
betaConv
nil
572
ref
2057
ref
appTerm
2059
def
axiom
nil
125
ref
2059
remove
nil
cons
cons
126
ref
2058
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
583
ref
576
ref
2057
remove
nil
cons
cons
622
ref
1900
remove
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
2000
remove
162
ref
1994
remove
cons
947
ref
1996
remove
cons
nil
cons
cons
cons
nil
cons
cons
962
ref
subst
proveHyp
proveHyp
proveHyp
eqMp
eqMp
eqMp
nil
161
ref
1981
remove
cons
162
ref
1977
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
proveHyp
proveHyp
eqMp
nil
161
ref
1946
remove
cons
162
ref
1947
remove
cons
nil
cons
2060
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
161
ref
1894
remove
cons
162
ref
1875
remove
cons
nil
cons
2061
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
161
ref
1890
remove
cons
2061
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
572
ref
622
ref
74
ref
1884
ref
622
remove
varTerm
appTerm
appTerm
1874
ref
appTerm
absTerm
appTerm
nil
cons
cons
126
ref
74
ref
1885
remove
appTerm
1874
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
583
ref
576
ref
1884
remove
nil
cons
cons
2061
ref
cons
nil
cons
cons
623
ref
subst
eqMp
eqMp
eqMp
nil
161
ref
1881
remove
cons
2061
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
1269
remove
1713
ref
74
ref
1863
ref
1713
ref
varTerm
appTerm
appTerm
1874
ref
appTerm
absTerm
appTerm
nil
cons
cons
126
ref
74
ref
1864
remove
appTerm
1874
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1297
ref
1294
ref
1863
remove
nil
cons
cons
2061
remove
cons
nil
cons
cons
623
ref
subst
eqMp
eqMp
eqMp
proveHyp
proveHyp
eqMp
nil
161
ref
1815
remove
cons
162
ref
1794
ref
cons
nil
cons
2062
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
161
ref
1809
remove
cons
2062
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
18
ref
185
ref
74
ref
1805
ref
914
remove
appTerm
appTerm
1790
ref
appTerm
absTerm
appTerm
nil
cons
cons
126
ref
74
ref
1806
remove
appTerm
1790
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
1805
remove
nil
cons
cons
2062
ref
cons
nil
cons
cons
623
ref
subst
eqMp
eqMp
eqMp
nil
161
ref
1801
remove
cons
2062
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
264
ref
452
ref
920
remove
1790
ref
appTerm
absTerm
appTerm
nil
cons
cons
126
ref
921
remove
1790
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
922
remove
2062
ref
cons
nil
cons
cons
623
ref
subst
eqMp
nil
924
remove
1795
remove
cons
nil
cons
cons
2063
def
143
ref
subst
2063
remove
192
ref
subst
48
ref
"_32402"
254
remove
var
2064
def
74
ref
1723
ref
1726
ref
275
remove
2064
remove
varTerm
appTerm
appTerm
appTerm
1732
ref
appTerm
appTerm
1782
ref
appTerm
absTerm
2065
def
374
remove
appTerm
2066
def
appTerm
refl
2065
ref
357
remove
appTerm
betaConv
appThm
164
ref
2066
remove
betaConv
appThm
74
ref
1723
ref
1726
ref
1241
remove
appTerm
appTerm
1732
ref
appTerm
appTerm
1782
remove
appTerm
refl
appThm
trans
2065
remove
refl
926
remove
appThm
eqMp
sym
1005
ref
1783
ref
1784
ref
936
ref
appThm
397
ref
1842
remove
1843
remove
176
ref
subst
proveHyp
subst
2067
def
trans
appThm
1785
ref
appThm
nil
1938
ref
1940
ref
1851
ref
684
remove
cons
1849
remove
1365
remove
cons
nil
cons
2068
def
cons
cons
cons
nil
cons
cons
1942
ref
subst
2069
def
trans
appThm
1786
remove
appThm
sym
nil
125
ref
132
ref
1331
remove
1309
ref
appTerm
1729
ref
appTerm
2070
def
appTerm
2071
def
48
ref
58
ref
appTerm
2072
def
1731
ref
appTerm
2073
def
appTerm
nil
cons
2074
def
cons
1948
remove
cons
nil
cons
cons
2075
def
143
ref
subst
2075
remove
192
ref
subst
nil
161
ref
2070
ref
nil
cons
cons
2076
def
162
ref
2073
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
2077
def
176
ref
subst
2077
remove
343
ref
subst
1954
remove
"_32404"
1265
ref
var
2078
def
1735
ref
1781
ref
1276
ref
1278
ref
1281
ref
2078
remove
varTerm
appTerm
appTerm
appTerm
appTerm
appTerm
absTerm
1309
ref
appTerm
betaConv
appThm
1955
remove
1735
ref
1781
remove
1372
ref
appTerm
2079
def
appTerm
refl
appThm
trans
1959
remove
2070
remove
assume
sym
2080
def
appThm
eqMp
sym
48
ref
"_32410"
7
ref
var
2081
def
95
ref
2081
remove
varTerm
appTerm
2079
ref
appTerm
absTerm
2082
def
1731
ref
appTerm
2083
def
appTerm
refl
2082
ref
58
remove
appTerm
betaConv
appThm
164
ref
2083
remove
betaConv
appThm
2052
remove
2079
ref
appTerm
refl
appThm
trans
2082
remove
refl
2073
remove
assume
sym
appThm
eqMp
sym
nil
68
ref
2079
remove
nil
cons
cons
nil
cons
nil
cons
cons
2056
ref
subst
sym
71
ref
eqMp
eqMp
eqMp
proveHyp
proveHyp
eqMp
nil
161
ref
2074
remove
cons
2060
remove
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
945
ref
2062
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
945
remove
946
remove
947
ref
1794
remove
cons
nil
cons
cons
cons
nil
cons
cons
962
ref
subst
proveHyp
proveHyp
eqMp
nil
963
remove
2062
remove
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
nil
161
ref
1789
remove
cons
162
ref
1792
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
964
ref
162
ref
1767
ref
cons
nil
cons
2084
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
966
ref
2084
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
18
ref
185
ref
967
ref
1765
ref
appTerm
absTerm
appTerm
nil
cons
cons
126
ref
968
ref
1765
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
969
ref
2084
ref
cons
nil
cons
cons
623
ref
subst
eqMp
eqMp
eqMp
nil
970
ref
2084
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
51
ref
1772
remove
appTerm
nil
cons
cons
126
ref
971
ref
1765
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
972
ref
2084
ref
cons
nil
cons
cons
623
ref
subst
eqMp
nil
974
ref
1768
ref
cons
nil
cons
cons
2085
def
143
ref
subst
2085
remove
192
ref
subst
nil
125
ref
1764
remove
nil
cons
2086
def
cons
126
ref
1757
remove
nil
cons
2087
def
cons
nil
cons
cons
nil
cons
cons
2088
def
143
ref
subst
2089
def
2088
remove
192
ref
subst
2090
def
nil
1294
remove
1755
remove
nil
cons
cons
2091
def
nil
cons
nil
cons
cons
1298
remove
subst
2092
def
1717
ref
nil
68
ref
1754
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
2093
def
48
ref
"_32386"
15
ref
var
2094
def
74
ref
1723
ref
1726
ref
33
ref
2094
remove
varTerm
2095
def
appTerm
appTerm
appTerm
1732
ref
appTerm
appTerm
1735
ref
96
ref
2095
remove
appTerm
1736
ref
appTerm
appTerm
appTerm
absTerm
2096
def
34
ref
appTerm
2097
def
appTerm
refl
2098
def
2096
ref
102
ref
appTerm
betaConv
appThm
164
ref
2097
remove
betaConv
appThm
2099
def
74
ref
1723
ref
1726
ref
290
remove
appTerm
appTerm
1732
ref
appTerm
appTerm
1735
ref
96
ref
102
ref
appTerm
2100
def
1736
ref
appTerm
appTerm
2101
def
appTerm
refl
appThm
trans
2096
remove
refl
2102
def
981
ref
appThm
eqMp
sym
1005
ref
1783
ref
1784
ref
982
ref
appThm
397
remove
1844
remove
1846
remove
176
ref
subst
proveHyp
subst
trans
appThm
1785
ref
appThm
nil
1938
remove
1940
remove
1851
remove
1644
remove
cons
2068
remove
cons
cons
cons
nil
cons
cons
1942
remove
subst
trans
appThm
2101
ref
refl
appThm
sym
nil
125
ref
2071
ref
1667
remove
1731
ref
appTerm
2103
def
appTerm
nil
cons
2104
def
cons
126
ref
2101
remove
nil
cons
2105
def
cons
nil
cons
cons
nil
cons
cons
2106
def
143
ref
subst
2106
remove
192
ref
subst
nil
2076
ref
162
ref
2103
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
2107
def
176
ref
subst
2107
remove
343
ref
subst
48
ref
"_32390"
1265
remove
var
2108
def
1735
ref
2100
ref
1276
remove
1278
remove
1281
remove
2108
remove
varTerm
appTerm
appTerm
appTerm
appTerm
appTerm
absTerm
2109
def
1729
remove
appTerm
2110
def
appTerm
refl
2109
ref
1309
remove
appTerm
betaConv
appThm
164
ref
2110
remove
betaConv
appThm
1735
ref
2100
ref
1372
remove
appTerm
2111
def
appTerm
refl
appThm
trans
2109
remove
refl
2080
remove
appThm
eqMp
sym
48
ref
"_32394"
7
remove
var
2112
def
95
remove
2112
remove
varTerm
appTerm
2111
ref
appTerm
absTerm
2113
def
1731
ref
appTerm
2114
def
appTerm
refl
2113
ref
1643
remove
appTerm
betaConv
appThm
164
ref
2114
remove
betaConv
appThm
2005
remove
2111
ref
appTerm
refl
appThm
trans
2113
remove
refl
2103
remove
assume
sym
appThm
eqMp
sym
nil
68
ref
2111
remove
nil
cons
cons
nil
cons
nil
cons
cons
2009
remove
subst
2100
remove
refl
1364
remove
appThm
nil
185
ref
1340
remove
cons
nil
cons
nil
cons
cons
2047
remove
subst
trans
trans
sym
71
ref
eqMp
eqMp
eqMp
proveHyp
proveHyp
eqMp
nil
161
ref
2104
remove
cons
162
ref
2105
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
nil
161
ref
2086
remove
cons
162
ref
2087
ref
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
2115
def
deductAntisym
eqMp
eqMp
nil
989
ref
2084
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
989
ref
990
ref
947
ref
1767
remove
cons
nil
cons
2116
def
cons
cons
nil
cons
cons
962
ref
subst
proveHyp
proveHyp
eqMp
nil
992
ref
2084
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
994
ref
1768
remove
cons
nil
cons
cons
2117
def
143
ref
subst
2117
remove
192
ref
subst
2089
remove
2090
remove
2092
remove
1717
remove
2093
remove
2098
remove
"_32382"
15
ref
var
2118
def
74
ref
1723
ref
1726
ref
33
ref
2118
remove
varTerm
2119
def
appTerm
appTerm
appTerm
1732
ref
appTerm
appTerm
1735
ref
96
ref
2119
remove
appTerm
1736
ref
appTerm
appTerm
appTerm
absTerm
99
ref
appTerm
betaConv
appThm
2099
remove
74
remove
1723
remove
1726
remove
287
remove
appTerm
appTerm
1732
remove
appTerm
appTerm
1735
remove
96
remove
99
ref
appTerm
1736
remove
appTerm
2120
def
appTerm
2121
def
appTerm
refl
appThm
trans
2102
remove
1000
ref
appThm
eqMp
sym
1005
ref
1783
remove
1784
remove
1001
ref
appThm
2067
remove
trans
appThm
1785
remove
appThm
2069
remove
2071
ref
refl
nil
68
ref
1937
ref
cons
nil
cons
nil
cons
cons
2122
def
68
ref
48
ref
2072
remove
70
ref
appTerm
appTerm
70
ref
appTerm
absTerm
2123
def
70
remove
appTerm
2124
def
betaConv
nil
572
remove
2123
ref
appTerm
2125
def
axiom
nil
125
ref
2125
remove
nil
cons
cons
126
ref
2124
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
583
remove
576
remove
2123
remove
nil
cons
cons
768
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
appThm
trans
trans
appThm
2121
ref
refl
appThm
sym
nil
125
ref
2071
remove
1731
ref
appTerm
nil
cons
2126
def
cons
126
ref
2121
remove
nil
cons
2127
def
cons
nil
cons
cons
nil
cons
cons
2128
def
143
ref
subst
2128
remove
192
ref
subst
nil
2076
remove
162
ref
1937
remove
cons
nil
cons
cons
nil
cons
cons
343
ref
subst
1999
remove
2122
remove
72
ref
subst
1731
remove
assume
eqMp
appThm
2120
ref
refl
appThm
nil
68
ref
2120
remove
nil
cons
cons
nil
cons
nil
cons
cons
2056
remove
subst
trans
sym
71
ref
eqMp
proveHyp
eqMp
nil
161
ref
2126
remove
cons
162
ref
2127
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
2115
remove
deductAntisym
eqMp
eqMp
nil
1002
ref
2084
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
1002
ref
1003
ref
2116
remove
cons
cons
nil
cons
cons
962
ref
subst
proveHyp
proveHyp
eqMp
nil
1004
ref
2084
remove
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
absThm
eqMp
nil
125
ref
18
ref
1766
remove
appTerm
nil
cons
cons
126
ref
18
ref
1758
ref
appTerm
nil
cons
2129
def
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1005
ref
1006
ref
19
ref
1005
remove
1006
ref
75
ref
1007
remove
1758
ref
79
remove
appTerm
betaConv
appThm
absThm
appThm
appThm
1760
ref
appThm
absThm
appThm
appThm
1006
remove
19
ref
1760
remove
absThm
appThm
appThm
nil
1009
remove
1758
remove
nil
cons
2130
def
cons
nil
cons
nil
cons
cons
1015
remove
subst
eqMp
eqMp
nil
125
ref
2129
remove
cons
126
ref
1759
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
ref
2130
remove
cons
187
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
2087
remove
cons
126
ref
1756
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
1297
remove
2091
remove
1713
remove
1939
remove
cons
nil
cons
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
eqMp
proveHyp
proveHyp
eqMp
nil
161
ref
1748
remove
cons
162
ref
1749
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
298
ref
1747
remove
appTerm
thm
nil
10
remove
11
ref
18
ref
19
ref
1587
remove
255
ref
"Parser.Stream.case.error.eof.cons"
const
2131
def
0
ref
25
ref
0
ref
25
ref
0
ref
0
ref
2
ref
31
ref
cons
opType
2132
def
31
remove
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
256
ref
appTerm
292
remove
appTerm
834
remove
75
remove
256
remove
absTerm
2133
def
absTerm
2134
def
appTerm
2135
def
34
ref
appTerm
appTerm
274
ref
appTerm
1570
remove
appTerm
appTerm
2136
def
absTerm
2137
def
appTerm
2138
def
absTerm
2139
def
nil
cons
cons
nil
cons
nil
cons
cons
67
remove
subst
11
remove
nil
68
ref
2138
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
73
ref
2137
ref
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
19
ref
nil
68
ref
2136
ref
nil
cons
2140
def
cons
nil
cons
nil
cons
cons
72
ref
subst
195
remove
nil
197
remove
126
ref
2140
ref
cons
nil
cons
2141
def
cons
nil
cons
cons
2142
def
184
ref
subst
proveHyp
2142
ref
143
ref
subst
2142
remove
192
ref
subst
nil
201
remove
2141
ref
cons
nil
cons
cons
2143
def
143
ref
subst
2143
remove
192
ref
subst
nil
52
ref
57
ref
204
remove
2136
ref
appTerm
2144
def
absTerm
2145
def
nil
cons
cons
nil
cons
nil
cons
cons
66
remove
subst
57
ref
nil
68
ref
2144
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
ref
subst
nil
208
remove
2141
ref
cons
nil
cons
cons
2146
def
143
ref
subst
2146
remove
192
ref
subst
210
remove
nil
211
remove
2141
ref
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
73
ref
107
ref
213
remove
2136
ref
appTerm
2147
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
93
remove
subst
107
remove
nil
68
remove
2147
remove
nil
cons
cons
nil
cons
nil
cons
cons
72
remove
subst
nil
216
remove
2141
ref
cons
nil
cons
cons
2148
def
143
ref
subst
2148
remove
192
ref
subst
218
remove
nil
220
remove
2141
ref
cons
nil
cons
cons
2149
def
184
ref
subst
proveHyp
2149
ref
143
ref
subst
2149
remove
192
ref
subst
48
remove
"_32314"
15
ref
var
2150
def
246
ref
33
ref
2150
remove
varTerm
2151
def
appTerm
appTerm
255
ref
2135
ref
2151
ref
appTerm
appTerm
274
ref
appTerm
1464
ref
2151
remove
appTerm
appTerm
appTerm
absTerm
2152
def
34
ref
appTerm
2153
def
appTerm
refl
2154
def
2152
remove
114
ref
appTerm
betaConv
appThm
164
remove
2153
remove
betaConv
appThm
2155
def
246
ref
232
remove
appTerm
255
ref
2135
ref
114
remove
appTerm
appTerm
274
ref
appTerm
2025
remove
appTerm
appTerm
refl
appThm
trans
2137
remove
refl
2156
def
236
remove
appThm
eqMp
sym
495
ref
352
remove
appThm
255
ref
refl
2157
def
nil
244
remove
"f"
2132
remove
var
2134
ref
nil
cons
cons
423
remove
1367
remove
cons
2158
def
"e"
25
remove
var
424
ref
cons
nil
cons
cons
cons
2159
def
cons
nil
cons
cons
347
remove
427
remove
cons
43
remove
cons
2160
def
19
remove
430
ref
2131
remove
0
ref
3
ref
0
ref
3
ref
0
ref
0
ref
2
remove
0
ref
15
ref
4
remove
cons
opType
nil
cons
2161
def
cons
opType
2162
def
2161
remove
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
"e"
3
remove
var
2163
def
varTerm
2164
def
appTerm
434
ref
appTerm
"f"
2162
ref
var
2165
def
varTerm
2166
def
appTerm
2167
def
247
remove
appTerm
appTerm
2166
ref
111
ref
appTerm
34
ref
appTerm
appTerm
absTerm
2168
def
34
remove
appTerm
2169
def
betaConv
57
remove
18
ref
2168
ref
appTerm
2170
def
absTerm
2171
def
111
ref
appTerm
2172
def
betaConv
2165
ref
51
ref
2171
ref
appTerm
2173
def
absTerm
2174
def
2166
ref
appTerm
2175
def
betaConv
433
ref
12
remove
0
ref
0
remove
2162
ref
8
ref
cons
opType
2176
def
8
remove
cons
opType
constTerm
2177
def
2174
ref
appTerm
2178
def
absTerm
2179
def
434
ref
appTerm
2180
def
betaConv
2163
ref
264
ref
2179
ref
appTerm
2181
def
absTerm
2182
def
2164
ref
appTerm
2183
def
betaConv
nil
132
ref
264
ref
2163
ref
264
ref
433
ref
2177
ref
2165
ref
430
ref
2167
ref
99
ref
appTerm
appTerm
2164
ref
appTerm
absTerm
2184
def
appTerm
2185
def
absTerm
2186
def
appTerm
2187
def
absTerm
2188
def
appTerm
2189
def
appTerm
132
remove
264
ref
2163
remove
264
ref
433
remove
2177
remove
2165
remove
430
remove
2167
remove
102
ref
appTerm
appTerm
434
ref
appTerm
absTerm
2190
def
appTerm
2191
def
absTerm
2192
def
appTerm
2193
def
absTerm
2194
def
appTerm
2195
def
appTerm
264
remove
2182
ref
appTerm
2196
def
appTerm
2197
def
appTerm
axiom
2198
def
nil
161
ref
2189
remove
nil
cons
2199
def
cons
162
ref
2197
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
2200
def
343
ref
subst
proveHyp
2201
def
nil
161
remove
2195
remove
nil
cons
2202
def
cons
162
ref
2196
remove
nil
cons
2203
def
cons
nil
cons
cons
nil
cons
cons
2204
def
343
remove
subst
proveHyp
nil
125
ref
2203
remove
cons
126
ref
2183
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
391
ref
2182
remove
nil
cons
cons
452
remove
2164
ref
nil
cons
cons
nil
cons
2205
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
2181
remove
nil
cons
cons
126
ref
2180
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
391
ref
2179
remove
nil
cons
cons
453
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
2178
remove
nil
cons
cons
126
ref
2175
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
"A"
2162
ref
nil
cons
cons
nil
cons
2206
def
"P"
2176
remove
var
2207
def
2174
remove
nil
cons
cons
"x"
2162
remove
var
2166
ref
nil
cons
cons
nil
cons
2208
def
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
2173
remove
nil
cons
cons
126
ref
2172
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
ref
52
remove
2171
remove
nil
cons
cons
350
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
2170
remove
nil
cons
cons
126
ref
2169
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
ref
73
remove
2168
remove
nil
cons
cons
187
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
subst
2134
remove
111
remove
appTerm
betaConv
113
ref
refl
appThm
2133
remove
113
remove
appTerm
betaConv
trans
trans
appThm
274
ref
refl
2209
def
appThm
2034
remove
appThm
appThm
nil
1369
ref
386
remove
nil
cons
cons
nil
cons
nil
cons
cons
1370
ref
subst
trans
sym
71
ref
eqMp
eqMp
eqMp
nil
964
remove
162
remove
2140
ref
cons
nil
cons
2210
def
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
966
remove
2210
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
18
remove
185
remove
967
remove
2136
ref
appTerm
absTerm
appTerm
nil
cons
cons
126
ref
968
remove
2136
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
91
remove
969
remove
2210
ref
cons
nil
cons
cons
623
ref
subst
eqMp
eqMp
eqMp
nil
970
remove
2210
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
125
ref
51
remove
2145
remove
appTerm
nil
cons
cons
126
ref
971
remove
2136
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
348
remove
972
remove
2210
ref
cons
nil
cons
cons
623
remove
subst
eqMp
nil
974
remove
2141
ref
cons
nil
cons
cons
2211
def
143
ref
subst
2211
remove
192
ref
subst
2154
ref
"_32312"
15
ref
var
2212
def
246
ref
33
ref
2212
remove
varTerm
2213
def
appTerm
appTerm
255
ref
2135
ref
2213
ref
appTerm
appTerm
274
ref
appTerm
1464
ref
2213
remove
appTerm
appTerm
appTerm
absTerm
102
ref
appTerm
betaConv
appThm
2155
ref
291
remove
255
ref
2135
ref
102
remove
appTerm
appTerm
274
ref
appTerm
1534
remove
appTerm
appTerm
refl
appThm
trans
2156
ref
981
remove
appThm
eqMp
sym
495
ref
982
remove
appThm
2157
ref
nil
2159
remove
nil
cons
cons
2214
def
2160
ref
2190
ref
2166
ref
appTerm
2215
def
betaConv
2192
ref
434
ref
appTerm
2216
def
betaConv
2194
ref
2164
ref
appTerm
2217
def
betaConv
2201
remove
2204
remove
176
ref
subst
proveHyp
nil
125
ref
2202
remove
cons
126
ref
2217
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
391
ref
2194
remove
nil
cons
cons
2205
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
2193
remove
nil
cons
cons
126
ref
2216
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
391
ref
2192
remove
nil
cons
cons
453
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
2191
remove
nil
cons
cons
126
ref
2215
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
2206
ref
2207
ref
2190
remove
nil
cons
cons
2208
ref
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
subst
subst
appThm
2209
ref
appThm
1553
remove
1555
remove
176
ref
subst
proveHyp
appThm
nil
422
remove
2158
remove
nil
cons
cons
nil
cons
cons
935
remove
subst
trans
appThm
1371
remove
trans
sym
71
ref
eqMp
eqMp
eqMp
nil
989
ref
2210
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
989
remove
990
remove
947
remove
2140
remove
cons
nil
cons
2218
def
cons
cons
nil
cons
cons
962
ref
subst
proveHyp
proveHyp
eqMp
nil
992
remove
2210
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
994
remove
2141
remove
cons
nil
cons
cons
2219
def
143
remove
subst
2219
remove
192
remove
subst
2154
remove
"_32310"
15
remove
var
2220
def
246
remove
33
remove
2220
remove
varTerm
2221
def
appTerm
appTerm
255
ref
2135
ref
2221
ref
appTerm
appTerm
274
ref
appTerm
1464
remove
2221
remove
appTerm
appTerm
appTerm
absTerm
99
ref
appTerm
betaConv
appThm
2155
remove
288
remove
255
remove
2135
remove
99
remove
appTerm
appTerm
274
remove
appTerm
1532
remove
appTerm
appTerm
refl
appThm
trans
2156
remove
1000
remove
appThm
eqMp
sym
495
remove
1001
remove
appThm
2157
remove
2214
remove
2160
remove
2184
ref
2166
remove
appTerm
2222
def
betaConv
2186
ref
434
remove
appTerm
2223
def
betaConv
2188
ref
2164
remove
appTerm
2224
def
betaConv
2198
remove
2200
remove
176
ref
subst
proveHyp
nil
125
ref
2199
remove
cons
126
ref
2224
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
ref
391
ref
2188
remove
nil
cons
cons
2205
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
ref
2187
remove
nil
cons
cons
126
ref
2223
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
396
remove
391
remove
2186
remove
nil
cons
cons
453
remove
cons
nil
cons
cons
194
ref
subst
eqMp
eqMp
nil
125
remove
2185
remove
nil
cons
cons
126
remove
2222
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
remove
subst
proveHyp
2206
remove
2207
remove
2184
remove
nil
cons
cons
2208
remove
cons
nil
cons
cons
194
remove
subst
eqMp
eqMp
subst
subst
appThm
2209
remove
appThm
1551
remove
1552
remove
176
ref
subst
proveHyp
appThm
936
remove
trans
appThm
nil
1369
remove
424
remove
cons
nil
cons
nil
cons
cons
1370
remove
subst
trans
sym
71
remove
eqMp
eqMp
eqMp
nil
1002
ref
2210
ref
cons
nil
cons
cons
176
ref
subst
deductAntisym
eqMp
nil
1002
remove
1003
remove
2218
remove
cons
cons
nil
cons
cons
962
remove
subst
proveHyp
proveHyp
eqMp
nil
1004
remove
2210
remove
cons
nil
cons
cons
176
remove
subst
deductAntisym
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
298
remove
2139
remove
appTerm
thm
339
remove
nil
301
remove
338
remove
appTerm
thm