6
version
nil
"P"
"->"
typeOp
0
def
0
ref
"A"
varType
1
def
0
ref
"C"
varType
2
def
"Data.Option.option"
typeOp
3
def
"Data.Sum.+"
typeOp
4
def
"B"
varType
5
def
2
ref
nil
cons
6
def
cons
7
def
opType
8
def
nil
cons
9
def
opType
10
def
nil
cons
11
def
cons
opType
nil
cons
cons
opType
12
def
"bool"
typeOp
nil
opType
13
def
nil
cons
14
def
cons
opType
15
def
var
16
def
"f"
12
ref
var
17
def
"Data.Bool.!"
const
18
def
0
ref
0
ref
2
ref
14
ref
cons
opType
19
def
14
ref
cons
opType
20
def
constTerm
21
def
"s"
2
ref
var
22
def
"Parser.invariant"
const
0
ref
0
ref
1
ref
0
ref
"Parser.Stream.stream"
typeOp
1
ref
nil
cons
23
def
opType
24
def
3
ref
"Data.Pair.*"
typeOp
25
def
5
ref
24
ref
nil
cons
26
def
cons
opType
27
def
nil
cons
28
def
opType
29
def
nil
cons
30
def
cons
opType
31
def
nil
cons
32
def
cons
opType
33
def
14
ref
cons
opType
34
def
constTerm
35
def
"Parser.fold.prs"
const
0
ref
12
ref
0
ref
2
ref
33
ref
nil
cons
36
def
cons
opType
37
def
nil
cons
cons
opType
constTerm
17
ref
varTerm
38
def
appTerm
39
def
22
ref
varTerm
40
def
appTerm
41
def
appTerm
42
def
absTerm
43
def
appTerm
44
def
absTerm
45
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
12
ref
nil
cons
cons
nil
cons
46
def
nil
nil
cons
47
def
cons
48
def
"="
const
49
def
0
ref
13
ref
0
ref
13
ref
14
ref
cons
opType
50
def
nil
cons
cons
opType
51
def
constTerm
52
def
18
ref
0
ref
0
ref
1
ref
14
ref
cons
opType
53
def
14
ref
cons
opType
54
def
constTerm
55
def
"P"
53
ref
var
56
def
varTerm
57
def
appTerm
58
def
appTerm
refl
"p"
53
ref
var
59
def
49
ref
0
ref
53
ref
54
ref
nil
cons
cons
opType
constTerm
59
ref
varTerm
60
def
appTerm
"x"
1
ref
var
61
def
"Data.Bool.T"
const
13
ref
constTerm
62
def
absTerm
63
def
appTerm
absTerm
64
def
57
ref
appTerm
betaConv
65
def
appThm
nil
49
ref
0
ref
54
ref
0
ref
54
ref
14
ref
cons
opType
66
def
nil
cons
cons
opType
constTerm
67
def
55
ref
appTerm
64
remove
appTerm
axiom
57
ref
refl
68
def
appThm
69
def
eqMp
sym
70
def
subst
71
def
subst
17
ref
nil
"t"
13
ref
var
72
def
44
remove
nil
cons
cons
nil
cons
nil
cons
cons
52
ref
72
ref
varTerm
73
def
appTerm
62
ref
appTerm
assume
sym
nil
62
ref
axiom
74
def
eqMp
73
ref
assume
74
ref
deductAntisym
deductAntisym
75
def
subst
nil
"P"
19
ref
var
76
def
43
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
6
ref
cons
77
def
nil
cons
78
def
47
ref
cons
79
def
70
ref
subst
80
def
subst
22
ref
nil
72
ref
42
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
"p"
33
ref
var
81
def
41
ref
nil
cons
82
def
cons
nil
cons
nil
cons
cons
81
ref
52
ref
35
ref
81
remove
varTerm
83
def
appTerm
appTerm
55
ref
61
ref
18
ref
0
ref
0
ref
24
ref
14
ref
cons
opType
84
def
14
ref
cons
opType
85
def
constTerm
86
def
"xs"
24
ref
var
87
def
"Data.Option.case.none.some"
const
88
def
0
ref
13
ref
0
ref
0
ref
27
ref
14
ref
cons
opType
89
def
0
ref
29
ref
14
ref
cons
opType
90
def
nil
cons
91
def
cons
opType
nil
cons
cons
opType
constTerm
62
ref
appTerm
92
def
"select"
const
93
def
0
ref
0
ref
89
ref
14
ref
cons
opType
94
def
89
ref
nil
cons
95
def
cons
opType
constTerm
96
def
"f"
89
ref
var
97
def
18
ref
0
ref
0
ref
5
ref
14
ref
cons
opType
98
def
14
ref
cons
opType
99
def
constTerm
100
def
"y"
5
ref
var
101
def
86
ref
"ys"
24
ref
var
102
def
52
ref
97
ref
varTerm
"Data.Pair.,"
const
103
def
0
ref
5
ref
0
ref
24
ref
28
ref
cons
opType
nil
cons
cons
opType
constTerm
104
def
101
ref
varTerm
105
def
appTerm
106
def
102
ref
varTerm
107
def
appTerm
108
def
appTerm
appTerm
109
def
"Parser.Stream.isSuffix"
const
0
ref
24
ref
84
ref
nil
cons
110
def
cons
opType
111
def
constTerm
112
def
107
ref
appTerm
113
def
87
ref
varTerm
114
def
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
115
def
83
ref
61
ref
varTerm
116
def
appTerm
114
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
117
def
83
ref
appTerm
118
def
betaConv
nil
18
ref
0
ref
34
ref
14
ref
cons
opType
constTerm
119
def
117
ref
appTerm
120
def
axiom
nil
"p"
13
ref
var
121
def
120
remove
nil
cons
cons
"q"
13
ref
var
122
def
118
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
52
ref
"Data.Bool.==>"
const
51
ref
constTerm
123
def
121
ref
varTerm
124
def
appTerm
125
def
122
ref
varTerm
126
def
appTerm
127
def
appTerm
128
def
refl
121
ref
122
ref
52
ref
"Data.Bool./\\"
const
51
ref
constTerm
129
def
124
ref
appTerm
130
def
126
ref
appTerm
131
def
appTerm
132
def
124
ref
appTerm
absTerm
133
def
absTerm
134
def
124
ref
appTerm
betaConv
126
ref
refl
135
def
appThm
133
remove
126
ref
appTerm
betaConv
trans
appThm
nil
49
ref
0
ref
51
ref
0
ref
51
ref
14
ref
cons
opType
136
def
nil
cons
cons
opType
constTerm
137
def
123
ref
appTerm
134
remove
appTerm
axiom
124
ref
refl
138
def
appThm
135
ref
appThm
eqMp
139
def
sym
140
def
132
remove
refl
122
ref
49
ref
0
ref
136
ref
0
ref
136
remove
14
ref
cons
opType
nil
cons
cons
opType
constTerm
141
def
"f"
51
ref
var
142
def
142
ref
varTerm
143
def
124
ref
appTerm
126
ref
appTerm
absTerm
144
def
appTerm
142
ref
143
ref
62
ref
appTerm
62
ref
appTerm
absTerm
145
def
appTerm
absTerm
146
def
126
ref
appTerm
betaConv
appThm
49
ref
0
ref
50
ref
0
ref
50
ref
14
ref
cons
opType
147
def
nil
cons
cons
opType
constTerm
148
def
130
remove
appTerm
refl
121
ref
146
remove
absTerm
149
def
124
ref
appTerm
betaConv
appThm
nil
137
ref
129
ref
appTerm
149
ref
appTerm
axiom
150
def
138
remove
appThm
eqMp
135
ref
appThm
eqMp
151
def
sym
142
ref
143
ref
refl
nil
72
ref
124
ref
nil
cons
152
def
cons
nil
cons
nil
cons
cons
75
ref
subst
124
ref
assume
153
def
eqMp
appThm
nil
72
ref
126
ref
nil
cons
154
def
cons
nil
cons
nil
cons
cons
75
ref
subst
126
ref
assume
155
def
eqMp
appThm
absThm
eqMp
156
def
nil
"P"
13
ref
var
157
def
152
ref
cons
"Q"
13
ref
var
158
def
154
ref
cons
nil
cons
159
def
cons
nil
cons
cons
52
ref
refl
160
def
142
ref
143
remove
157
ref
varTerm
161
def
appTerm
162
def
158
ref
varTerm
163
def
appTerm
absTerm
164
def
121
ref
122
ref
124
ref
absTerm
absTerm
165
def
appTerm
betaConv
165
ref
161
ref
appTerm
betaConv
163
ref
refl
166
def
appThm
122
ref
161
ref
absTerm
163
ref
appTerm
betaConv
trans
trans
appThm
145
ref
165
ref
appTerm
betaConv
165
ref
62
ref
appTerm
betaConv
62
ref
refl
167
def
appThm
122
ref
62
ref
absTerm
62
ref
appTerm
betaConv
trans
trans
appThm
52
ref
129
ref
161
ref
appTerm
168
def
163
ref
appTerm
169
def
appTerm
refl
122
ref
141
remove
142
remove
162
remove
126
ref
appTerm
absTerm
appTerm
145
ref
appTerm
absTerm
163
ref
appTerm
betaConv
appThm
148
ref
168
remove
appTerm
refl
149
remove
161
ref
appTerm
betaConv
appThm
150
remove
161
ref
refl
170
def
appThm
eqMp
166
ref
appThm
eqMp
169
remove
assume
eqMp
171
def
165
remove
refl
appThm
eqMp
sym
74
ref
eqMp
172
def
subst
173
def
deductAntisym
eqMp
139
remove
127
ref
assume
eqMp
sym
153
ref
eqMp
160
ref
144
remove
121
ref
122
ref
126
ref
absTerm
174
def
absTerm
175
def
appTerm
betaConv
175
ref
124
ref
appTerm
betaConv
135
remove
appThm
174
ref
126
ref
appTerm
betaConv
trans
trans
appThm
145
remove
175
ref
appTerm
betaConv
175
ref
62
ref
appTerm
betaConv
167
remove
appThm
174
ref
62
ref
appTerm
betaConv
trans
trans
176
def
appThm
151
remove
131
remove
assume
eqMp
175
ref
refl
177
def
appThm
eqMp
sym
74
ref
eqMp
178
def
proveHyp
179
def
deductAntisym
180
def
subst
proveHyp
"A"
36
ref
cons
nil
cons
181
def
"P"
34
ref
var
182
def
117
remove
nil
cons
cons
"x"
33
ref
var
183
def
83
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
121
ref
58
ref
nil
cons
184
def
cons
122
ref
57
ref
116
ref
appTerm
185
def
nil
cons
186
def
cons
nil
cons
cons
nil
cons
cons
187
def
140
ref
subst
187
remove
178
remove
156
remove
deductAntisym
188
def
subst
52
ref
185
ref
appTerm
refl
63
remove
116
ref
appTerm
betaConv
appThm
65
remove
69
remove
58
remove
assume
eqMp
eqMp
116
ref
refl
189
def
appThm
eqMp
sym
74
ref
eqMp
eqMp
nil
157
ref
184
remove
cons
158
ref
186
ref
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
190
def
subst
eqMp
eqMp
subst
sym
nil
56
ref
61
ref
86
ref
87
ref
115
remove
41
ref
116
ref
appTerm
191
def
114
ref
appTerm
192
def
appTerm
193
def
absTerm
194
def
appTerm
195
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
61
ref
nil
72
ref
195
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
"P"
84
ref
var
196
def
194
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
26
ref
cons
197
def
nil
cons
198
def
47
ref
cons
70
ref
subst
199
def
subst
87
ref
nil
72
ref
193
ref
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
22
ref
193
remove
absTerm
200
def
40
ref
appTerm
201
def
betaConv
61
ref
21
ref
200
ref
appTerm
202
def
absTerm
203
def
116
ref
appTerm
204
def
betaConv
87
ref
55
ref
203
ref
appTerm
205
def
absTerm
206
def
114
ref
appTerm
207
def
betaConv
208
def
nil
56
ref
61
ref
21
ref
22
ref
92
ref
96
ref
97
ref
100
ref
101
ref
86
ref
102
ref
109
ref
113
ref
"Parser.Stream.error"
const
24
ref
constTerm
209
def
appTerm
210
def
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
211
def
appTerm
212
def
191
ref
209
ref
appTerm
appTerm
213
def
absTerm
214
def
appTerm
215
def
absTerm
216
def
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
61
ref
nil
72
ref
215
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
76
ref
214
remove
nil
cons
cons
nil
cons
nil
cons
cons
80
ref
subst
22
ref
nil
72
ref
213
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
212
ref
refl
217
def
nil
87
ref
209
ref
nil
cons
218
def
cons
nil
cons
nil
cons
cons
219
def
87
ref
49
ref
0
ref
29
ref
91
remove
cons
opType
constTerm
220
def
192
ref
appTerm
88
ref
0
ref
29
ref
0
ref
0
ref
8
ref
30
ref
cons
opType
221
def
0
ref
10
ref
30
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
"Data.Option.none"
const
222
def
29
ref
constTerm
223
def
appTerm
224
def
"y"
8
ref
var
225
def
"Data.Sum.case.left.right"
const
226
def
0
ref
0
ref
5
ref
30
ref
cons
opType
227
def
0
ref
0
ref
2
ref
30
ref
cons
opType
228
def
221
ref
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
229
def
"z"
5
ref
var
230
def
"Data.Option.some"
const
231
def
0
ref
27
ref
30
ref
cons
opType
constTerm
232
def
104
ref
230
ref
varTerm
233
def
appTerm
234
def
114
ref
appTerm
appTerm
absTerm
appTerm
"t"
2
ref
var
235
def
"Parser.Stream.case.error.eof.cons"
const
236
def
0
ref
29
ref
0
ref
29
ref
0
ref
33
ref
32
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
223
ref
appTerm
223
ref
appTerm
237
def
"z"
1
ref
var
238
def
"zs"
24
ref
var
239
def
39
ref
235
ref
varTerm
240
def
appTerm
238
ref
varTerm
241
def
appTerm
239
ref
varTerm
242
def
appTerm
243
def
absTerm
244
def
absTerm
245
def
appTerm
246
def
114
ref
appTerm
absTerm
appTerm
225
ref
varTerm
247
def
appTerm
absTerm
appTerm
38
ref
116
ref
appTerm
40
ref
appTerm
248
def
appTerm
appTerm
absTerm
249
def
114
ref
appTerm
250
def
betaConv
61
ref
86
ref
249
ref
appTerm
251
def
absTerm
252
def
116
ref
appTerm
253
def
betaConv
22
ref
55
ref
252
ref
appTerm
254
def
absTerm
255
def
40
ref
appTerm
256
def
betaConv
17
ref
21
ref
255
ref
appTerm
257
def
absTerm
258
def
38
ref
appTerm
259
def
betaConv
nil
18
ref
0
ref
15
remove
14
ref
cons
opType
constTerm
260
def
258
ref
appTerm
261
def
axiom
nil
121
ref
261
remove
nil
cons
cons
122
ref
259
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
46
ref
16
ref
258
remove
nil
cons
cons
"x"
12
ref
var
38
ref
nil
cons
cons
nil
cons
262
def
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
257
remove
nil
cons
cons
122
ref
256
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
78
ref
76
ref
255
remove
nil
cons
cons
"x"
2
ref
var
263
def
40
ref
nil
cons
cons
nil
cons
264
def
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
254
remove
nil
cons
cons
122
ref
253
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
"A"
23
ref
cons
265
def
nil
cons
266
def
56
ref
252
remove
nil
cons
cons
61
ref
116
ref
nil
cons
cons
nil
cons
267
def
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
251
remove
nil
cons
cons
122
ref
250
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
198
ref
196
ref
249
remove
nil
cons
cons
"x"
24
ref
var
268
def
114
ref
nil
cons
cons
nil
cons
269
def
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
270
def
subst
appThm
sym
"x"
10
ref
var
271
def
"Data.Bool.\\/"
const
51
remove
constTerm
272
def
49
ref
0
ref
10
ref
0
ref
10
ref
14
ref
cons
opType
273
def
nil
cons
cons
opType
constTerm
274
def
271
ref
varTerm
appTerm
275
def
222
ref
10
ref
constTerm
276
def
appTerm
appTerm
"Data.Bool.?"
const
277
def
0
ref
0
ref
8
ref
14
ref
cons
opType
278
def
14
ref
cons
opType
279
def
constTerm
280
def
"a"
8
ref
var
281
def
275
remove
231
ref
0
ref
8
ref
11
ref
cons
opType
constTerm
282
def
281
ref
varTerm
appTerm
283
def
appTerm
absTerm
appTerm
appTerm
absTerm
284
def
248
ref
appTerm
285
def
betaConv
"A"
9
ref
cons
286
def
nil
cons
287
def
47
ref
cons
288
def
nil
18
ref
0
ref
0
ref
3
remove
23
ref
opType
289
def
14
ref
cons
opType
290
def
14
ref
cons
opType
constTerm
"x"
289
ref
var
291
def
272
ref
49
ref
0
ref
289
ref
290
remove
nil
cons
cons
opType
constTerm
291
remove
varTerm
appTerm
292
def
222
remove
289
ref
constTerm
293
def
appTerm
appTerm
277
ref
54
ref
constTerm
294
def
"a"
1
ref
var
295
def
292
remove
231
remove
0
ref
1
ref
289
ref
nil
cons
cons
opType
constTerm
295
ref
varTerm
296
def
appTerm
297
def
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
axiom
298
def
subst
nil
121
ref
18
ref
0
ref
273
ref
14
ref
cons
opType
constTerm
284
ref
appTerm
nil
cons
cons
122
ref
285
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
"A"
11
remove
cons
nil
cons
"P"
273
remove
var
284
remove
nil
cons
cons
271
remove
248
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
299
def
nil
121
ref
272
ref
274
remove
248
ref
appTerm
300
def
276
ref
appTerm
301
def
appTerm
280
remove
281
ref
300
ref
283
remove
appTerm
absTerm
302
def
appTerm
303
def
appTerm
nil
cons
304
def
cons
305
def
122
ref
212
ref
224
ref
225
ref
229
ref
230
ref
232
ref
234
ref
209
ref
appTerm
306
def
appTerm
absTerm
307
def
appTerm
235
ref
246
ref
209
ref
appTerm
absTerm
308
def
appTerm
309
def
247
ref
appTerm
310
def
absTerm
311
def
appTerm
312
def
248
ref
appTerm
appTerm
313
def
nil
cons
314
def
cons
nil
cons
315
def
cons
nil
cons
cons
316
def
180
ref
subst
proveHyp
316
ref
140
ref
subst
316
remove
188
ref
subst
nil
"P"
278
ref
var
317
def
225
ref
123
ref
302
ref
247
ref
appTerm
318
def
appTerm
319
def
313
ref
appTerm
320
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
288
remove
70
ref
subst
321
def
subst
225
ref
nil
72
ref
320
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
121
ref
318
ref
nil
cons
322
def
cons
323
def
315
ref
cons
nil
cons
cons
324
def
140
ref
subst
324
remove
188
ref
subst
318
ref
betaConv
318
remove
assume
eqMp
325
def
nil
121
ref
300
remove
282
remove
247
ref
appTerm
326
def
appTerm
327
def
nil
cons
328
def
cons
329
def
315
ref
cons
nil
cons
cons
330
def
180
ref
subst
proveHyp
330
ref
140
ref
subst
330
remove
188
ref
subst
52
ref
"_32059"
10
ref
var
331
def
212
ref
312
ref
331
remove
varTerm
appTerm
appTerm
absTerm
332
def
248
ref
appTerm
333
def
appTerm
refl
334
def
332
ref
326
ref
appTerm
betaConv
appThm
160
ref
333
remove
betaConv
appThm
335
def
212
ref
312
ref
326
ref
appTerm
appTerm
refl
appThm
trans
332
remove
refl
336
def
327
remove
assume
337
def
appThm
eqMp
sym
217
ref
nil
281
remove
247
ref
nil
cons
338
def
cons
339
def
"f"
221
remove
var
340
def
311
ref
nil
cons
cons
"b"
29
ref
var
223
ref
nil
cons
341
def
cons
342
def
nil
cons
343
def
cons
344
def
cons
nil
cons
cons
286
remove
"B"
30
ref
cons
nil
cons
345
def
cons
47
ref
cons
346
def
295
ref
49
ref
0
ref
5
ref
98
ref
nil
cons
cons
opType
constTerm
347
def
88
remove
0
ref
5
ref
0
ref
0
ref
1
ref
5
ref
nil
cons
348
def
cons
349
def
opType
350
def
0
ref
289
remove
348
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
"b"
5
ref
var
351
def
varTerm
352
def
appTerm
"f"
350
ref
var
353
def
varTerm
354
def
appTerm
355
def
297
remove
appTerm
appTerm
354
ref
296
ref
appTerm
appTerm
absTerm
356
def
296
ref
appTerm
357
def
betaConv
353
ref
55
ref
356
ref
appTerm
358
def
absTerm
359
def
354
ref
appTerm
360
def
betaConv
351
ref
18
ref
0
ref
0
ref
350
ref
14
ref
cons
opType
361
def
14
ref
cons
opType
constTerm
362
def
359
ref
appTerm
363
def
absTerm
364
def
352
ref
appTerm
365
def
betaConv
nil
100
ref
364
ref
appTerm
366
def
axiom
nil
121
ref
366
remove
nil
cons
cons
122
ref
365
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
"A"
348
ref
cons
367
def
nil
cons
368
def
"P"
98
remove
var
369
def
364
remove
nil
cons
cons
"x"
5
ref
var
370
def
352
ref
nil
cons
cons
nil
cons
371
def
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
363
remove
nil
cons
cons
122
ref
360
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
"A"
350
ref
nil
cons
cons
nil
cons
372
def
"P"
361
ref
var
373
def
359
remove
nil
cons
cons
"x"
350
ref
var
374
def
354
ref
nil
cons
cons
nil
cons
375
def
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
358
remove
nil
cons
cons
122
ref
357
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
266
ref
56
ref
356
remove
nil
cons
cons
61
ref
296
ref
nil
cons
cons
nil
cons
376
def
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
377
def
subst
378
def
subst
311
remove
247
ref
appTerm
betaConv
trans
appThm
sym
"x"
8
ref
var
379
def
272
ref
277
ref
99
remove
constTerm
380
def
"a"
5
ref
var
381
def
49
ref
0
ref
8
ref
278
remove
nil
cons
cons
opType
constTerm
382
def
379
ref
varTerm
383
def
appTerm
384
def
"Data.Sum.left"
const
385
def
0
ref
5
ref
9
ref
cons
opType
constTerm
386
def
381
ref
varTerm
387
def
appTerm
388
def
appTerm
absTerm
appTerm
appTerm
277
ref
20
remove
constTerm
389
def
"b"
2
ref
var
390
def
384
remove
"Data.Sum.right"
const
391
def
0
ref
2
ref
9
remove
cons
opType
constTerm
392
def
390
ref
varTerm
appTerm
393
def
appTerm
absTerm
appTerm
appTerm
absTerm
394
def
247
ref
appTerm
395
def
betaConv
367
ref
"B"
6
ref
cons
396
def
nil
cons
cons
47
ref
cons
nil
18
ref
0
ref
0
ref
4
remove
349
ref
opType
397
def
14
ref
cons
opType
398
def
14
ref
cons
opType
constTerm
"x"
397
ref
var
399
def
272
ref
294
ref
295
ref
49
ref
0
ref
397
ref
398
remove
nil
cons
cons
opType
constTerm
399
remove
varTerm
appTerm
400
def
385
remove
0
ref
1
ref
397
ref
nil
cons
401
def
cons
opType
constTerm
296
ref
appTerm
402
def
appTerm
absTerm
appTerm
appTerm
380
ref
351
ref
400
remove
391
remove
0
ref
5
ref
401
remove
cons
opType
constTerm
352
ref
appTerm
403
def
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
axiom
subst
nil
121
ref
18
ref
279
remove
constTerm
404
def
394
ref
appTerm
nil
cons
cons
122
ref
395
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
287
ref
317
ref
394
remove
nil
cons
cons
379
ref
338
remove
cons
nil
cons
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
405
def
nil
121
ref
272
ref
380
ref
381
ref
382
remove
247
ref
appTerm
406
def
388
remove
appTerm
absTerm
407
def
appTerm
408
def
appTerm
389
remove
390
ref
406
ref
393
remove
appTerm
absTerm
409
def
appTerm
410
def
appTerm
nil
cons
411
def
cons
412
def
122
ref
212
ref
310
remove
appTerm
413
def
nil
cons
414
def
cons
nil
cons
415
def
cons
nil
cons
cons
416
def
180
ref
subst
proveHyp
416
ref
140
ref
subst
416
remove
188
ref
subst
nil
76
ref
235
ref
123
ref
409
ref
240
ref
appTerm
417
def
appTerm
418
def
413
ref
appTerm
419
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
80
ref
subst
235
ref
nil
72
ref
419
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
121
ref
417
ref
nil
cons
420
def
cons
421
def
415
ref
cons
nil
cons
cons
422
def
140
ref
subst
422
remove
188
ref
subst
417
ref
betaConv
417
remove
assume
eqMp
423
def
nil
121
ref
406
ref
392
remove
240
ref
appTerm
424
def
appTerm
425
def
nil
cons
426
def
cons
427
def
415
ref
cons
nil
cons
cons
428
def
180
ref
subst
proveHyp
428
ref
140
ref
subst
428
remove
188
ref
subst
52
ref
"_32063"
8
ref
var
429
def
212
ref
309
ref
429
remove
varTerm
appTerm
appTerm
absTerm
430
def
247
ref
appTerm
431
def
appTerm
refl
432
def
430
ref
424
ref
appTerm
betaConv
appThm
160
ref
431
remove
betaConv
appThm
433
def
212
ref
309
ref
424
ref
appTerm
appTerm
refl
appThm
trans
430
remove
refl
434
def
425
remove
assume
435
def
appThm
eqMp
sym
217
ref
nil
390
remove
240
ref
nil
cons
436
def
cons
437
def
"g"
228
remove
var
438
def
308
ref
nil
cons
cons
"f"
227
remove
var
439
def
307
ref
nil
cons
cons
nil
cons
cons
440
def
cons
nil
cons
cons
367
ref
396
remove
"C"
30
ref
cons
nil
cons
cons
cons
47
ref
cons
441
def
351
ref
49
ref
0
ref
2
ref
19
remove
nil
cons
cons
opType
constTerm
442
def
226
remove
0
ref
0
ref
1
ref
6
ref
cons
opType
443
def
0
ref
0
ref
7
remove
opType
444
def
0
ref
397
remove
6
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
"f"
443
ref
var
445
def
varTerm
446
def
appTerm
"g"
444
ref
var
447
def
varTerm
448
def
appTerm
449
def
403
remove
appTerm
appTerm
448
ref
352
ref
appTerm
appTerm
absTerm
450
def
352
ref
appTerm
451
def
betaConv
447
ref
100
ref
450
ref
appTerm
452
def
absTerm
453
def
448
ref
appTerm
454
def
betaConv
445
ref
18
ref
0
ref
0
ref
444
ref
14
ref
cons
opType
455
def
14
ref
cons
opType
constTerm
456
def
453
ref
appTerm
457
def
absTerm
458
def
446
ref
appTerm
459
def
betaConv
nil
18
ref
0
ref
0
ref
443
ref
14
ref
cons
opType
460
def
14
ref
cons
opType
constTerm
461
def
458
ref
appTerm
462
def
axiom
nil
121
ref
462
remove
nil
cons
cons
122
ref
459
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
"A"
443
ref
nil
cons
463
def
cons
nil
cons
464
def
"P"
460
remove
var
465
def
458
remove
nil
cons
cons
"x"
443
remove
var
446
ref
nil
cons
cons
nil
cons
466
def
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
457
remove
nil
cons
cons
122
ref
454
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
"A"
444
ref
nil
cons
467
def
cons
nil
cons
468
def
"P"
455
remove
var
469
def
453
remove
nil
cons
cons
"x"
444
ref
var
470
def
448
ref
nil
cons
cons
nil
cons
471
def
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
452
remove
nil
cons
cons
122
ref
451
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
368
ref
369
ref
450
remove
nil
cons
cons
371
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
472
def
subst
308
remove
240
ref
appTerm
betaConv
nil
"f"
33
ref
var
473
def
245
ref
nil
cons
cons
342
remove
"e"
29
ref
var
341
ref
cons
nil
cons
cons
474
def
cons
475
def
nil
cons
cons
476
def
265
ref
345
ref
cons
47
ref
cons
477
def
"f"
0
ref
1
ref
0
ref
24
ref
348
ref
cons
opType
nil
cons
478
def
cons
opType
479
def
var
480
def
347
ref
236
remove
0
ref
5
ref
0
ref
5
ref
0
ref
479
ref
478
remove
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
"e"
5
ref
var
481
def
varTerm
482
def
appTerm
352
ref
appTerm
480
ref
varTerm
483
def
appTerm
484
def
209
ref
appTerm
appTerm
482
ref
appTerm
absTerm
485
def
483
ref
appTerm
486
def
betaConv
351
ref
18
ref
0
ref
0
ref
479
ref
14
ref
cons
opType
487
def
14
ref
cons
opType
constTerm
488
def
485
ref
appTerm
489
def
absTerm
490
def
352
ref
appTerm
491
def
betaConv
481
ref
100
ref
490
ref
appTerm
492
def
absTerm
493
def
482
ref
appTerm
494
def
betaConv
nil
129
ref
100
ref
493
ref
appTerm
495
def
appTerm
129
ref
100
ref
481
ref
100
ref
351
ref
488
ref
480
ref
347
ref
484
ref
"Parser.Stream.eof"
const
24
ref
constTerm
496
def
appTerm
appTerm
352
ref
appTerm
absTerm
497
def
appTerm
498
def
absTerm
499
def
appTerm
500
def
absTerm
501
def
appTerm
502
def
appTerm
100
ref
481
remove
100
ref
351
ref
488
remove
480
remove
55
ref
61
ref
86
ref
87
ref
347
ref
484
remove
"Parser.Stream.cons"
const
0
ref
1
ref
0
ref
24
ref
26
ref
cons
opType
nil
cons
cons
opType
constTerm
503
def
116
ref
appTerm
504
def
114
ref
appTerm
505
def
appTerm
appTerm
483
ref
116
ref
appTerm
114
ref
appTerm
appTerm
absTerm
506
def
appTerm
507
def
absTerm
508
def
appTerm
509
def
absTerm
510
def
appTerm
511
def
absTerm
512
def
appTerm
513
def
absTerm
514
def
appTerm
515
def
appTerm
516
def
appTerm
axiom
517
def
nil
157
ref
495
remove
nil
cons
518
def
cons
158
ref
516
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
519
def
172
ref
subst
proveHyp
nil
121
ref
518
remove
cons
122
ref
494
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
368
ref
369
ref
493
remove
nil
cons
cons
370
ref
482
ref
nil
cons
cons
nil
cons
520
def
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
492
remove
nil
cons
cons
122
ref
491
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
368
ref
369
ref
490
remove
nil
cons
cons
371
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
489
remove
nil
cons
cons
122
ref
486
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
"A"
479
ref
nil
cons
cons
nil
cons
521
def
"P"
487
remove
var
522
def
485
remove
nil
cons
cons
"x"
479
remove
var
483
ref
nil
cons
cons
nil
cons
523
def
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
524
def
subst
trans
trans
appThm
nil
97
ref
211
remove
nil
cons
cons
"b"
13
ref
var
62
ref
nil
cons
525
def
cons
nil
cons
526
def
cons
527
def
nil
cons
cons
"A"
28
remove
cons
528
def
"B"
14
ref
cons
nil
cons
529
def
cons
47
ref
cons
530
def
353
ref
347
ref
355
remove
293
remove
appTerm
appTerm
352
ref
appTerm
absTerm
531
def
354
ref
appTerm
532
def
betaConv
351
ref
362
ref
531
ref
appTerm
533
def
absTerm
534
def
352
ref
appTerm
535
def
betaConv
nil
100
ref
534
ref
appTerm
536
def
axiom
nil
121
ref
536
remove
nil
cons
cons
122
ref
535
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
368
ref
369
ref
534
remove
nil
cons
cons
371
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
533
remove
nil
cons
cons
122
ref
532
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
372
ref
373
ref
531
remove
nil
cons
cons
375
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
537
def
subst
538
def
subst
539
def
trans
sym
74
ref
eqMp
eqMp
eqMp
nil
157
ref
426
remove
cons
540
def
158
ref
414
ref
cons
nil
cons
541
def
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
157
ref
420
remove
cons
542
def
541
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
121
ref
21
ref
263
ref
123
ref
409
ref
263
ref
varTerm
543
def
appTerm
appTerm
544
def
413
ref
appTerm
absTerm
appTerm
nil
cons
cons
122
ref
123
ref
410
ref
appTerm
545
def
413
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
78
ref
76
ref
409
remove
nil
cons
cons
546
def
541
ref
cons
nil
cons
cons
nil
121
ref
55
ref
61
ref
123
ref
185
ref
appTerm
547
def
163
ref
appTerm
548
def
absTerm
549
def
appTerm
550
def
nil
cons
551
def
cons
552
def
122
ref
123
ref
294
ref
57
ref
appTerm
553
def
appTerm
554
def
163
ref
appTerm
nil
cons
555
def
cons
nil
cons
cons
nil
cons
cons
556
def
140
ref
subst
556
remove
188
ref
subst
nil
121
ref
553
ref
nil
cons
557
def
cons
558
def
122
ref
163
ref
nil
cons
559
def
cons
nil
cons
560
def
cons
nil
cons
cons
561
def
140
ref
subst
561
remove
188
ref
subst
nil
552
ref
560
ref
cons
nil
cons
cons
562
def
180
ref
subst
122
ref
123
ref
55
ref
61
ref
547
remove
126
ref
appTerm
absTerm
appTerm
appTerm
126
ref
appTerm
absTerm
563
def
163
ref
appTerm
564
def
betaConv
nil
558
remove
122
ref
18
ref
147
remove
constTerm
565
def
563
ref
appTerm
566
def
nil
cons
567
def
cons
nil
cons
cons
nil
cons
cons
568
def
180
ref
subst
52
ref
553
remove
appTerm
569
def
refl
59
ref
565
ref
122
ref
123
ref
55
ref
61
ref
123
ref
60
ref
116
ref
appTerm
570
def
appTerm
571
def
126
ref
appTerm
absTerm
appTerm
appTerm
126
ref
appTerm
absTerm
appTerm
absTerm
572
def
57
remove
appTerm
betaConv
appThm
nil
67
remove
294
ref
appTerm
572
remove
appTerm
axiom
68
remove
appThm
eqMp
573
def
nil
121
ref
569
remove
566
ref
appTerm
nil
cons
cons
122
ref
554
remove
566
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
568
remove
nil
121
ref
52
ref
124
ref
appTerm
574
def
126
ref
appTerm
575
def
nil
cons
576
def
cons
577
def
122
ref
127
ref
nil
cons
578
def
cons
nil
cons
579
def
cons
nil
cons
cons
580
def
140
ref
subst
580
remove
188
ref
subst
140
ref
188
ref
575
remove
assume
581
def
153
remove
eqMp
eqMp
173
ref
deductAntisym
eqMp
582
def
eqMp
nil
157
ref
576
remove
cons
583
def
158
ref
578
ref
cons
nil
cons
584
def
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
585
def
subst
eqMp
eqMp
nil
121
ref
567
remove
cons
122
ref
564
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
"A"
14
ref
cons
nil
cons
586
def
"P"
50
remove
var
587
def
563
remove
nil
cons
cons
"x"
13
ref
var
588
def
559
ref
cons
nil
cons
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
157
ref
557
remove
cons
158
ref
559
remove
cons
nil
cons
589
def
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
nil
157
ref
551
ref
cons
590
def
158
ref
555
remove
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
591
def
subst
eqMp
nil
369
ref
230
ref
123
ref
407
ref
233
ref
appTerm
592
def
appTerm
593
def
413
ref
appTerm
594
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
368
ref
47
ref
cons
70
ref
subst
595
def
subst
230
ref
nil
72
ref
594
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
121
ref
592
ref
nil
cons
596
def
cons
597
def
415
ref
cons
nil
cons
cons
598
def
140
ref
subst
598
remove
188
ref
subst
592
ref
betaConv
592
remove
assume
eqMp
599
def
nil
121
ref
406
ref
386
ref
233
ref
appTerm
600
def
appTerm
601
def
nil
cons
602
def
cons
603
def
415
remove
cons
nil
cons
cons
604
def
180
ref
subst
proveHyp
604
ref
140
ref
subst
604
remove
188
ref
subst
432
remove
"_32061"
8
ref
var
605
def
212
ref
309
ref
605
remove
varTerm
appTerm
appTerm
absTerm
600
ref
appTerm
betaConv
appThm
433
remove
212
ref
309
remove
600
ref
appTerm
appTerm
refl
appThm
trans
434
remove
601
remove
assume
606
def
appThm
eqMp
sym
217
ref
nil
381
ref
233
ref
nil
cons
607
def
cons
608
def
440
remove
cons
nil
cons
cons
441
remove
295
ref
442
ref
449
remove
402
remove
appTerm
appTerm
446
ref
296
ref
appTerm
appTerm
absTerm
609
def
296
ref
appTerm
610
def
betaConv
447
remove
55
ref
609
ref
appTerm
611
def
absTerm
612
def
448
remove
appTerm
613
def
betaConv
445
remove
456
ref
612
ref
appTerm
614
def
absTerm
615
def
446
remove
appTerm
616
def
betaConv
nil
461
remove
615
ref
appTerm
617
def
axiom
nil
121
ref
617
remove
nil
cons
cons
122
ref
616
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
464
remove
465
remove
615
remove
nil
cons
cons
466
remove
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
614
remove
nil
cons
cons
122
ref
613
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
468
ref
469
ref
612
remove
nil
cons
cons
471
remove
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
611
remove
nil
cons
cons
122
ref
610
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
266
ref
56
ref
609
remove
nil
cons
cons
376
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
618
def
subst
307
remove
233
ref
appTerm
betaConv
trans
appThm
nil
"a"
27
ref
var
619
def
306
remove
nil
cons
cons
527
remove
cons
nil
cons
cons
530
remove
377
remove
subst
620
def
subst
nil
102
ref
218
remove
cons
101
ref
607
remove
cons
nil
cons
621
def
cons
nil
cons
cons
102
ref
52
ref
96
ref
"_32075"
89
ref
var
622
def
100
ref
101
ref
86
ref
102
ref
52
ref
622
remove
varTerm
108
ref
appTerm
appTerm
210
ref
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
623
def
appTerm
624
def
108
ref
appTerm
appTerm
210
ref
appTerm
absTerm
625
def
107
ref
appTerm
626
def
betaConv
101
ref
86
ref
625
ref
appTerm
627
def
absTerm
628
def
105
ref
appTerm
629
def
betaConv
623
ref
624
remove
appTerm
630
def
betaConv
623
ref
"_32073"
27
ref
var
631
def
112
ref
93
ref
0
ref
0
ref
0
ref
27
ref
26
ref
cons
opType
632
def
14
ref
cons
opType
632
ref
nil
cons
cons
opType
constTerm
"fn"
632
remove
var
633
def
100
ref
381
ref
86
ref
"b"
24
ref
var
634
def
49
ref
111
ref
constTerm
635
def
633
remove
varTerm
104
ref
387
remove
appTerm
634
ref
varTerm
636
def
appTerm
637
def
appTerm
appTerm
636
ref
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
638
def
631
remove
varTerm
appTerm
appTerm
209
ref
appTerm
absTerm
639
def
appTerm
betaConv
sym
nil
369
ref
101
ref
86
ref
102
ref
52
ref
639
ref
108
ref
appTerm
640
def
appTerm
210
remove
appTerm
641
def
absTerm
642
def
appTerm
643
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
595
ref
subst
101
ref
nil
72
ref
643
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
196
ref
642
remove
nil
cons
cons
nil
cons
nil
cons
cons
199
ref
subst
102
ref
nil
72
ref
641
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
640
remove
betaConv
52
ref
"_32070"
24
ref
var
644
def
112
ref
644
remove
varTerm
appTerm
209
ref
appTerm
absTerm
645
def
107
ref
appTerm
646
def
appTerm
refl
645
ref
638
ref
108
ref
appTerm
647
def
appTerm
betaConv
appThm
160
ref
646
remove
betaConv
appThm
112
ref
647
ref
appTerm
648
def
209
ref
appTerm
refl
appThm
trans
645
remove
refl
nil
634
ref
107
ref
nil
cons
649
def
cons
381
ref
105
ref
nil
cons
650
def
cons
nil
cons
cons
nil
cons
cons
367
remove
"B"
26
remove
cons
nil
cons
cons
47
ref
cons
651
def
351
ref
347
ref
93
ref
0
ref
0
ref
0
ref
25
remove
349
ref
opType
652
def
348
ref
cons
opType
653
def
14
ref
cons
opType
654
def
653
ref
nil
cons
655
def
cons
opType
constTerm
"fn"
653
remove
var
656
def
55
ref
295
ref
100
ref
351
ref
347
ref
656
ref
varTerm
103
remove
0
ref
1
ref
0
ref
5
ref
652
ref
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
296
ref
appTerm
352
ref
appTerm
657
def
appTerm
appTerm
658
def
352
ref
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
659
def
appTerm
660
def
657
ref
appTerm
appTerm
352
ref
appTerm
absTerm
661
def
352
ref
appTerm
662
def
betaConv
295
ref
100
ref
661
ref
appTerm
663
def
absTerm
664
def
296
ref
appTerm
665
def
betaConv
659
ref
660
remove
appTerm
666
def
betaConv
277
ref
0
ref
654
ref
14
ref
cons
opType
constTerm
667
def
refl
656
remove
55
ref
refl
668
def
295
ref
100
ref
refl
669
def
351
ref
658
remove
refl
295
ref
351
ref
352
ref
absTerm
670
def
absTerm
671
def
296
ref
appTerm
betaConv
352
ref
refl
672
def
appThm
670
remove
352
ref
appTerm
betaConv
trans
appThm
absThm
appThm
absThm
appThm
absThm
appThm
"C"
348
ref
cons
nil
cons
"_1343"
0
ref
1
ref
0
ref
5
ref
348
remove
cons
opType
nil
cons
cons
opType
var
671
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
"f"
0
ref
1
ref
467
remove
cons
opType
673
def
var
674
def
295
ref
351
ref
"_1343"
673
ref
var
varTerm
296
ref
appTerm
352
ref
appTerm
675
def
absTerm
676
def
absTerm
677
def
nil
cons
cons
nil
cons
nil
cons
cons
674
ref
277
ref
0
ref
0
ref
0
ref
652
ref
6
remove
cons
opType
678
def
14
ref
cons
opType
679
def
14
ref
cons
opType
680
def
constTerm
681
def
"fn"
678
ref
var
682
def
55
ref
295
ref
100
ref
351
ref
442
ref
682
ref
varTerm
683
def
657
ref
appTerm
appTerm
684
def
674
remove
varTerm
685
def
296
ref
appTerm
352
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
686
def
685
ref
appTerm
687
def
betaConv
nil
18
ref
0
ref
0
ref
673
ref
14
ref
cons
opType
688
def
14
ref
cons
opType
constTerm
686
ref
appTerm
689
def
axiom
nil
121
ref
689
remove
nil
cons
cons
122
ref
687
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
"A"
673
ref
nil
cons
cons
nil
cons
"P"
688
remove
var
686
remove
nil
cons
cons
"x"
673
remove
var
685
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
nil
121
ref
681
ref
682
ref
55
ref
295
ref
100
ref
351
ref
684
ref
677
remove
296
remove
appTerm
690
def
352
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
691
def
absTerm
692
def
appTerm
693
def
nil
cons
cons
122
ref
681
remove
682
ref
55
ref
295
ref
100
ref
351
ref
684
ref
675
remove
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
694
def
appTerm
695
def
nil
cons
696
def
cons
nil
cons
697
def
cons
nil
cons
cons
180
ref
subst
nil
"P"
679
remove
var
698
def
682
ref
123
ref
692
ref
683
ref
appTerm
699
def
appTerm
695
ref
appTerm
700
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
678
ref
nil
cons
cons
nil
cons
701
def
47
ref
cons
70
ref
subst
subst
682
remove
nil
72
ref
700
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
121
ref
699
ref
nil
cons
702
def
cons
697
ref
cons
nil
cons
cons
703
def
140
ref
subst
703
remove
188
ref
subst
699
ref
betaConv
699
remove
assume
eqMp
nil
121
ref
691
ref
nil
cons
704
def
cons
697
remove
cons
nil
cons
cons
705
def
180
ref
subst
proveHyp
705
ref
140
ref
subst
705
remove
188
ref
subst
694
ref
683
ref
appTerm
betaConv
sym
668
ref
295
ref
669
remove
351
ref
684
remove
refl
690
remove
betaConv
672
remove
appThm
676
remove
352
ref
appTerm
betaConv
trans
appThm
absThm
appThm
absThm
appThm
691
remove
assume
eqMp
eqMp
701
ref
698
ref
694
remove
nil
cons
cons
"x"
678
remove
var
706
def
683
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
573
remove
sym
nil
587
ref
158
ref
123
ref
550
ref
appTerm
707
def
163
ref
appTerm
708
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
586
ref
47
ref
cons
709
def
70
ref
subst
710
def
subst
158
ref
nil
72
ref
708
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
562
ref
140
ref
subst
562
remove
188
ref
subst
nil
121
ref
186
ref
cons
560
ref
cons
nil
cons
cons
711
def
180
ref
subst
712
def
549
ref
116
ref
appTerm
713
def
betaConv
nil
552
ref
122
ref
713
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
266
ref
56
ref
549
remove
nil
cons
cons
714
def
267
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
715
def
eqMp
eqMp
nil
590
ref
589
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
716
def
subst
proveHyp
eqMp
nil
157
ref
704
remove
cons
158
ref
696
remove
cons
nil
cons
717
def
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
157
ref
702
remove
cons
717
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
121
ref
18
ref
680
remove
constTerm
706
ref
123
ref
692
ref
706
remove
varTerm
appTerm
appTerm
695
ref
appTerm
absTerm
appTerm
nil
cons
cons
122
ref
123
ref
693
remove
appTerm
695
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
701
remove
698
remove
692
remove
nil
cons
cons
717
remove
cons
nil
cons
cons
591
ref
subst
eqMp
eqMp
proveHyp
subst
eqMp
nil
121
ref
667
remove
659
ref
appTerm
nil
cons
cons
122
ref
666
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
"A"
655
remove
cons
nil
cons
"p"
654
remove
var
659
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
121
ref
294
ref
60
ref
appTerm
718
def
nil
cons
719
def
cons
720
def
122
ref
52
ref
60
ref
93
remove
0
ref
53
ref
23
remove
cons
opType
constTerm
60
ref
appTerm
appTerm
721
def
appTerm
722
def
62
ref
appTerm
723
def
nil
cons
724
def
cons
nil
cons
725
def
cons
nil
cons
cons
726
def
140
ref
subst
726
remove
188
ref
subst
294
ref
refl
nil
"t"
53
ref
var
60
ref
nil
cons
727
def
cons
nil
cons
nil
cons
cons
265
remove
529
remove
cons
47
ref
cons
"t"
350
ref
var
728
def
49
ref
0
ref
350
ref
361
remove
nil
cons
cons
opType
constTerm
729
def
61
ref
728
remove
varTerm
730
def
116
ref
appTerm
absTerm
appTerm
730
ref
appTerm
absTerm
731
def
730
ref
appTerm
732
def
betaConv
nil
362
ref
731
ref
appTerm
733
def
axiom
nil
121
ref
733
remove
nil
cons
cons
122
ref
732
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
372
ref
373
ref
731
remove
nil
cons
cons
374
ref
730
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
subst
appThm
nil
72
ref
719
ref
cons
nil
cons
nil
cons
cons
734
def
75
ref
subst
718
ref
assume
eqMp
trans
sym
74
ref
eqMp
nil
121
ref
294
ref
61
ref
570
ref
absTerm
735
def
appTerm
nil
cons
cons
725
ref
cons
nil
cons
cons
180
ref
subst
proveHyp
nil
56
ref
727
ref
cons
158
ref
724
remove
cons
nil
cons
736
def
cons
nil
cons
cons
nil
552
remove
122
ref
123
ref
294
ref
61
ref
185
ref
absTerm
737
def
appTerm
738
def
appTerm
163
ref
appTerm
739
def
nil
cons
740
def
cons
nil
cons
741
def
cons
nil
cons
cons
742
def
582
remove
nil
121
ref
578
ref
cons
743
def
122
ref
123
ref
126
ref
appTerm
744
def
124
ref
appTerm
nil
cons
745
def
cons
nil
cons
746
def
cons
nil
cons
cons
188
ref
subst
proveHyp
744
ref
refl
581
remove
appThm
sym
nil
121
ref
154
ref
cons
747
def
122
ref
154
ref
cons
nil
cons
748
def
cons
nil
cons
cons
749
def
140
ref
subst
749
remove
188
ref
subst
155
remove
eqMp
nil
157
ref
154
remove
cons
159
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
750
def
eqMp
nil
747
ref
122
ref
152
ref
cons
nil
cons
751
def
cons
nil
cons
cons
180
ref
subst
nil
157
ref
578
remove
cons
752
def
158
ref
745
remove
cons
nil
cons
753
def
cons
nil
cons
cons
754
def
160
ref
164
remove
175
ref
appTerm
betaConv
175
remove
161
ref
appTerm
betaConv
166
ref
appThm
174
remove
163
ref
appTerm
betaConv
trans
trans
appThm
176
remove
appThm
171
remove
177
remove
appThm
eqMp
sym
74
ref
eqMp
755
def
subst
eqMp
180
ref
754
remove
172
ref
subst
eqMp
deductAntisym
deductAntisym
756
def
subst
742
ref
140
ref
subst
742
remove
188
ref
subst
nil
56
ref
61
ref
123
ref
737
ref
116
ref
appTerm
757
def
appTerm
163
ref
appTerm
758
def
absTerm
759
def
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
61
ref
nil
72
ref
758
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
121
ref
757
ref
nil
cons
760
def
cons
560
ref
cons
nil
cons
cons
761
def
140
ref
subst
761
remove
188
ref
subst
757
ref
betaConv
762
def
757
remove
assume
eqMp
712
remove
proveHyp
715
remove
eqMp
eqMp
nil
157
ref
760
remove
cons
589
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
121
ref
55
ref
759
remove
appTerm
nil
cons
cons
741
remove
cons
nil
cons
cons
180
ref
subst
proveHyp
266
ref
56
ref
737
remove
nil
cons
cons
763
def
589
ref
cons
nil
cons
cons
591
ref
subst
eqMp
eqMp
nil
590
remove
158
ref
740
ref
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
nil
121
ref
707
remove
739
ref
appTerm
nil
cons
cons
122
ref
123
ref
739
ref
appTerm
550
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
188
ref
subst
proveHyp
nil
121
ref
740
ref
cons
122
ref
551
ref
cons
nil
cons
cons
nil
cons
cons
764
def
140
ref
subst
764
remove
188
ref
subst
nil
714
remove
nil
cons
nil
cons
cons
70
ref
subst
61
ref
nil
72
ref
548
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
711
ref
140
ref
subst
711
remove
188
ref
subst
762
remove
sym
185
remove
assume
eqMp
266
ref
763
remove
267
ref
cons
nil
cons
cons
716
ref
subst
proveHyp
nil
121
ref
738
remove
nil
cons
cons
560
remove
cons
nil
cons
cons
180
ref
subst
739
remove
assume
eqMp
proveHyp
eqMp
nil
157
ref
186
remove
cons
589
remove
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
157
ref
740
remove
cons
158
ref
551
remove
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
subst
nil
56
ref
61
ref
571
ref
723
ref
appTerm
765
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
61
ref
nil
72
ref
765
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
121
ref
570
ref
nil
cons
766
def
cons
767
def
725
remove
cons
nil
cons
cons
768
def
140
ref
subst
768
remove
188
ref
subst
nil
72
ref
721
ref
nil
cons
769
def
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
767
remove
122
ref
769
remove
cons
770
def
nil
cons
cons
nil
cons
cons
180
ref
subst
61
ref
571
remove
721
ref
appTerm
absTerm
771
def
116
ref
appTerm
772
def
betaConv
59
ref
55
ref
771
ref
appTerm
773
def
absTerm
774
def
60
ref
appTerm
775
def
betaConv
nil
18
ref
66
remove
constTerm
776
def
774
ref
appTerm
777
def
axiom
nil
121
ref
777
remove
nil
cons
cons
122
ref
775
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
"A"
53
ref
nil
cons
778
def
cons
nil
cons
779
def
"P"
54
remove
var
780
def
774
remove
nil
cons
cons
"x"
53
ref
var
781
def
727
remove
cons
nil
cons
782
def
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
773
remove
nil
cons
cons
122
ref
772
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
266
ref
56
ref
771
remove
nil
cons
cons
267
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
eqMp
eqMp
eqMp
nil
157
ref
766
remove
cons
736
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
eqMp
eqMp
nil
157
ref
719
ref
cons
736
remove
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
nil
121
ref
123
ref
718
ref
appTerm
783
def
723
remove
appTerm
nil
cons
cons
122
ref
52
ref
783
ref
721
remove
appTerm
appTerm
784
def
783
ref
62
ref
appTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
nil
"q'"
13
ref
var
785
def
525
ref
cons
nil
cons
nil
cons
cons
718
ref
refl
nil
121
ref
52
ref
718
ref
appTerm
786
def
718
remove
appTerm
nil
cons
cons
122
ref
123
ref
783
ref
722
remove
785
ref
varTerm
787
def
appTerm
788
def
appTerm
appTerm
784
ref
783
remove
787
ref
appTerm
appTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
nil
"p'"
13
ref
var
789
def
719
remove
cons
nil
cons
nil
cons
cons
785
ref
123
ref
786
remove
789
ref
varTerm
790
def
appTerm
appTerm
123
ref
123
ref
790
ref
appTerm
791
def
788
remove
appTerm
appTerm
784
remove
791
ref
787
ref
appTerm
792
def
appTerm
appTerm
appTerm
absTerm
793
def
787
ref
appTerm
794
def
betaConv
789
ref
565
ref
793
ref
appTerm
795
def
absTerm
796
def
790
ref
appTerm
797
def
betaConv
nil
770
remove
720
remove
nil
cons
cons
nil
cons
cons
nil
587
ref
789
ref
565
ref
785
ref
123
ref
574
remove
790
ref
appTerm
798
def
appTerm
123
ref
791
ref
52
ref
126
ref
appTerm
787
ref
appTerm
799
def
appTerm
800
def
appTerm
128
remove
792
ref
appTerm
801
def
appTerm
802
def
appTerm
803
def
absTerm
804
def
appTerm
805
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
710
ref
subst
789
remove
nil
72
ref
805
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
587
ref
804
remove
nil
cons
cons
nil
cons
nil
cons
cons
710
remove
subst
785
remove
nil
72
ref
803
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
121
ref
798
remove
nil
cons
806
def
cons
807
def
122
ref
802
remove
nil
cons
808
def
cons
nil
cons
cons
nil
cons
cons
809
def
140
ref
subst
809
remove
188
ref
subst
nil
121
ref
800
ref
nil
cons
810
def
cons
122
ref
801
remove
nil
cons
811
def
cons
nil
cons
cons
nil
cons
cons
812
def
140
ref
subst
812
remove
188
ref
subst
nil
743
remove
122
ref
792
ref
nil
cons
813
def
cons
nil
cons
cons
nil
cons
cons
814
def
756
remove
subst
814
ref
140
ref
subst
814
remove
188
ref
subst
nil
121
ref
790
ref
nil
cons
815
def
cons
816
def
122
ref
787
ref
nil
cons
817
def
cons
nil
cons
818
def
cons
nil
cons
cons
819
def
140
ref
subst
819
ref
188
ref
subst
nil
807
ref
122
ref
125
ref
790
remove
appTerm
820
def
nil
cons
821
def
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
nil
121
ref
152
remove
cons
122
ref
815
ref
cons
nil
cons
cons
nil
cons
cons
822
def
585
ref
subst
eqMp
823
def
nil
121
ref
821
ref
cons
824
def
818
ref
cons
nil
cons
cons
825
def
180
ref
subst
proveHyp
nil
807
remove
122
ref
791
remove
124
remove
appTerm
826
def
nil
cons
827
def
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
822
ref
nil
577
remove
746
remove
cons
nil
cons
cons
828
def
140
ref
subst
828
remove
188
ref
subst
750
remove
eqMp
nil
583
remove
753
remove
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
829
def
subst
eqMp
830
def
nil
121
ref
827
ref
cons
831
def
122
ref
123
ref
820
ref
appTerm
832
def
787
ref
appTerm
nil
cons
833
def
cons
nil
cons
cons
nil
cons
cons
834
def
180
ref
subst
proveHyp
834
ref
140
ref
subst
834
remove
188
ref
subst
825
ref
140
ref
subst
825
remove
188
ref
subst
nil
816
ref
751
remove
cons
nil
cons
cons
180
ref
subst
826
remove
assume
eqMp
835
def
822
remove
180
ref
subst
820
remove
assume
eqMp
836
def
835
remove
proveHyp
proveHyp
nil
816
remove
122
ref
799
remove
nil
cons
837
def
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
800
remove
assume
eqMp
838
def
nil
121
ref
837
remove
cons
839
def
122
ref
744
ref
787
ref
appTerm
840
def
nil
cons
841
def
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
nil
747
remove
818
ref
cons
nil
cons
cons
842
def
585
remove
subst
eqMp
843
def
nil
121
ref
841
ref
cons
844
def
818
remove
cons
nil
cons
cons
845
def
180
ref
subst
proveHyp
838
remove
nil
839
remove
122
ref
123
ref
787
ref
appTerm
126
ref
appTerm
846
def
nil
cons
847
def
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
842
ref
829
remove
subst
eqMp
848
def
nil
121
ref
847
ref
cons
849
def
122
ref
123
ref
840
ref
appTerm
850
def
787
remove
appTerm
nil
cons
851
def
cons
nil
cons
cons
nil
cons
cons
852
def
180
ref
subst
proveHyp
852
ref
140
ref
subst
852
remove
188
ref
subst
845
ref
140
ref
subst
845
remove
188
ref
subst
179
remove
842
remove
180
ref
subst
840
remove
assume
eqMp
proveHyp
eqMp
nil
157
ref
841
remove
cons
853
def
158
ref
817
ref
cons
nil
cons
854
def
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
nil
157
ref
847
remove
cons
855
def
158
ref
851
remove
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
proveHyp
eqMp
nil
157
ref
821
remove
cons
856
def
854
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
nil
157
ref
827
remove
cons
857
def
158
ref
833
remove
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
157
ref
815
ref
cons
854
remove
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
nil
752
remove
158
ref
813
ref
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
nil
121
ref
123
ref
127
ref
appTerm
792
ref
appTerm
nil
cons
cons
122
ref
123
ref
792
ref
appTerm
127
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
188
ref
subst
proveHyp
nil
121
ref
813
ref
cons
579
remove
cons
nil
cons
cons
858
def
140
ref
subst
858
remove
188
ref
subst
140
ref
188
ref
823
remove
nil
824
remove
748
ref
cons
nil
cons
cons
859
def
180
ref
subst
proveHyp
830
remove
nil
831
remove
122
ref
832
remove
126
ref
appTerm
nil
cons
860
def
cons
nil
cons
cons
nil
cons
cons
861
def
180
ref
subst
proveHyp
861
ref
140
ref
subst
861
remove
188
ref
subst
859
ref
140
ref
subst
859
remove
188
ref
subst
836
remove
843
remove
nil
844
remove
748
ref
cons
nil
cons
cons
862
def
180
ref
subst
proveHyp
848
remove
nil
849
remove
122
ref
850
remove
126
remove
appTerm
nil
cons
863
def
cons
nil
cons
cons
nil
cons
cons
864
def
180
ref
subst
proveHyp
864
ref
140
ref
subst
864
remove
188
ref
subst
862
ref
140
ref
subst
862
remove
188
ref
subst
819
remove
180
ref
subst
792
remove
assume
eqMp
nil
121
ref
817
ref
cons
748
remove
cons
nil
cons
cons
180
ref
subst
846
remove
assume
eqMp
proveHyp
eqMp
nil
853
remove
159
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
nil
855
remove
158
ref
863
remove
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
proveHyp
eqMp
nil
856
remove
159
remove
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
nil
857
remove
158
ref
860
remove
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
173
remove
deductAntisym
eqMp
eqMp
nil
157
ref
813
remove
cons
584
remove
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
157
ref
810
remove
cons
158
ref
811
remove
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
nil
157
ref
806
remove
cons
158
ref
808
remove
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
subst
nil
121
ref
565
ref
796
ref
appTerm
nil
cons
cons
122
ref
797
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
586
ref
587
ref
796
remove
nil
cons
cons
588
ref
815
remove
cons
nil
cons
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
795
remove
nil
cons
cons
122
ref
794
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
586
ref
587
ref
793
remove
nil
cons
cons
588
ref
817
remove
cons
nil
cons
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
eqMp
subst
eqMp
734
remove
72
ref
52
ref
123
ref
73
ref
appTerm
62
ref
appTerm
appTerm
62
ref
appTerm
absTerm
865
def
73
ref
appTerm
866
def
betaConv
nil
565
ref
865
ref
appTerm
867
def
axiom
nil
121
ref
867
remove
nil
cons
cons
122
ref
866
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
586
ref
587
ref
865
remove
nil
cons
cons
588
ref
73
ref
nil
cons
cons
nil
cons
868
def
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
trans
sym
74
ref
eqMp
869
def
subst
eqMp
eqMp
nil
121
ref
55
ref
664
ref
appTerm
nil
cons
cons
122
ref
665
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
266
ref
56
ref
664
remove
nil
cons
cons
376
remove
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
663
remove
nil
cons
cons
122
ref
662
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
368
ref
369
ref
661
remove
nil
cons
cons
371
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
sym
subst
subst
870
def
appThm
eqMp
sym
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
"A"
95
ref
cons
nil
cons
871
def
"P"
94
ref
var
872
def
623
ref
nil
cons
873
def
cons
"x"
89
ref
var
874
def
639
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
716
ref
subst
proveHyp
nil
121
ref
277
ref
0
ref
94
ref
14
ref
cons
opType
constTerm
875
def
623
remove
appTerm
nil
cons
cons
122
ref
630
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
nil
"p"
94
ref
var
876
def
873
remove
cons
nil
cons
nil
cons
cons
871
ref
47
ref
cons
869
remove
subst
877
def
subst
eqMp
eqMp
nil
121
ref
100
ref
628
ref
appTerm
nil
cons
cons
122
ref
629
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
368
ref
369
ref
628
remove
nil
cons
cons
370
ref
650
remove
cons
nil
cons
878
def
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
627
remove
nil
cons
cons
122
ref
626
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
198
ref
196
ref
625
remove
nil
cons
cons
268
ref
649
ref
cons
nil
cons
879
def
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
219
remove
nil
72
ref
112
ref
114
ref
appTerm
880
def
114
ref
appTerm
881
def
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
87
ref
881
remove
absTerm
882
def
114
ref
appTerm
883
def
betaConv
nil
86
ref
882
ref
appTerm
884
def
axiom
nil
121
ref
884
remove
nil
cons
cons
122
ref
883
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
198
ref
196
ref
882
remove
nil
cons
cons
269
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
eqMp
885
def
subst
trans
trans
trans
sym
74
ref
eqMp
eqMp
eqMp
nil
157
ref
602
remove
cons
886
def
541
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
157
ref
596
remove
cons
887
def
541
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
121
ref
100
ref
370
ref
123
ref
407
ref
370
ref
varTerm
888
def
appTerm
appTerm
889
def
413
ref
appTerm
absTerm
appTerm
nil
cons
cons
122
ref
123
ref
408
ref
appTerm
890
def
413
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
368
ref
369
ref
407
ref
nil
cons
cons
891
def
541
ref
cons
nil
cons
cons
591
ref
subst
eqMp
nil
157
ref
408
remove
nil
cons
cons
892
def
158
ref
410
remove
nil
cons
cons
893
def
"R"
13
ref
var
894
def
414
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
121
ref
123
ref
163
ref
appTerm
895
def
894
ref
varTerm
896
def
appTerm
897
def
nil
cons
cons
122
ref
896
ref
nil
cons
898
def
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
nil
121
ref
123
ref
161
ref
appTerm
899
def
896
ref
appTerm
nil
cons
cons
122
ref
123
ref
897
remove
appTerm
896
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
"r"
13
ref
var
900
def
123
ref
899
remove
900
ref
varTerm
901
def
appTerm
appTerm
902
def
123
ref
895
remove
901
ref
appTerm
appTerm
901
ref
appTerm
appTerm
absTerm
903
def
896
remove
appTerm
904
def
betaConv
52
ref
272
ref
161
ref
appTerm
905
def
163
ref
appTerm
906
def
appTerm
refl
122
ref
565
ref
900
ref
902
remove
123
ref
744
remove
901
ref
appTerm
appTerm
901
ref
appTerm
907
def
appTerm
absTerm
appTerm
absTerm
163
remove
appTerm
betaConv
appThm
148
remove
905
remove
appTerm
refl
121
ref
122
ref
565
ref
900
remove
123
ref
125
remove
901
remove
appTerm
appTerm
907
remove
appTerm
absTerm
appTerm
absTerm
absTerm
908
def
161
remove
appTerm
betaConv
appThm
nil
137
remove
272
ref
appTerm
908
remove
appTerm
axiom
170
remove
appThm
eqMp
166
remove
appThm
eqMp
906
remove
assume
eqMp
nil
121
ref
565
ref
903
ref
appTerm
nil
cons
cons
122
ref
904
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
586
ref
587
ref
903
remove
nil
cons
cons
588
ref
898
remove
cons
nil
cons
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
eqMp
eqMp
909
def
subst
proveHyp
proveHyp
eqMp
nil
157
ref
411
remove
cons
910
def
541
remove
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
nil
157
ref
328
remove
cons
911
def
158
ref
314
ref
cons
nil
cons
912
def
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
157
ref
322
remove
cons
913
def
912
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
121
ref
404
ref
379
ref
123
ref
302
ref
383
remove
appTerm
appTerm
914
def
313
ref
appTerm
absTerm
appTerm
nil
cons
cons
122
ref
123
ref
303
ref
appTerm
915
def
313
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
287
ref
317
ref
302
remove
nil
cons
cons
916
def
912
ref
cons
nil
cons
cons
591
ref
subst
eqMp
nil
121
ref
301
ref
nil
cons
917
def
cons
918
def
315
remove
cons
nil
cons
cons
919
def
140
ref
subst
919
remove
188
ref
subst
334
remove
"_32057"
10
ref
var
920
def
212
ref
312
ref
920
remove
varTerm
appTerm
appTerm
absTerm
276
ref
appTerm
betaConv
appThm
335
remove
212
remove
312
remove
276
ref
appTerm
appTerm
refl
appThm
trans
336
remove
301
remove
assume
921
def
appThm
eqMp
sym
217
remove
nil
344
remove
nil
cons
cons
346
remove
537
remove
subst
922
def
subst
appThm
539
remove
trans
sym
74
ref
eqMp
eqMp
eqMp
nil
157
ref
917
remove
cons
923
def
912
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
nil
923
ref
158
ref
303
remove
nil
cons
cons
924
def
894
ref
314
remove
cons
nil
cons
cons
cons
nil
cons
cons
909
ref
subst
proveHyp
proveHyp
eqMp
nil
157
ref
304
remove
cons
925
def
912
remove
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
121
ref
55
ref
216
remove
appTerm
926
def
nil
cons
cons
122
ref
129
ref
55
ref
61
ref
21
ref
22
ref
92
ref
96
ref
97
ref
100
ref
101
ref
86
ref
102
ref
109
ref
113
ref
496
ref
appTerm
927
def
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
928
def
appTerm
929
def
191
ref
496
ref
appTerm
appTerm
930
def
absTerm
931
def
appTerm
932
def
absTerm
933
def
appTerm
934
def
appTerm
55
ref
61
ref
86
ref
87
ref
123
ref
205
ref
appTerm
935
def
55
ref
"x'"
1
ref
var
936
def
21
ref
22
ref
92
ref
96
ref
97
ref
100
ref
101
ref
86
ref
102
ref
109
ref
113
ref
505
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
41
ref
936
ref
varTerm
appTerm
937
def
505
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
938
def
appTerm
939
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
188
ref
subst
proveHyp
nil
56
ref
933
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
61
ref
nil
72
ref
932
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
76
ref
931
remove
nil
cons
cons
nil
cons
nil
cons
cons
80
ref
subst
22
ref
nil
72
ref
930
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
929
ref
refl
940
def
nil
87
ref
496
ref
nil
cons
941
def
cons
nil
cons
nil
cons
cons
942
def
270
ref
subst
appThm
sym
299
ref
nil
305
ref
122
ref
929
ref
224
ref
225
ref
229
ref
230
ref
232
ref
234
ref
496
ref
appTerm
943
def
appTerm
absTerm
944
def
appTerm
235
ref
246
ref
496
ref
appTerm
absTerm
945
def
appTerm
946
def
247
ref
appTerm
947
def
absTerm
948
def
appTerm
949
def
248
ref
appTerm
appTerm
950
def
nil
cons
951
def
cons
nil
cons
952
def
cons
nil
cons
cons
953
def
180
ref
subst
proveHyp
953
ref
140
ref
subst
953
remove
188
ref
subst
nil
317
ref
225
ref
319
ref
950
ref
appTerm
954
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
321
ref
subst
225
ref
nil
72
ref
954
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
323
ref
952
ref
cons
nil
cons
cons
955
def
140
ref
subst
955
remove
188
ref
subst
325
ref
nil
329
ref
952
ref
cons
nil
cons
cons
956
def
180
ref
subst
proveHyp
956
ref
140
ref
subst
956
remove
188
ref
subst
52
ref
"_32079"
10
ref
var
957
def
929
ref
949
ref
957
remove
varTerm
appTerm
appTerm
absTerm
958
def
248
ref
appTerm
959
def
appTerm
refl
960
def
958
ref
326
ref
appTerm
betaConv
appThm
160
ref
959
remove
betaConv
appThm
961
def
929
ref
949
ref
326
ref
appTerm
appTerm
refl
appThm
trans
958
remove
refl
962
def
337
ref
appThm
eqMp
sym
940
ref
nil
339
ref
340
ref
948
ref
nil
cons
cons
343
ref
cons
963
def
cons
nil
cons
cons
378
ref
subst
948
remove
247
ref
appTerm
betaConv
trans
appThm
sym
405
ref
nil
412
ref
122
ref
929
ref
947
remove
appTerm
964
def
nil
cons
965
def
cons
nil
cons
966
def
cons
nil
cons
cons
967
def
180
ref
subst
proveHyp
967
ref
140
ref
subst
967
remove
188
ref
subst
nil
76
ref
235
ref
418
ref
964
ref
appTerm
968
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
80
ref
subst
235
ref
nil
72
ref
968
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
421
ref
966
ref
cons
nil
cons
cons
969
def
140
ref
subst
969
remove
188
ref
subst
423
ref
nil
427
ref
966
ref
cons
nil
cons
cons
970
def
180
ref
subst
proveHyp
970
ref
140
ref
subst
970
remove
188
ref
subst
52
ref
"_32083"
8
ref
var
971
def
929
ref
946
ref
971
remove
varTerm
appTerm
appTerm
absTerm
972
def
247
ref
appTerm
973
def
appTerm
refl
974
def
972
ref
424
ref
appTerm
betaConv
appThm
160
ref
973
remove
betaConv
appThm
975
def
929
ref
946
ref
424
ref
appTerm
appTerm
refl
appThm
trans
972
remove
refl
976
def
435
ref
appThm
eqMp
sym
940
ref
nil
437
ref
438
ref
945
ref
nil
cons
cons
439
ref
944
ref
nil
cons
cons
nil
cons
cons
977
def
cons
nil
cons
cons
472
ref
subst
945
remove
240
ref
appTerm
betaConv
476
remove
477
ref
497
ref
483
ref
appTerm
978
def
betaConv
499
ref
352
ref
appTerm
979
def
betaConv
501
ref
482
ref
appTerm
980
def
betaConv
517
remove
519
remove
755
ref
subst
proveHyp
981
def
nil
157
ref
502
remove
nil
cons
982
def
cons
158
ref
515
remove
nil
cons
983
def
cons
nil
cons
cons
nil
cons
cons
984
def
172
ref
subst
proveHyp
nil
121
ref
982
remove
cons
122
ref
980
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
368
ref
369
ref
501
remove
nil
cons
cons
520
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
500
remove
nil
cons
cons
122
ref
979
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
368
ref
369
ref
499
remove
nil
cons
cons
371
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
498
remove
nil
cons
cons
122
ref
978
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
521
ref
522
ref
497
remove
nil
cons
cons
523
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
985
def
subst
trans
trans
appThm
nil
97
ref
928
remove
nil
cons
cons
526
ref
cons
986
def
nil
cons
cons
538
ref
subst
987
def
trans
sym
74
ref
eqMp
eqMp
eqMp
nil
540
ref
158
ref
965
ref
cons
nil
cons
988
def
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
542
ref
988
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
121
ref
21
ref
263
ref
544
ref
964
ref
appTerm
absTerm
appTerm
nil
cons
cons
122
ref
545
ref
964
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
78
ref
546
ref
988
ref
cons
nil
cons
cons
591
ref
subst
eqMp
nil
369
ref
230
ref
593
remove
964
ref
appTerm
989
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
595
ref
subst
230
ref
nil
72
ref
989
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
597
remove
966
ref
cons
nil
cons
cons
990
def
140
ref
subst
990
remove
188
ref
subst
599
remove
nil
603
remove
966
remove
cons
nil
cons
cons
991
def
180
ref
subst
proveHyp
991
ref
140
ref
subst
991
remove
188
ref
subst
974
remove
"_32081"
8
ref
var
992
def
929
ref
946
ref
992
remove
varTerm
appTerm
appTerm
absTerm
600
ref
appTerm
betaConv
appThm
975
remove
929
ref
946
remove
600
remove
appTerm
appTerm
refl
appThm
trans
976
remove
606
remove
appThm
eqMp
sym
940
ref
nil
608
remove
977
remove
cons
nil
cons
cons
618
ref
subst
944
remove
233
remove
appTerm
betaConv
trans
appThm
nil
619
ref
943
remove
nil
cons
cons
986
remove
cons
nil
cons
cons
620
ref
subst
nil
102
ref
941
remove
cons
621
remove
cons
nil
cons
cons
102
ref
52
ref
96
ref
"_32095"
89
ref
var
993
def
100
ref
101
ref
86
ref
102
ref
52
ref
993
remove
varTerm
108
ref
appTerm
appTerm
927
ref
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
994
def
appTerm
995
def
108
ref
appTerm
appTerm
927
ref
appTerm
absTerm
996
def
107
ref
appTerm
997
def
betaConv
101
ref
86
ref
996
ref
appTerm
998
def
absTerm
999
def
105
ref
appTerm
1000
def
betaConv
994
ref
995
remove
appTerm
1001
def
betaConv
994
ref
"_32093"
27
ref
var
1002
def
112
ref
638
ref
1002
remove
varTerm
appTerm
appTerm
496
ref
appTerm
absTerm
1003
def
appTerm
betaConv
sym
nil
369
ref
101
ref
86
ref
102
ref
52
ref
1003
ref
108
ref
appTerm
1004
def
appTerm
927
remove
appTerm
1005
def
absTerm
1006
def
appTerm
1007
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
595
ref
subst
101
ref
nil
72
ref
1007
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
196
ref
1006
remove
nil
cons
cons
nil
cons
nil
cons
cons
199
ref
subst
102
ref
nil
72
ref
1005
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
1004
remove
betaConv
52
ref
"_32090"
24
ref
var
1008
def
112
ref
1008
remove
varTerm
appTerm
496
ref
appTerm
absTerm
1009
def
107
ref
appTerm
1010
def
appTerm
refl
1009
ref
647
ref
appTerm
betaConv
appThm
160
ref
1010
remove
betaConv
appThm
648
ref
496
ref
appTerm
refl
appThm
trans
1009
remove
refl
870
ref
appThm
eqMp
sym
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
871
ref
872
ref
994
ref
nil
cons
1011
def
cons
874
ref
1003
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
716
ref
subst
proveHyp
nil
121
ref
875
ref
994
remove
appTerm
nil
cons
cons
122
ref
1001
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
nil
876
ref
1011
remove
cons
nil
cons
nil
cons
cons
877
ref
subst
eqMp
eqMp
nil
121
ref
100
ref
999
ref
appTerm
nil
cons
cons
122
ref
1000
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
368
ref
369
ref
999
remove
nil
cons
cons
878
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
998
remove
nil
cons
cons
122
ref
997
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
198
ref
196
ref
996
remove
nil
cons
cons
879
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
942
remove
885
ref
subst
trans
trans
trans
sym
74
ref
eqMp
eqMp
eqMp
nil
886
remove
988
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
887
remove
988
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
121
ref
100
ref
370
ref
889
ref
964
ref
appTerm
absTerm
appTerm
nil
cons
cons
122
ref
890
ref
964
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
368
ref
891
ref
988
ref
cons
nil
cons
cons
591
ref
subst
eqMp
nil
892
ref
893
ref
894
ref
965
remove
cons
nil
cons
cons
cons
nil
cons
cons
909
ref
subst
proveHyp
proveHyp
eqMp
nil
910
ref
988
remove
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
nil
911
ref
158
ref
951
ref
cons
nil
cons
1012
def
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
913
ref
1012
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
121
ref
404
ref
379
ref
914
ref
950
ref
appTerm
absTerm
appTerm
nil
cons
cons
122
ref
915
ref
950
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
287
ref
916
ref
1012
ref
cons
nil
cons
cons
591
ref
subst
eqMp
nil
918
ref
952
remove
cons
nil
cons
cons
1013
def
140
ref
subst
1013
remove
188
ref
subst
960
remove
"_32077"
10
ref
var
1014
def
929
ref
949
ref
1014
remove
varTerm
appTerm
appTerm
absTerm
276
ref
appTerm
betaConv
appThm
961
remove
929
remove
949
remove
276
ref
appTerm
appTerm
refl
appThm
trans
962
remove
921
ref
appThm
eqMp
sym
940
remove
nil
963
remove
nil
cons
cons
922
ref
subst
appThm
987
remove
trans
sym
74
ref
eqMp
eqMp
eqMp
nil
923
ref
1012
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
nil
923
ref
924
ref
894
ref
951
remove
cons
nil
cons
cons
cons
nil
cons
cons
909
ref
subst
proveHyp
proveHyp
eqMp
nil
925
ref
1012
remove
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
121
ref
934
remove
nil
cons
cons
122
ref
938
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
188
ref
subst
proveHyp
nil
56
ref
238
ref
86
ref
87
ref
935
remove
55
ref
936
ref
21
ref
22
ref
92
ref
96
ref
97
ref
100
ref
101
ref
86
ref
102
ref
109
ref
113
ref
503
ref
241
ref
appTerm
1015
def
114
ref
appTerm
1016
def
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
937
ref
1016
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
1017
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
238
remove
nil
72
ref
1017
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
196
ref
239
ref
123
ref
55
ref
61
ref
21
ref
22
ref
92
ref
96
ref
97
ref
100
ref
101
ref
86
ref
102
ref
109
ref
113
ref
242
ref
appTerm
1018
def
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
1019
def
appTerm
1020
def
191
ref
242
ref
appTerm
appTerm
absTerm
appTerm
absTerm
1021
def
appTerm
1022
def
appTerm
55
ref
936
remove
21
ref
22
ref
92
remove
96
ref
97
ref
100
ref
101
ref
86
ref
102
ref
109
remove
113
remove
1015
remove
242
ref
appTerm
1023
def
appTerm
1024
def
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
1025
def
appTerm
1026
def
937
remove
1023
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
1027
def
appTerm
1028
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
199
ref
subst
239
remove
nil
72
ref
1028
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
121
ref
1022
remove
nil
cons
1029
def
cons
1030
def
122
ref
1027
remove
nil
cons
1031
def
cons
nil
cons
cons
nil
cons
cons
1032
def
140
ref
subst
1032
remove
188
ref
subst
nil
56
ref
61
ref
21
ref
22
ref
1026
ref
191
ref
1023
ref
appTerm
appTerm
1033
def
absTerm
1034
def
appTerm
1035
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
61
ref
nil
72
ref
1035
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
76
ref
1034
remove
nil
cons
cons
nil
cons
nil
cons
cons
80
ref
subst
22
ref
nil
72
ref
1033
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
1026
ref
refl
1036
def
nil
87
ref
1023
ref
nil
cons
1037
def
cons
nil
cons
nil
cons
cons
1038
def
270
remove
subst
appThm
sym
299
remove
nil
305
remove
122
ref
1026
ref
224
remove
225
ref
229
remove
230
remove
232
ref
234
remove
1023
ref
appTerm
appTerm
absTerm
1039
def
appTerm
235
ref
246
remove
1023
ref
appTerm
absTerm
1040
def
appTerm
1041
def
247
ref
appTerm
1042
def
absTerm
1043
def
appTerm
1044
def
248
ref
appTerm
appTerm
1045
def
nil
cons
1046
def
cons
nil
cons
1047
def
cons
nil
cons
cons
1048
def
180
ref
subst
proveHyp
1048
ref
140
ref
subst
1048
remove
188
ref
subst
nil
317
remove
225
ref
319
remove
1045
ref
appTerm
1049
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
321
remove
subst
225
remove
nil
72
ref
1049
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
323
remove
1047
ref
cons
nil
cons
cons
1050
def
140
ref
subst
1050
remove
188
ref
subst
325
remove
nil
329
remove
1047
ref
cons
nil
cons
cons
1051
def
180
ref
subst
proveHyp
1051
ref
140
ref
subst
1051
remove
188
ref
subst
52
ref
"_32099"
10
ref
var
1052
def
1026
ref
1044
ref
1052
remove
varTerm
appTerm
appTerm
absTerm
1053
def
248
remove
appTerm
1054
def
appTerm
refl
1055
def
1053
ref
326
ref
appTerm
betaConv
appThm
160
ref
1054
remove
betaConv
appThm
1056
def
1026
ref
1044
ref
326
remove
appTerm
appTerm
refl
appThm
trans
1053
remove
refl
1057
def
337
remove
appThm
eqMp
sym
1036
ref
nil
339
remove
340
remove
1043
ref
nil
cons
cons
343
remove
cons
1058
def
cons
nil
cons
cons
378
remove
subst
1043
remove
247
ref
appTerm
betaConv
trans
appThm
sym
405
remove
nil
412
remove
122
ref
1026
ref
1042
remove
appTerm
1059
def
nil
cons
1060
def
cons
nil
cons
1061
def
cons
nil
cons
cons
1062
def
180
ref
subst
proveHyp
1062
ref
140
ref
subst
1062
remove
188
ref
subst
nil
76
ref
235
ref
418
remove
1059
ref
appTerm
1063
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
80
ref
subst
235
remove
nil
72
ref
1063
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
421
remove
1061
ref
cons
nil
cons
cons
1064
def
140
ref
subst
1064
remove
188
ref
subst
423
remove
nil
427
remove
1061
ref
cons
nil
cons
cons
1065
def
180
ref
subst
proveHyp
1065
ref
140
ref
subst
1065
remove
188
ref
subst
52
ref
"_32103"
8
ref
var
1066
def
1026
ref
1041
ref
1066
remove
varTerm
appTerm
appTerm
absTerm
1067
def
247
remove
appTerm
1068
def
appTerm
refl
1069
def
1067
ref
424
ref
appTerm
betaConv
appThm
160
ref
1068
remove
betaConv
appThm
1070
def
1026
ref
1041
ref
424
remove
appTerm
appTerm
refl
appThm
trans
1067
remove
refl
1071
def
435
remove
appThm
eqMp
sym
1036
ref
nil
437
remove
438
remove
1040
ref
nil
cons
cons
439
remove
1039
ref
nil
cons
cons
nil
cons
cons
1072
def
cons
nil
cons
cons
472
remove
subst
1040
remove
240
ref
appTerm
betaConv
nil
87
ref
242
ref
nil
cons
1073
def
cons
61
ref
241
ref
nil
cons
1074
def
cons
1075
def
475
remove
cons
cons
nil
cons
cons
477
remove
506
ref
114
ref
appTerm
1076
def
betaConv
508
ref
116
ref
appTerm
1077
def
betaConv
510
ref
483
remove
appTerm
1078
def
betaConv
512
ref
352
remove
appTerm
1079
def
betaConv
514
ref
482
remove
appTerm
1080
def
betaConv
981
remove
984
remove
755
ref
subst
proveHyp
nil
121
ref
983
remove
cons
122
ref
1080
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
368
ref
369
ref
514
remove
nil
cons
cons
520
remove
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
513
remove
nil
cons
cons
122
ref
1079
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
368
ref
369
ref
512
remove
nil
cons
cons
371
remove
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
511
remove
nil
cons
cons
122
ref
1078
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
521
remove
522
remove
510
remove
nil
cons
cons
523
remove
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
509
remove
nil
cons
cons
122
ref
1077
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
266
ref
56
ref
508
remove
nil
cons
cons
267
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
507
remove
nil
cons
cons
122
ref
1076
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
198
ref
196
ref
506
remove
nil
cons
cons
269
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
1081
def
subst
trans
trans
245
remove
241
ref
appTerm
betaConv
242
ref
refl
appThm
244
remove
242
ref
appTerm
betaConv
trans
trans
appThm
sym
22
ref
1020
ref
41
ref
241
ref
appTerm
242
ref
appTerm
appTerm
absTerm
1082
def
240
remove
appTerm
1083
def
betaConv
1021
ref
241
remove
appTerm
1084
def
betaConv
nil
1030
remove
122
ref
1084
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
266
ref
56
ref
1021
remove
nil
cons
cons
1075
remove
nil
cons
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
21
ref
1082
ref
appTerm
nil
cons
cons
122
ref
1083
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
78
ref
76
ref
1082
remove
nil
cons
cons
263
ref
436
remove
cons
nil
cons
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
1020
ref
243
ref
appTerm
1085
def
nil
cons
cons
122
ref
1026
ref
243
ref
appTerm
1086
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
"x"
29
ref
var
1087
def
272
ref
220
ref
1087
ref
varTerm
appTerm
1088
def
223
ref
appTerm
appTerm
277
ref
94
ref
constTerm
1089
def
619
ref
1088
remove
232
ref
619
ref
varTerm
appTerm
1090
def
appTerm
absTerm
appTerm
appTerm
absTerm
1091
def
243
ref
appTerm
1092
def
betaConv
528
remove
nil
cons
1093
def
47
ref
cons
1094
def
298
remove
subst
nil
121
ref
18
ref
0
ref
90
ref
14
ref
cons
opType
constTerm
1091
ref
appTerm
nil
cons
cons
122
ref
1092
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
"A"
30
remove
cons
nil
cons
1095
def
"P"
90
remove
var
1091
remove
nil
cons
cons
1087
ref
243
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
272
ref
220
ref
243
ref
appTerm
1096
def
223
ref
appTerm
1097
def
appTerm
1089
remove
619
ref
1096
ref
1090
remove
appTerm
absTerm
1098
def
appTerm
1099
def
appTerm
nil
cons
1100
def
cons
122
ref
123
ref
1085
remove
appTerm
1086
remove
appTerm
1101
def
nil
cons
1102
def
cons
nil
cons
1103
def
cons
nil
cons
cons
1104
def
180
ref
subst
proveHyp
1104
ref
140
ref
subst
1104
remove
188
ref
subst
nil
"P"
89
ref
var
1105
def
"yys"
27
ref
var
1106
def
123
ref
1098
ref
1106
ref
varTerm
1107
def
appTerm
1108
def
appTerm
1101
ref
appTerm
1109
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
1094
remove
70
ref
subst
subst
1106
remove
nil
72
ref
1109
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
121
ref
1108
ref
nil
cons
1110
def
cons
1103
ref
cons
nil
cons
cons
1111
def
140
ref
subst
1111
remove
188
ref
subst
1108
ref
betaConv
1108
remove
assume
eqMp
nil
121
ref
1096
remove
232
remove
1107
ref
appTerm
1112
def
appTerm
1113
def
nil
cons
1114
def
cons
1103
ref
cons
nil
cons
cons
1115
def
180
ref
subst
proveHyp
1115
ref
140
ref
subst
1115
remove
188
ref
subst
52
ref
"_32119"
29
ref
var
1116
def
123
ref
1020
ref
1116
remove
varTerm
1117
def
appTerm
appTerm
1026
ref
1117
remove
appTerm
appTerm
absTerm
1118
def
243
remove
appTerm
1119
def
appTerm
refl
1120
def
1118
ref
1112
ref
appTerm
betaConv
appThm
160
ref
1119
remove
betaConv
appThm
1121
def
123
ref
1020
ref
1112
ref
appTerm
appTerm
1026
ref
1112
remove
appTerm
appTerm
refl
appThm
trans
1118
remove
refl
1122
def
1113
remove
assume
appThm
eqMp
sym
123
ref
refl
1123
def
nil
619
ref
1107
ref
nil
cons
1124
def
cons
1125
def
97
ref
1019
ref
nil
cons
cons
526
ref
cons
1126
def
cons
nil
cons
cons
620
ref
subst
appThm
nil
1125
remove
97
remove
1025
ref
nil
cons
cons
526
remove
cons
1127
def
cons
nil
cons
cons
620
ref
subst
appThm
sym
"x"
27
ref
var
1128
def
380
ref
381
ref
277
remove
85
ref
constTerm
1129
def
634
ref
49
ref
0
ref
27
ref
95
remove
cons
opType
constTerm
1130
def
1128
ref
varTerm
1131
def
appTerm
637
ref
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
1132
def
1107
ref
appTerm
1133
def
betaConv
651
remove
nil
18
ref
0
ref
0
ref
652
ref
14
ref
cons
opType
1134
def
14
ref
cons
opType
constTerm
"x"
652
ref
var
1135
def
294
ref
295
remove
380
ref
351
remove
49
ref
0
ref
652
remove
1134
remove
nil
cons
cons
opType
constTerm
1135
remove
varTerm
appTerm
657
remove
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
axiom
subst
nil
121
ref
18
ref
94
remove
constTerm
1136
def
1132
ref
appTerm
nil
cons
cons
122
ref
1133
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
1093
ref
1105
ref
1132
remove
nil
cons
cons
1128
ref
1124
remove
cons
nil
cons
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
380
remove
381
ref
1129
ref
634
ref
1130
remove
1107
ref
appTerm
1137
def
637
remove
appTerm
absTerm
appTerm
absTerm
1138
def
appTerm
1139
def
nil
cons
cons
122
ref
123
ref
1019
ref
1107
ref
appTerm
appTerm
1025
ref
1107
ref
appTerm
appTerm
1140
def
nil
cons
1141
def
cons
nil
cons
1142
def
cons
nil
cons
cons
180
ref
subst
proveHyp
nil
369
ref
101
ref
123
ref
1138
ref
105
ref
appTerm
1143
def
appTerm
1140
ref
appTerm
1144
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
595
ref
subst
101
ref
nil
72
ref
1144
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
121
ref
1143
ref
nil
cons
1145
def
cons
1142
ref
cons
nil
cons
cons
1146
def
140
ref
subst
1146
remove
188
ref
subst
1143
ref
betaConv
1143
remove
assume
eqMp
nil
121
ref
1129
ref
634
remove
1137
ref
106
remove
636
remove
appTerm
appTerm
absTerm
1147
def
appTerm
1148
def
nil
cons
cons
1142
ref
cons
nil
cons
cons
180
ref
subst
proveHyp
nil
196
ref
102
ref
123
ref
1147
ref
107
ref
appTerm
1149
def
appTerm
1140
ref
appTerm
1150
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
199
ref
subst
102
ref
nil
72
ref
1150
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
121
ref
1149
ref
nil
cons
1151
def
cons
1142
ref
cons
nil
cons
cons
1152
def
140
ref
subst
1152
remove
188
ref
subst
1149
ref
betaConv
1149
remove
assume
eqMp
nil
121
ref
1137
remove
108
ref
appTerm
1153
def
nil
cons
1154
def
cons
1142
remove
cons
nil
cons
cons
1155
def
180
ref
subst
proveHyp
1155
ref
140
ref
subst
1155
remove
188
ref
subst
52
ref
"_32121"
27
ref
var
1156
def
123
ref
1019
ref
1156
remove
varTerm
1157
def
appTerm
appTerm
1025
ref
1157
remove
appTerm
appTerm
absTerm
1158
def
1107
remove
appTerm
1159
def
appTerm
refl
1158
ref
108
ref
appTerm
betaConv
appThm
160
ref
1159
remove
betaConv
appThm
123
ref
1019
remove
108
ref
appTerm
appTerm
1025
remove
108
ref
appTerm
appTerm
refl
appThm
trans
1158
remove
refl
1153
remove
assume
appThm
eqMp
sym
1123
ref
102
ref
52
ref
96
ref
"_32133"
89
ref
var
1160
def
100
ref
101
ref
86
ref
102
ref
52
ref
1160
remove
varTerm
108
ref
appTerm
appTerm
1018
ref
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
1161
def
appTerm
1162
def
108
ref
appTerm
appTerm
1018
ref
appTerm
absTerm
1163
def
107
ref
appTerm
1164
def
betaConv
101
ref
86
ref
1163
ref
appTerm
1165
def
absTerm
1166
def
105
ref
appTerm
1167
def
betaConv
1161
ref
1162
remove
appTerm
1168
def
betaConv
1161
ref
"_32131"
27
ref
var
1169
def
112
ref
638
ref
1169
remove
varTerm
appTerm
appTerm
242
ref
appTerm
absTerm
1170
def
appTerm
betaConv
sym
nil
369
ref
101
ref
86
ref
102
ref
52
ref
1170
ref
108
ref
appTerm
1171
def
appTerm
1018
ref
appTerm
1172
def
absTerm
1173
def
appTerm
1174
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
595
ref
subst
101
ref
nil
72
ref
1174
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
196
ref
1173
remove
nil
cons
cons
nil
cons
nil
cons
cons
199
ref
subst
102
ref
nil
72
ref
1172
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
1171
remove
betaConv
52
ref
"_32128"
24
ref
var
1175
def
112
ref
1175
remove
varTerm
appTerm
242
ref
appTerm
absTerm
1176
def
107
ref
appTerm
1177
def
appTerm
refl
1176
ref
647
ref
appTerm
betaConv
appThm
160
ref
1177
remove
betaConv
appThm
648
ref
242
remove
appTerm
refl
appThm
trans
1176
remove
refl
870
ref
appThm
eqMp
sym
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
871
ref
872
ref
1161
ref
nil
cons
1178
def
cons
874
ref
1170
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
716
ref
subst
proveHyp
nil
121
ref
875
ref
1161
remove
appTerm
nil
cons
cons
122
ref
1168
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
nil
876
ref
1178
remove
cons
nil
cons
nil
cons
cons
877
ref
subst
eqMp
eqMp
nil
121
ref
100
ref
1166
ref
appTerm
nil
cons
cons
122
ref
1167
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
368
ref
369
ref
1166
remove
nil
cons
cons
878
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
1165
remove
nil
cons
cons
122
ref
1164
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
198
ref
196
ref
1163
remove
nil
cons
cons
879
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
appThm
102
ref
52
ref
96
remove
"_32145"
89
remove
var
1179
def
100
ref
101
ref
86
ref
102
ref
52
ref
1179
remove
varTerm
108
ref
appTerm
appTerm
1024
ref
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
1180
def
appTerm
1181
def
108
ref
appTerm
appTerm
1024
ref
appTerm
absTerm
1182
def
107
ref
appTerm
1183
def
betaConv
101
ref
86
ref
1182
ref
appTerm
1184
def
absTerm
1185
def
105
remove
appTerm
1186
def
betaConv
1180
ref
1181
remove
appTerm
1187
def
betaConv
1180
ref
"_32143"
27
remove
var
1188
def
112
ref
638
remove
1188
remove
varTerm
appTerm
appTerm
1023
ref
appTerm
absTerm
1189
def
appTerm
betaConv
sym
nil
369
ref
101
ref
86
ref
102
ref
52
ref
1189
ref
108
remove
appTerm
1190
def
appTerm
1024
ref
appTerm
1191
def
absTerm
1192
def
appTerm
1193
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
595
ref
subst
101
ref
nil
72
ref
1193
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
196
ref
1192
remove
nil
cons
cons
nil
cons
nil
cons
cons
199
ref
subst
102
ref
nil
72
ref
1191
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
1190
remove
betaConv
52
ref
"_32140"
24
ref
var
1194
def
112
remove
1194
remove
varTerm
appTerm
1023
ref
appTerm
absTerm
1195
def
107
ref
appTerm
1196
def
appTerm
refl
1195
ref
647
remove
appTerm
betaConv
appThm
160
ref
1196
remove
betaConv
appThm
648
remove
1023
ref
appTerm
refl
appThm
trans
1195
remove
refl
870
remove
appThm
eqMp
sym
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
871
remove
872
remove
1180
ref
nil
cons
1197
def
cons
874
remove
1189
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
716
remove
subst
proveHyp
nil
121
ref
875
remove
1180
remove
appTerm
nil
cons
cons
122
ref
1187
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
nil
876
remove
1197
remove
cons
nil
cons
nil
cons
cons
877
remove
subst
eqMp
eqMp
nil
121
ref
100
ref
1185
ref
appTerm
nil
cons
cons
122
ref
1186
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
368
ref
369
ref
1185
remove
nil
cons
cons
878
remove
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
1184
remove
nil
cons
cons
122
ref
1183
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
198
ref
196
ref
1182
remove
nil
cons
cons
879
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
1198
def
appThm
sym
nil
121
ref
1018
ref
nil
cons
1199
def
cons
122
ref
1024
remove
nil
cons
1200
def
cons
nil
cons
1201
def
cons
nil
cons
cons
1202
def
140
ref
subst
1202
remove
188
ref
subst
nil
102
ref
1073
remove
cons
"y"
1
ref
var
1203
def
1074
remove
cons
87
ref
649
remove
cons
nil
cons
1204
def
cons
cons
nil
cons
cons
102
ref
52
ref
"Parser.Stream.isProperSuffix"
const
111
remove
constTerm
1205
def
114
ref
appTerm
1206
def
503
remove
1203
ref
varTerm
1207
def
appTerm
107
ref
appTerm
appTerm
appTerm
880
remove
107
ref
appTerm
1208
def
appTerm
absTerm
1209
def
107
ref
appTerm
1210
def
betaConv
1203
ref
86
ref
1209
ref
appTerm
1211
def
absTerm
1212
def
1207
ref
appTerm
1213
def
betaConv
87
ref
55
ref
1212
ref
appTerm
1214
def
absTerm
1215
def
114
ref
appTerm
1216
def
betaConv
nil
86
ref
1215
ref
appTerm
1217
def
axiom
nil
121
ref
1217
remove
nil
cons
cons
122
ref
1216
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
198
ref
196
ref
1215
remove
nil
cons
cons
269
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
1214
remove
nil
cons
cons
122
ref
1213
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
266
ref
56
ref
1212
remove
nil
cons
cons
61
ref
1207
ref
nil
cons
cons
nil
cons
1218
def
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
1211
remove
nil
cons
cons
122
ref
1210
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
198
ref
196
ref
1209
remove
nil
cons
cons
879
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
nil
72
ref
1199
ref
cons
nil
cons
nil
cons
cons
75
ref
subst
1018
remove
assume
eqMp
trans
sym
74
ref
eqMp
nil
121
ref
1205
remove
107
ref
appTerm
1023
ref
appTerm
nil
cons
cons
1201
remove
cons
nil
cons
cons
180
ref
subst
proveHyp
nil
102
ref
1037
remove
cons
1219
def
1204
remove
cons
nil
cons
cons
102
remove
123
ref
1206
remove
107
ref
appTerm
appTerm
1208
remove
appTerm
absTerm
1220
def
107
remove
appTerm
1221
def
betaConv
87
ref
86
ref
1220
ref
appTerm
1222
def
absTerm
1223
def
114
ref
appTerm
1224
def
betaConv
nil
86
ref
1223
ref
appTerm
1225
def
axiom
nil
121
ref
1225
remove
nil
cons
cons
122
ref
1224
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
198
ref
196
ref
1223
remove
nil
cons
cons
269
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
1222
remove
nil
cons
cons
122
ref
1221
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
198
ref
196
ref
1220
remove
nil
cons
cons
879
remove
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
nil
157
ref
1199
remove
cons
158
ref
1200
remove
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
157
ref
1154
remove
cons
158
ref
1141
remove
cons
nil
cons
1226
def
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
157
ref
1151
remove
cons
1226
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
121
ref
86
ref
268
ref
123
ref
1147
ref
268
ref
varTerm
1227
def
appTerm
appTerm
1140
ref
appTerm
absTerm
appTerm
nil
cons
cons
122
ref
123
ref
1148
remove
appTerm
1140
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
198
ref
196
ref
1147
remove
nil
cons
cons
1226
ref
cons
nil
cons
cons
591
ref
subst
eqMp
eqMp
eqMp
nil
157
ref
1145
remove
cons
1226
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
121
ref
100
ref
370
ref
123
ref
1138
ref
888
remove
appTerm
appTerm
1140
ref
appTerm
absTerm
appTerm
nil
cons
cons
122
ref
123
ref
1139
remove
appTerm
1140
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
368
ref
369
ref
1138
remove
nil
cons
cons
1226
remove
cons
nil
cons
cons
591
ref
subst
eqMp
eqMp
eqMp
eqMp
eqMp
nil
157
ref
1114
remove
cons
158
ref
1102
ref
cons
nil
cons
1228
def
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
157
ref
1110
remove
cons
1228
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
121
ref
1136
remove
1128
remove
123
ref
1098
ref
1131
remove
appTerm
appTerm
1101
ref
appTerm
absTerm
appTerm
nil
cons
cons
122
ref
123
ref
1099
ref
appTerm
1101
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
1093
remove
1105
remove
1098
remove
nil
cons
cons
1228
ref
cons
nil
cons
cons
591
ref
subst
eqMp
nil
121
ref
1097
ref
nil
cons
1229
def
cons
1103
remove
cons
nil
cons
cons
1230
def
140
ref
subst
1230
remove
188
ref
subst
1120
remove
"_32117"
29
remove
var
1231
def
123
ref
1020
ref
1231
remove
varTerm
1232
def
appTerm
appTerm
1026
ref
1232
remove
appTerm
appTerm
absTerm
223
ref
appTerm
betaConv
appThm
1121
remove
123
ref
1020
remove
223
ref
appTerm
appTerm
1026
ref
223
ref
appTerm
appTerm
refl
appThm
trans
1122
remove
1097
remove
assume
appThm
eqMp
sym
1123
ref
nil
1126
remove
nil
cons
cons
538
ref
subst
appThm
nil
1127
ref
nil
cons
cons
538
remove
subst
1233
def
appThm
nil
72
ref
525
remove
cons
nil
cons
nil
cons
cons
1234
def
72
ref
52
ref
123
ref
62
remove
appTerm
73
ref
appTerm
appTerm
73
ref
appTerm
absTerm
1235
def
73
ref
appTerm
1236
def
betaConv
nil
565
ref
1235
ref
appTerm
1237
def
axiom
nil
121
ref
1237
remove
nil
cons
cons
122
ref
1236
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
586
ref
587
ref
1235
remove
nil
cons
cons
868
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
trans
sym
74
ref
eqMp
eqMp
eqMp
nil
157
ref
1229
remove
cons
1238
def
1228
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
nil
1238
remove
158
ref
1099
remove
nil
cons
cons
894
ref
1102
remove
cons
nil
cons
cons
cons
nil
cons
cons
909
ref
subst
proveHyp
proveHyp
eqMp
nil
157
ref
1100
remove
cons
1228
remove
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
nil
540
remove
158
ref
1060
ref
cons
nil
cons
1239
def
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
542
remove
1239
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
121
ref
21
ref
263
ref
544
remove
1059
ref
appTerm
absTerm
appTerm
nil
cons
cons
122
ref
545
remove
1059
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
78
ref
546
remove
1239
ref
cons
nil
cons
cons
591
ref
subst
eqMp
nil
369
remove
"w"
5
remove
var
1240
def
123
ref
407
remove
1240
ref
varTerm
1241
def
appTerm
1242
def
appTerm
1059
ref
appTerm
1243
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
595
remove
subst
1240
remove
nil
72
ref
1243
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
121
ref
1242
ref
nil
cons
1244
def
cons
1061
ref
cons
nil
cons
cons
1245
def
140
ref
subst
1245
remove
188
ref
subst
1242
ref
betaConv
1242
remove
assume
eqMp
nil
121
ref
406
remove
386
remove
1241
ref
appTerm
1246
def
appTerm
1247
def
nil
cons
1248
def
cons
1061
remove
cons
nil
cons
cons
1249
def
180
ref
subst
proveHyp
1249
ref
140
ref
subst
1249
remove
188
ref
subst
1069
remove
"_32101"
8
remove
var
1250
def
1026
ref
1041
ref
1250
remove
varTerm
appTerm
appTerm
absTerm
1246
ref
appTerm
betaConv
appThm
1070
remove
1026
ref
1041
remove
1246
remove
appTerm
appTerm
refl
appThm
trans
1071
remove
1247
remove
assume
appThm
eqMp
sym
1036
ref
nil
381
remove
1241
ref
nil
cons
1251
def
cons
1072
remove
cons
nil
cons
cons
618
remove
subst
1039
remove
1241
ref
appTerm
betaConv
trans
appThm
nil
619
remove
104
remove
1241
remove
appTerm
1023
remove
appTerm
nil
cons
cons
1127
remove
cons
nil
cons
cons
620
remove
subst
nil
1219
remove
101
remove
1251
remove
cons
nil
cons
cons
nil
cons
cons
1198
remove
subst
1038
remove
885
remove
subst
trans
trans
trans
sym
74
ref
eqMp
eqMp
eqMp
nil
157
ref
1248
remove
cons
1239
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
157
ref
1244
remove
cons
1239
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
121
ref
100
remove
370
remove
889
remove
1059
ref
appTerm
absTerm
appTerm
nil
cons
cons
122
ref
890
remove
1059
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
368
remove
891
remove
1239
ref
cons
nil
cons
cons
591
ref
subst
eqMp
nil
892
remove
893
remove
894
ref
1060
remove
cons
nil
cons
cons
cons
nil
cons
cons
909
ref
subst
proveHyp
proveHyp
eqMp
nil
910
remove
1239
remove
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
nil
911
remove
158
ref
1046
ref
cons
nil
cons
1252
def
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
913
remove
1252
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
121
ref
404
remove
379
remove
914
remove
1045
ref
appTerm
absTerm
appTerm
nil
cons
cons
122
ref
915
remove
1045
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
287
remove
916
remove
1252
ref
cons
nil
cons
cons
591
ref
subst
eqMp
nil
918
remove
1047
remove
cons
nil
cons
cons
1253
def
140
ref
subst
1253
remove
188
ref
subst
1055
remove
"_32097"
10
remove
var
1254
def
1026
ref
1044
ref
1254
remove
varTerm
appTerm
appTerm
absTerm
276
ref
appTerm
betaConv
appThm
1056
remove
1026
remove
1044
remove
276
remove
appTerm
appTerm
refl
appThm
trans
1057
remove
921
remove
appThm
eqMp
sym
1036
remove
nil
1058
remove
nil
cons
cons
922
remove
subst
appThm
1233
remove
trans
sym
74
ref
eqMp
eqMp
eqMp
nil
923
ref
1252
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
nil
923
remove
924
remove
894
ref
1046
remove
cons
nil
cons
cons
cons
nil
cons
cons
909
ref
subst
proveHyp
proveHyp
eqMp
nil
925
remove
1252
remove
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
157
ref
1029
remove
cons
158
ref
1031
remove
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
eqMp
nil
121
ref
129
ref
926
remove
appTerm
939
remove
appTerm
nil
cons
cons
122
ref
86
ref
206
ref
appTerm
nil
cons
1255
def
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
1123
ref
129
ref
refl
1256
def
206
ref
209
ref
appTerm
betaConv
appThm
1256
ref
206
ref
496
ref
appTerm
betaConv
appThm
668
remove
61
ref
86
ref
refl
1257
def
87
ref
1123
remove
208
ref
appThm
206
ref
505
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
appThm
1257
remove
87
ref
208
remove
absThm
appThm
appThm
nil
"p"
84
ref
var
1258
def
206
remove
nil
cons
1259
def
cons
nil
cons
nil
cons
cons
1258
ref
123
ref
129
ref
1258
remove
varTerm
1260
def
209
ref
appTerm
appTerm
129
ref
1260
ref
496
ref
appTerm
appTerm
55
ref
61
ref
86
ref
87
ref
123
ref
1260
ref
114
ref
appTerm
1261
def
appTerm
1260
ref
505
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
appTerm
86
ref
87
ref
1261
remove
absTerm
appTerm
appTerm
absTerm
1262
def
1260
ref
appTerm
1263
def
betaConv
nil
18
ref
0
ref
85
ref
14
ref
cons
opType
constTerm
1262
ref
appTerm
1264
def
axiom
nil
121
ref
1264
remove
nil
cons
cons
122
ref
1263
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
"A"
110
remove
cons
nil
cons
"P"
85
remove
var
1262
remove
nil
cons
cons
"x"
84
remove
var
1260
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
nil
121
ref
1255
remove
cons
122
ref
207
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
198
ref
196
ref
1259
remove
cons
269
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
205
remove
nil
cons
cons
122
ref
204
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
266
ref
56
ref
203
remove
nil
cons
cons
267
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
202
remove
nil
cons
cons
122
ref
201
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
78
ref
76
ref
200
remove
nil
cons
cons
264
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
eqMp
1265
def
absThm
eqMp
eqMp
absThm
eqMp
nil
260
ref
45
remove
appTerm
thm
260
ref
refl
1266
def
17
ref
nil
"g"
0
ref
2
remove
"Parser.parser"
typeOp
349
remove
opType
1267
def
nil
cons
1268
def
cons
opType
1269
def
var
"Function.o"
const
1270
def
0
ref
0
ref
33
ref
1268
ref
cons
opType
1271
def
0
ref
37
ref
1269
ref
nil
cons
1272
def
cons
opType
nil
cons
cons
opType
constTerm
"Parser.mk"
const
1271
ref
constTerm
1273
def
appTerm
39
ref
appTerm
1274
def
nil
cons
cons
"f"
1269
ref
var
"Parser.fold"
const
0
ref
12
remove
1272
remove
cons
opType
constTerm
38
ref
appTerm
1275
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
77
ref
"B"
1268
ref
cons
nil
cons
cons
47
ref
cons
"g"
350
ref
var
1276
def
52
ref
729
remove
354
ref
appTerm
1276
ref
varTerm
1277
def
appTerm
1278
def
appTerm
55
ref
61
ref
347
remove
354
ref
116
ref
appTerm
appTerm
1277
ref
116
ref
appTerm
1279
def
appTerm
absTerm
appTerm
1280
def
appTerm
absTerm
1281
def
1277
ref
appTerm
1282
def
betaConv
353
ref
362
ref
1281
ref
appTerm
1283
def
absTerm
1284
def
354
remove
appTerm
1285
def
betaConv
362
ref
refl
1286
def
353
ref
1286
remove
1276
ref
nil
"y"
13
remove
var
1280
ref
nil
cons
cons
588
remove
1278
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
709
remove
1203
remove
52
ref
49
ref
0
ref
1
remove
778
remove
cons
opType
constTerm
1287
def
116
ref
appTerm
1288
def
1207
ref
appTerm
appTerm
1287
remove
1207
ref
appTerm
116
ref
appTerm
appTerm
absTerm
1289
def
1207
remove
appTerm
1290
def
betaConv
61
ref
55
ref
1289
ref
appTerm
1291
def
absTerm
1292
def
116
ref
appTerm
1293
def
betaConv
nil
55
ref
1292
ref
appTerm
1294
def
axiom
nil
121
ref
1294
remove
nil
cons
cons
122
ref
1293
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
266
ref
56
ref
1292
remove
nil
cons
cons
267
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
1291
remove
nil
cons
cons
122
ref
1290
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
266
ref
56
ref
1289
remove
nil
cons
cons
1218
remove
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
subst
absThm
appThm
absThm
appThm
sym
nil
362
ref
353
remove
362
ref
1276
ref
52
ref
1280
remove
appTerm
1278
remove
appTerm
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
121
ref
362
ref
1284
ref
appTerm
nil
cons
cons
122
ref
1285
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
372
ref
373
ref
1284
remove
nil
cons
cons
375
remove
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
1283
remove
nil
cons
cons
122
ref
1282
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
372
ref
373
ref
1281
remove
nil
cons
cons
374
remove
1277
ref
nil
cons
cons
nil
cons
1295
def
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
1296
def
subst
subst
21
ref
refl
1297
def
263
remove
49
ref
0
ref
1267
ref
0
ref
1267
ref
14
ref
cons
opType
1298
def
nil
cons
cons
opType
constTerm
1299
def
refl
nil
22
ref
543
ref
nil
cons
cons
nil
cons
nil
cons
cons
22
ref
1299
remove
1275
ref
40
ref
appTerm
1300
def
appTerm
1273
ref
41
ref
appTerm
appTerm
absTerm
1301
def
40
ref
appTerm
1302
def
betaConv
17
ref
21
ref
1301
ref
appTerm
1303
def
absTerm
1304
def
38
ref
appTerm
1305
def
betaConv
nil
260
ref
1304
ref
appTerm
1306
def
axiom
nil
121
ref
1306
remove
nil
cons
cons
122
ref
1305
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
46
ref
16
ref
1304
remove
nil
cons
cons
262
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
1303
remove
nil
cons
cons
122
ref
1302
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
78
ref
76
ref
1301
remove
nil
cons
cons
264
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
1307
def
subst
appThm
nil
"g"
37
remove
var
39
ref
nil
cons
cons
"f"
1271
remove
var
1273
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
"B"
36
ref
cons
77
remove
"C"
1268
ref
cons
nil
cons
cons
cons
47
ref
cons
61
ref
442
remove
1270
remove
0
ref
444
ref
0
ref
350
remove
463
remove
cons
opType
nil
cons
cons
opType
constTerm
"f"
444
remove
var
1308
def
varTerm
1309
def
appTerm
1277
ref
appTerm
116
ref
appTerm
appTerm
1309
ref
1279
remove
appTerm
appTerm
absTerm
1310
def
116
ref
appTerm
1311
def
betaConv
1276
remove
55
ref
1310
ref
appTerm
1312
def
absTerm
1313
def
1277
remove
appTerm
1314
def
betaConv
1308
remove
362
remove
1313
ref
appTerm
1315
def
absTerm
1316
def
1309
ref
appTerm
1317
def
betaConv
nil
456
remove
1316
ref
appTerm
1318
def
axiom
nil
121
ref
1318
remove
nil
cons
cons
122
ref
1317
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
468
remove
469
remove
1316
remove
nil
cons
cons
470
remove
1309
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
1315
remove
nil
cons
cons
122
ref
1314
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
372
remove
373
remove
1313
remove
nil
cons
cons
1295
remove
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
1312
remove
nil
cons
cons
122
ref
1311
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
266
ref
56
ref
1310
remove
nil
cons
cons
267
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
subst
appThm
nil
"x"
1267
ref
var
1319
def
1273
ref
39
remove
543
remove
appTerm
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
1268
remove
cons
nil
cons
1320
def
47
ref
cons
1321
def
nil
72
ref
1288
remove
116
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
189
ref
eqMp
1322
def
subst
subst
trans
absThm
appThm
1234
ref
79
remove
72
ref
52
ref
55
ref
61
ref
73
ref
absTerm
appTerm
appTerm
73
ref
appTerm
absTerm
1323
def
73
remove
appTerm
1324
def
betaConv
nil
565
remove
1323
ref
appTerm
1325
def
axiom
nil
121
ref
1325
remove
nil
cons
cons
122
ref
1324
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
586
remove
587
remove
1323
remove
nil
cons
cons
868
remove
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
1326
def
subst
subst
1327
def
trans
trans
absThm
appThm
1234
remove
48
remove
1326
remove
subst
subst
1328
def
trans
sym
74
ref
eqMp
nil
260
ref
17
ref
49
ref
0
ref
1269
ref
0
ref
1269
remove
14
ref
cons
opType
nil
cons
cons
opType
constTerm
1275
remove
appTerm
1274
remove
appTerm
absTerm
appTerm
thm
1266
remove
17
ref
1297
remove
22
ref
49
ref
0
ref
33
ref
34
remove
nil
cons
cons
opType
constTerm
1329
def
refl
"Parser.dest"
const
0
ref
1267
ref
36
remove
cons
opType
constTerm
1330
def
refl
1307
remove
appThm
appThm
41
ref
refl
appThm
nil
"r"
33
remove
var
1331
def
82
remove
cons
nil
cons
nil
cons
cons
1331
ref
52
ref
1329
ref
1330
ref
1273
remove
1331
ref
varTerm
1332
def
appTerm
appTerm
appTerm
1332
ref
appTerm
1333
def
appTerm
35
remove
1332
ref
appTerm
1334
def
appTerm
1335
def
absTerm
1336
def
1332
ref
appTerm
1337
def
betaConv
119
ref
refl
1331
ref
1335
remove
assume
sym
52
ref
1334
remove
appTerm
1333
remove
appTerm
1338
def
assume
sym
deductAntisym
absThm
appThm
nil
119
ref
1331
remove
1338
remove
absTerm
appTerm
axiom
eqMp
nil
121
ref
119
remove
1336
ref
appTerm
nil
cons
cons
122
ref
1337
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
181
remove
182
remove
1336
remove
nil
cons
cons
183
remove
1332
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
1265
remove
trans
trans
absThm
appThm
1327
remove
trans
absThm
appThm
1328
remove
trans
sym
74
ref
eqMp
1339
def
nil
260
ref
17
ref
21
ref
22
ref
1329
remove
1330
ref
1300
ref
appTerm
appTerm
41
remove
appTerm
absTerm
1340
def
appTerm
1341
def
absTerm
1342
def
appTerm
1343
def
thm
nil
16
ref
17
ref
21
remove
22
ref
49
remove
0
ref
31
ref
0
ref
31
ref
14
ref
cons
opType
nil
cons
cons
opType
constTerm
"Parser.apply"
const
0
ref
1267
ref
32
remove
cons
opType
constTerm
1344
def
1300
ref
appTerm
1345
def
appTerm
237
remove
61
ref
87
ref
192
remove
absTerm
1346
def
absTerm
1347
def
appTerm
1348
def
appTerm
1349
def
absTerm
1350
def
appTerm
1351
def
absTerm
1352
def
nil
cons
cons
nil
cons
nil
cons
cons
71
remove
subst
17
remove
nil
72
ref
1351
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
76
ref
1350
remove
nil
cons
cons
nil
cons
nil
cons
cons
80
remove
subst
22
remove
nil
72
ref
1349
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
"g"
31
ref
var
1348
ref
nil
cons
cons
"f"
31
remove
var
1345
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
197
remove
345
remove
cons
47
ref
cons
1296
remove
subst
subst
sym
nil
196
ref
87
ref
220
ref
1345
ref
114
ref
appTerm
appTerm
1348
ref
114
ref
appTerm
appTerm
1353
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
199
ref
subst
87
ref
nil
72
ref
1353
ref
nil
cons
1354
def
cons
nil
cons
nil
cons
cons
75
ref
subst
87
ref
272
ref
635
remove
114
ref
appTerm
1355
def
209
ref
appTerm
1356
def
appTerm
272
remove
1355
ref
496
ref
appTerm
1357
def
appTerm
294
remove
61
ref
1129
remove
"xt"
24
remove
var
1358
def
1355
remove
504
remove
1358
ref
varTerm
1359
def
appTerm
appTerm
1360
def
absTerm
1361
def
appTerm
1362
def
absTerm
1363
def
appTerm
1364
def
appTerm
1365
def
appTerm
1366
def
absTerm
1367
def
114
ref
appTerm
1368
def
betaConv
nil
86
ref
1367
ref
appTerm
1369
def
axiom
nil
121
ref
1369
remove
nil
cons
cons
122
ref
1368
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
198
ref
196
ref
1367
remove
nil
cons
cons
269
ref
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
1366
remove
nil
cons
1370
def
cons
122
ref
1354
ref
cons
nil
cons
1371
def
cons
nil
cons
cons
1372
def
180
ref
subst
proveHyp
1372
ref
140
ref
subst
1372
remove
188
ref
subst
nil
121
ref
1365
remove
nil
cons
1373
def
cons
1371
ref
cons
nil
cons
cons
1374
def
140
ref
subst
1374
remove
188
ref
subst
nil
56
ref
61
ref
123
ref
1363
ref
116
ref
appTerm
1375
def
appTerm
1353
ref
appTerm
1376
def
absTerm
1377
def
nil
cons
cons
nil
cons
nil
cons
cons
70
remove
subst
61
ref
nil
72
ref
1376
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
subst
nil
121
ref
1375
ref
nil
cons
1378
def
cons
1371
ref
cons
nil
cons
cons
1379
def
140
ref
subst
1379
remove
188
ref
subst
1375
ref
betaConv
1375
remove
assume
eqMp
nil
121
ref
1362
ref
nil
cons
cons
1371
ref
cons
nil
cons
cons
180
ref
subst
proveHyp
nil
196
ref
1358
ref
123
ref
1361
ref
1359
ref
appTerm
1380
def
appTerm
1353
ref
appTerm
1381
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
199
remove
subst
1358
remove
nil
72
remove
1381
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
remove
subst
nil
121
ref
1380
ref
nil
cons
1382
def
cons
1371
ref
cons
nil
cons
cons
1383
def
140
ref
subst
1383
remove
188
ref
subst
1380
ref
betaConv
1380
remove
assume
eqMp
nil
121
ref
1360
ref
nil
cons
1384
def
cons
1371
ref
cons
nil
cons
cons
1385
def
180
ref
subst
proveHyp
1385
ref
140
ref
subst
1385
remove
188
ref
subst
220
ref
refl
1386
def
1345
remove
refl
1387
def
1360
remove
assume
1388
def
appThm
nil
87
ref
1359
ref
nil
cons
cons
1389
def
"p"
1267
remove
var
1390
def
1300
remove
nil
cons
cons
nil
cons
1391
def
cons
nil
cons
cons
87
remove
220
ref
1344
remove
1390
ref
varTerm
1392
def
appTerm
1393
def
505
remove
appTerm
appTerm
1330
remove
1392
ref
appTerm
116
ref
appTerm
114
ref
appTerm
appTerm
absTerm
1394
def
114
remove
appTerm
1395
def
betaConv
61
ref
86
ref
1394
ref
appTerm
1396
def
absTerm
1397
def
116
ref
appTerm
1398
def
betaConv
1390
ref
129
ref
220
ref
1393
ref
209
remove
appTerm
appTerm
223
ref
appTerm
1399
def
appTerm
129
ref
220
remove
1393
remove
496
remove
appTerm
appTerm
223
remove
appTerm
1400
def
appTerm
55
ref
1397
ref
appTerm
1401
def
appTerm
1402
def
appTerm
absTerm
1403
def
1392
ref
appTerm
1404
def
betaConv
129
ref
18
remove
0
remove
1298
ref
14
remove
cons
opType
constTerm
1405
def
1390
ref
1399
ref
absTerm
1406
def
appTerm
1407
def
appTerm
refl
160
ref
1256
ref
1405
ref
refl
1408
def
1390
ref
1390
ref
1400
ref
absTerm
1409
def
1392
ref
appTerm
betaConv
1410
def
absThm
appThm
appThm
1408
ref
1390
ref
1390
ref
1401
ref
absTerm
1411
def
1392
ref
appTerm
betaConv
1412
def
absThm
appThm
appThm
appThm
1408
ref
1390
ref
1256
ref
1410
remove
appThm
1412
remove
appThm
absThm
appThm
appThm
nil
"p"
1298
ref
var
1413
def
1409
ref
nil
cons
cons
"q"
1298
ref
var
1414
def
1411
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
1321
remove
"q"
53
remove
var
1415
def
52
ref
129
ref
55
ref
735
remove
appTerm
appTerm
55
ref
61
ref
1415
ref
varTerm
1416
def
116
ref
appTerm
1417
def
absTerm
appTerm
appTerm
1418
def
appTerm
55
ref
61
remove
129
ref
570
remove
appTerm
1417
remove
appTerm
absTerm
appTerm
1419
def
appTerm
1420
def
absTerm
1421
def
1416
ref
appTerm
1422
def
betaConv
59
ref
776
ref
1421
ref
appTerm
1423
def
absTerm
1424
def
60
remove
appTerm
1425
def
betaConv
776
ref
refl
1426
def
59
ref
1426
remove
1415
ref
1420
remove
assume
sym
52
remove
1419
remove
appTerm
1418
remove
appTerm
1427
def
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
nil
776
ref
59
remove
776
ref
1415
remove
1427
remove
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
121
ref
776
remove
1424
ref
appTerm
nil
cons
cons
122
ref
1425
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
779
ref
780
ref
1424
remove
nil
cons
cons
782
remove
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
1423
remove
nil
cons
cons
122
ref
1422
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
779
remove
780
remove
1421
remove
nil
cons
cons
781
remove
1416
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
1428
def
subst
eqMp
appThm
160
remove
1256
ref
1408
ref
1390
ref
1406
ref
1392
ref
appTerm
betaConv
1429
def
absThm
appThm
appThm
1408
ref
1390
ref
1390
ref
1402
ref
absTerm
1430
def
1392
ref
appTerm
betaConv
1431
def
absThm
appThm
appThm
appThm
1408
remove
1390
remove
1256
remove
1429
remove
appThm
1431
remove
appThm
absThm
appThm
appThm
nil
1413
remove
1406
remove
nil
cons
cons
1414
remove
1430
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
1428
remove
subst
eqMp
trans
nil
1407
ref
axiom
nil
121
ref
1407
remove
nil
cons
cons
122
ref
129
remove
1405
ref
1409
remove
appTerm
1432
def
appTerm
1405
ref
1411
remove
appTerm
1433
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
188
ref
subst
proveHyp
nil
1432
ref
axiom
nil
121
ref
1432
remove
nil
cons
cons
122
ref
1433
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
188
ref
subst
proveHyp
nil
1433
remove
axiom
eqMp
eqMp
eqMp
nil
121
ref
1405
remove
1403
ref
appTerm
nil
cons
cons
122
ref
1404
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
1320
remove
"P"
1298
remove
var
1403
remove
nil
cons
cons
1319
remove
1392
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
1434
def
nil
157
ref
1399
remove
nil
cons
cons
158
ref
1402
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
1435
def
755
ref
subst
proveHyp
1436
def
nil
157
ref
1400
remove
nil
cons
cons
158
ref
1401
remove
nil
cons
1437
def
cons
nil
cons
cons
nil
cons
cons
1438
def
755
remove
subst
proveHyp
nil
121
ref
1437
remove
cons
122
ref
1398
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
266
ref
56
ref
1397
remove
nil
cons
cons
267
remove
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
1396
remove
nil
cons
cons
122
ref
1395
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
198
ref
196
ref
1394
remove
nil
cons
cons
269
remove
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
subst
1340
ref
40
remove
appTerm
1439
def
betaConv
1342
ref
38
remove
appTerm
1440
def
betaConv
1339
remove
nil
121
ref
1343
remove
nil
cons
cons
122
ref
1440
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
46
remove
16
remove
1342
remove
nil
cons
cons
262
remove
cons
nil
cons
cons
190
ref
subst
eqMp
eqMp
nil
121
ref
1341
remove
nil
cons
cons
122
ref
1439
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
78
remove
76
remove
1340
remove
nil
cons
cons
264
remove
cons
nil
cons
cons
190
remove
subst
eqMp
eqMp
189
remove
appThm
1359
ref
refl
1441
def
appThm
trans
trans
appThm
1348
remove
refl
1442
def
1388
remove
appThm
nil
1389
remove
473
remove
1347
ref
nil
cons
cons
474
remove
cons
1443
def
cons
nil
cons
cons
1081
remove
subst
1347
remove
116
remove
appTerm
betaConv
1441
remove
appThm
1346
remove
1359
ref
appTerm
betaConv
trans
trans
trans
appThm
nil
1087
ref
191
remove
1359
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
1095
remove
47
remove
cons
1322
remove
subst
1444
def
subst
trans
sym
74
ref
eqMp
eqMp
nil
157
ref
1384
remove
cons
158
ref
1354
ref
cons
nil
cons
1445
def
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
157
ref
1382
remove
cons
1445
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
121
ref
86
remove
268
remove
123
ref
1361
ref
1227
remove
appTerm
appTerm
1353
ref
appTerm
absTerm
appTerm
nil
cons
cons
122
ref
123
ref
1362
remove
appTerm
1353
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
ref
subst
proveHyp
198
remove
196
remove
1361
remove
nil
cons
cons
1445
ref
cons
nil
cons
cons
591
ref
subst
eqMp
eqMp
eqMp
nil
157
ref
1378
remove
cons
1445
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
121
ref
55
remove
1377
remove
appTerm
nil
cons
cons
122
remove
123
remove
1364
ref
appTerm
1353
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
180
remove
subst
proveHyp
266
remove
56
remove
1363
remove
nil
cons
cons
1445
ref
cons
nil
cons
cons
591
remove
subst
eqMp
nil
121
ref
1357
ref
nil
cons
1446
def
cons
1371
ref
cons
nil
cons
cons
1447
def
140
ref
subst
1447
remove
188
ref
subst
1386
ref
1387
ref
1357
remove
assume
1448
def
appThm
nil
1391
remove
nil
cons
cons
1449
def
1436
remove
1438
remove
172
ref
subst
proveHyp
subst
trans
appThm
1442
ref
1448
remove
appThm
nil
1443
remove
nil
cons
cons
1450
def
985
remove
subst
trans
appThm
nil
1087
remove
341
remove
cons
nil
cons
nil
cons
cons
1444
remove
subst
1451
def
trans
sym
74
ref
eqMp
eqMp
nil
157
ref
1446
remove
cons
1452
def
1445
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
nil
1452
remove
158
ref
1364
remove
nil
cons
cons
894
remove
1354
remove
cons
nil
cons
1453
def
cons
cons
nil
cons
cons
909
ref
subst
proveHyp
proveHyp
eqMp
nil
157
ref
1373
ref
cons
1445
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
nil
121
remove
1356
ref
nil
cons
1454
def
cons
1371
remove
cons
nil
cons
cons
1455
def
140
remove
subst
1455
remove
188
remove
subst
1386
remove
1387
remove
1356
remove
assume
1456
def
appThm
1449
remove
1434
remove
1435
remove
172
ref
subst
proveHyp
subst
trans
appThm
1442
remove
1456
remove
appThm
1450
remove
524
remove
subst
trans
appThm
1451
remove
trans
sym
74
remove
eqMp
eqMp
nil
157
ref
1454
remove
cons
1457
def
1445
ref
cons
nil
cons
cons
172
ref
subst
deductAntisym
eqMp
nil
1457
remove
158
remove
1373
remove
cons
1453
remove
cons
cons
nil
cons
cons
909
remove
subst
proveHyp
proveHyp
eqMp
nil
157
remove
1370
remove
cons
1445
remove
cons
nil
cons
cons
172
remove
subst
deductAntisym
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
260
remove
1352
remove
appTerm
thm