6
version
"Data.Bool.!"
const
0
def
"->"
typeOp
1
def
1
ref
"Number.Natural.natural"
"HOLLight.mk_num"
"HOLLight.dest_num"
nil
"HOLLight.NUM_REP"
"a"
"ind"
typeOp
nil
opType
2
def
var
3
def
0
ref
1
ref
1
ref
1
ref
2
ref
"bool"
typeOp
nil
opType
4
def
nil
cons
5
def
cons
opType
6
def
5
ref
cons
opType
7
def
5
ref
cons
opType
constTerm
8
def
"NUM_REP'"
6
ref
var
9
def
"Data.Bool.==>"
const
1
ref
4
ref
1
ref
4
ref
5
ref
cons
opType
10
def
nil
cons
cons
opType
11
def
constTerm
12
def
0
ref
7
ref
constTerm
13
def
3
ref
12
ref
"Data.Bool.\\/"
const
11
ref
constTerm
14
def
"="
const
15
def
1
ref
2
ref
6
ref
nil
cons
16
def
cons
opType
17
def
constTerm
18
def
3
ref
varTerm
19
def
appTerm
20
def
"HOLLight.IND_0"
"select"
const
21
def
1
ref
6
ref
2
ref
nil
cons
22
def
cons
opType
constTerm
"z"
2
ref
var
23
def
"Data.Bool./\\"
const
11
ref
constTerm
24
def
13
ref
"x1"
2
ref
var
25
def
13
ref
"x2"
2
ref
var
26
def
15
ref
11
ref
constTerm
27
def
18
ref
"HOLLight.IND_SUC"
21
ref
1
ref
1
ref
1
ref
2
ref
22
ref
cons
opType
28
def
5
ref
cons
opType
29
def
28
ref
nil
cons
30
def
cons
opType
constTerm
"f"
28
ref
var
31
def
"Data.Bool.?"
const
32
def
7
ref
constTerm
33
def
23
ref
24
ref
13
ref
25
ref
13
ref
26
ref
27
ref
18
ref
31
ref
varTerm
34
def
25
ref
varTerm
35
def
appTerm
appTerm
34
ref
26
ref
varTerm
36
def
appTerm
37
def
appTerm
38
def
appTerm
18
ref
35
ref
appTerm
36
ref
appTerm
39
def
appTerm
absTerm
40
def
appTerm
absTerm
41
def
appTerm
42
def
appTerm
43
def
13
ref
"x"
2
ref
var
44
def
"Data.Bool.~"
const
10
ref
constTerm
45
def
18
ref
34
ref
44
ref
varTerm
46
def
appTerm
47
def
appTerm
23
ref
varTerm
48
def
appTerm
49
def
appTerm
absTerm
50
def
appTerm
51
def
appTerm
absTerm
appTerm
52
def
absTerm
53
def
appTerm
54
def
defineConst
55
def
pop
28
ref
constTerm
56
def
35
ref
appTerm
appTerm
56
ref
36
ref
appTerm
appTerm
appTerm
39
ref
appTerm
absTerm
57
def
appTerm
58
def
absTerm
59
def
appTerm
60
def
appTerm
61
def
13
ref
44
ref
45
ref
18
ref
56
ref
46
ref
appTerm
appTerm
62
def
48
ref
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
63
def
appTerm
64
def
defineConst
65
def
pop
2
ref
constTerm
66
def
appTerm
67
def
appTerm
68
def
33
ref
"i"
2
ref
var
69
def
24
ref
20
remove
56
ref
69
ref
varTerm
70
def
appTerm
71
def
appTerm
72
def
appTerm
73
def
9
ref
varTerm
74
def
70
ref
appTerm
75
def
appTerm
76
def
absTerm
77
def
appTerm
78
def
appTerm
79
def
appTerm
74
ref
19
ref
appTerm
80
def
appTerm
81
def
absTerm
82
def
appTerm
83
def
appTerm
84
def
80
ref
appTerm
85
def
absTerm
86
def
appTerm
87
def
absTerm
88
def
defineConst
89
def
pop
90
def
pop
89
remove
nil
"p"
4
ref
var
91
def
15
ref
1
ref
6
ref
7
ref
nil
cons
cons
opType
constTerm
92
def
90
remove
6
ref
constTerm
93
def
appTerm
88
ref
appTerm
nil
cons
cons
"q"
4
ref
var
94
def
24
ref
24
ref
93
ref
66
ref
appTerm
95
def
appTerm
13
ref
69
ref
12
ref
93
ref
70
ref
appTerm
96
def
appTerm
93
ref
71
ref
appTerm
97
def
appTerm
absTerm
98
def
appTerm
99
def
appTerm
100
def
appTerm
24
ref
8
ref
9
ref
12
ref
24
ref
74
ref
66
ref
appTerm
appTerm
13
ref
69
ref
12
ref
75
ref
appTerm
74
ref
71
ref
appTerm
appTerm
absTerm
appTerm
appTerm
appTerm
101
def
13
ref
3
ref
12
ref
93
ref
19
ref
appTerm
102
def
appTerm
103
def
80
ref
appTerm
absTerm
appTerm
appTerm
absTerm
104
def
appTerm
105
def
appTerm
13
ref
3
ref
27
ref
102
ref
appTerm
68
ref
33
ref
69
ref
73
ref
96
ref
appTerm
absTerm
appTerm
appTerm
appTerm
absTerm
appTerm
106
def
appTerm
107
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
27
ref
12
ref
91
ref
varTerm
108
def
appTerm
109
def
94
ref
varTerm
110
def
appTerm
111
def
appTerm
112
def
refl
91
ref
94
ref
27
ref
24
ref
108
ref
appTerm
113
def
110
ref
appTerm
114
def
appTerm
115
def
108
ref
appTerm
absTerm
116
def
absTerm
117
def
108
ref
appTerm
betaConv
110
ref
refl
118
def
appThm
116
remove
110
ref
appTerm
betaConv
trans
appThm
nil
15
ref
1
ref
11
ref
1
ref
11
ref
5
ref
cons
opType
119
def
nil
cons
cons
opType
constTerm
120
def
12
ref
appTerm
117
remove
appTerm
axiom
108
ref
refl
121
def
appThm
118
ref
appThm
eqMp
122
def
sym
123
def
115
remove
refl
94
ref
15
ref
1
ref
119
ref
1
ref
119
remove
5
ref
cons
opType
nil
cons
cons
opType
constTerm
124
def
"f"
11
remove
var
125
def
125
ref
varTerm
126
def
108
ref
appTerm
110
ref
appTerm
absTerm
127
def
appTerm
125
ref
126
ref
"Data.Bool.T"
const
4
ref
constTerm
128
def
appTerm
128
ref
appTerm
absTerm
129
def
appTerm
absTerm
130
def
110
ref
appTerm
betaConv
appThm
15
ref
1
ref
10
ref
1
ref
10
ref
5
ref
cons
opType
131
def
nil
cons
cons
opType
constTerm
132
def
113
ref
appTerm
refl
91
ref
130
remove
absTerm
133
def
108
ref
appTerm
betaConv
appThm
nil
120
ref
24
ref
appTerm
133
ref
appTerm
axiom
134
def
121
remove
appThm
eqMp
118
ref
appThm
eqMp
135
def
sym
125
ref
126
ref
refl
nil
"t"
4
ref
var
136
def
108
ref
nil
cons
137
def
cons
nil
cons
nil
cons
cons
138
def
27
ref
136
ref
varTerm
139
def
appTerm
140
def
128
ref
appTerm
141
def
assume
sym
nil
128
ref
axiom
142
def
eqMp
139
ref
assume
142
ref
deductAntisym
deductAntisym
143
def
subst
108
ref
assume
144
def
eqMp
appThm
nil
136
ref
110
ref
nil
cons
145
def
cons
nil
cons
nil
cons
cons
146
def
143
ref
subst
110
ref
assume
147
def
eqMp
appThm
absThm
eqMp
148
def
nil
"P"
4
ref
var
149
def
137
ref
cons
150
def
"Q"
4
ref
var
151
def
145
ref
cons
nil
cons
152
def
cons
nil
cons
cons
27
ref
refl
153
def
125
ref
126
remove
149
ref
varTerm
154
def
appTerm
155
def
151
ref
varTerm
156
def
appTerm
absTerm
157
def
91
ref
94
ref
108
ref
absTerm
absTerm
158
def
appTerm
betaConv
158
ref
154
ref
appTerm
betaConv
156
ref
refl
159
def
appThm
94
ref
154
ref
absTerm
156
ref
appTerm
betaConv
trans
trans
appThm
129
ref
158
ref
appTerm
betaConv
158
ref
128
ref
appTerm
betaConv
128
ref
refl
160
def
appThm
94
ref
128
ref
absTerm
128
ref
appTerm
betaConv
trans
trans
appThm
27
ref
24
ref
154
ref
appTerm
161
def
156
ref
appTerm
162
def
appTerm
refl
94
ref
124
remove
125
remove
155
remove
110
ref
appTerm
absTerm
appTerm
129
ref
appTerm
absTerm
156
ref
appTerm
betaConv
appThm
132
ref
161
remove
appTerm
refl
133
remove
154
ref
appTerm
betaConv
appThm
134
remove
154
ref
refl
163
def
appThm
eqMp
159
ref
appThm
eqMp
162
remove
assume
eqMp
164
def
158
remove
refl
appThm
eqMp
sym
142
ref
eqMp
165
def
subst
166
def
deductAntisym
eqMp
122
remove
111
ref
assume
eqMp
sym
144
ref
eqMp
153
ref
127
remove
91
ref
94
ref
110
ref
absTerm
167
def
absTerm
168
def
appTerm
betaConv
168
ref
108
ref
appTerm
betaConv
118
ref
appThm
167
ref
110
ref
appTerm
betaConv
trans
trans
appThm
129
remove
168
ref
appTerm
betaConv
168
ref
128
ref
appTerm
betaConv
160
remove
appThm
167
ref
128
ref
appTerm
betaConv
trans
trans
169
def
appThm
135
remove
114
ref
assume
eqMp
168
ref
refl
170
def
appThm
eqMp
sym
142
ref
eqMp
171
def
proveHyp
172
def
deductAntisym
173
def
subst
proveHyp
nil
"NUM_REP"
6
ref
var
174
def
93
ref
nil
cons
cons
nil
cons
nil
cons
cons
nil
91
ref
92
remove
174
ref
varTerm
175
def
appTerm
88
ref
appTerm
176
def
nil
cons
177
def
cons
94
ref
24
ref
24
ref
175
ref
66
ref
appTerm
178
def
appTerm
13
ref
69
ref
12
ref
175
ref
70
ref
appTerm
179
def
appTerm
180
def
175
ref
71
ref
appTerm
181
def
appTerm
182
def
absTerm
183
def
appTerm
184
def
appTerm
185
def
appTerm
24
ref
8
ref
9
ref
101
remove
13
ref
3
ref
12
ref
175
ref
19
ref
appTerm
186
def
appTerm
187
def
80
ref
appTerm
188
def
absTerm
189
def
appTerm
190
def
appTerm
absTerm
appTerm
191
def
appTerm
13
ref
3
ref
27
ref
186
ref
appTerm
192
def
68
ref
33
ref
69
ref
73
ref
179
ref
appTerm
193
def
absTerm
194
def
appTerm
195
def
appTerm
196
def
appTerm
197
def
absTerm
198
def
appTerm
199
def
appTerm
200
def
appTerm
nil
cons
201
def
cons
nil
cons
cons
nil
cons
cons
202
def
123
ref
subst
202
remove
171
remove
148
remove
deductAntisym
203
def
subst
nil
"P"
7
remove
var
204
def
174
ref
8
ref
9
ref
12
ref
190
ref
appTerm
13
ref
3
ref
12
ref
196
ref
appTerm
205
def
79
ref
appTerm
206
def
absTerm
207
def
appTerm
208
def
appTerm
209
def
absTerm
210
def
appTerm
211
def
absTerm
212
def
nil
cons
cons
213
def
nil
cons
nil
cons
cons
"A"
16
remove
cons
nil
cons
214
def
nil
nil
cons
215
def
cons
27
ref
0
ref
1
ref
1
ref
"A"
varType
216
def
5
ref
cons
opType
217
def
5
ref
cons
opType
218
def
constTerm
219
def
"P"
217
ref
var
220
def
varTerm
221
def
appTerm
222
def
appTerm
refl
"p"
217
ref
var
223
def
15
ref
1
ref
217
ref
218
ref
nil
cons
cons
opType
constTerm
223
ref
varTerm
224
def
appTerm
"x"
216
ref
var
225
def
128
ref
absTerm
226
def
appTerm
absTerm
227
def
221
ref
appTerm
betaConv
228
def
appThm
nil
15
ref
1
ref
218
ref
1
ref
218
ref
5
ref
cons
opType
229
def
nil
cons
cons
opType
constTerm
230
def
219
ref
appTerm
227
remove
appTerm
axiom
221
ref
refl
231
def
appThm
232
def
eqMp
sym
233
def
subst
234
def
subst
174
ref
nil
136
ref
211
remove
nil
cons
235
def
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
204
ref
210
ref
nil
cons
cons
236
def
nil
cons
nil
cons
cons
234
ref
subst
9
ref
nil
136
ref
209
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
91
ref
190
ref
nil
cons
237
def
cons
238
def
94
ref
208
remove
nil
cons
239
def
cons
nil
cons
cons
nil
cons
cons
240
def
123
ref
subst
240
ref
203
ref
subst
nil
"P"
6
ref
var
241
def
207
ref
nil
cons
cons
242
def
nil
cons
nil
cons
cons
"A"
22
ref
cons
243
def
nil
cons
244
def
215
ref
cons
245
def
233
ref
subst
246
def
subst
3
ref
nil
136
ref
206
remove
nil
cons
247
def
cons
nil
cons
nil
cons
cons
143
ref
subst
91
ref
109
ref
108
ref
appTerm
248
def
absTerm
249
def
67
ref
appTerm
250
def
betaConv
nil
"P"
10
remove
var
251
def
249
ref
nil
cons
cons
252
def
nil
cons
nil
cons
cons
"A"
5
ref
cons
nil
cons
253
def
215
ref
cons
254
def
233
ref
subst
255
def
subst
91
ref
nil
136
ref
248
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
91
ref
137
ref
cons
256
def
94
ref
137
ref
cons
nil
cons
257
def
cons
nil
cons
cons
258
def
123
ref
subst
258
remove
203
ref
subst
144
remove
eqMp
nil
150
ref
151
ref
137
ref
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
259
def
nil
91
ref
0
ref
131
remove
constTerm
260
def
249
ref
appTerm
nil
cons
cons
261
def
94
ref
250
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
252
ref
"x"
4
ref
var
262
def
67
ref
nil
cons
263
def
cons
nil
cons
cons
nil
cons
cons
nil
91
ref
222
ref
nil
cons
264
def
cons
94
ref
221
ref
225
ref
varTerm
265
def
appTerm
266
def
nil
cons
267
def
cons
nil
cons
cons
nil
cons
cons
268
def
123
ref
subst
268
remove
203
ref
subst
27
ref
266
ref
appTerm
refl
226
remove
265
ref
appTerm
betaConv
appThm
228
remove
232
remove
222
remove
assume
eqMp
eqMp
265
ref
refl
269
def
appThm
eqMp
sym
142
ref
eqMp
eqMp
nil
149
ref
264
remove
cons
151
ref
267
ref
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
270
def
subst
eqMp
eqMp
nil
91
ref
12
ref
67
ref
appTerm
271
def
67
ref
appTerm
272
def
nil
cons
cons
94
ref
12
ref
195
ref
appTerm
273
def
78
ref
appTerm
274
def
nil
cons
cons
nil
cons
275
def
cons
nil
cons
cons
203
ref
subst
proveHyp
nil
241
ref
69
ref
12
ref
193
ref
appTerm
276
def
76
remove
appTerm
277
def
absTerm
278
def
nil
cons
cons
nil
cons
nil
cons
cons
246
ref
subst
69
ref
nil
136
ref
277
remove
nil
cons
279
def
cons
nil
cons
nil
cons
cons
143
ref
subst
249
remove
72
ref
appTerm
280
def
betaConv
259
ref
nil
261
remove
94
ref
280
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
252
remove
262
ref
72
ref
nil
cons
281
def
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
12
ref
72
ref
appTerm
72
remove
appTerm
282
def
nil
cons
cons
94
ref
180
remove
75
ref
appTerm
283
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
203
ref
subst
proveHyp
nil
3
ref
70
ref
nil
cons
284
def
cons
nil
cons
nil
cons
cons
nil
136
ref
188
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
285
def
189
ref
19
ref
appTerm
286
def
betaConv
nil
238
remove
94
ref
286
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
244
ref
241
ref
189
remove
nil
cons
cons
287
def
44
ref
19
ref
nil
cons
cons
nil
cons
288
def
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
subst
sym
142
ref
eqMp
eqMp
nil
91
ref
24
ref
282
remove
appTerm
283
remove
appTerm
nil
cons
cons
94
ref
279
remove
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
"q2"
4
ref
var
289
def
75
remove
nil
cons
cons
"p2"
4
ref
var
290
def
281
ref
cons
"q1"
4
ref
var
291
def
179
ref
nil
cons
292
def
cons
"p1"
4
ref
var
293
def
281
ref
cons
nil
cons
cons
cons
cons
nil
cons
cons
289
ref
12
ref
24
ref
12
ref
293
ref
varTerm
294
def
appTerm
290
ref
varTerm
295
def
appTerm
appTerm
12
ref
291
ref
varTerm
296
def
appTerm
289
ref
varTerm
297
def
appTerm
appTerm
appTerm
298
def
12
ref
24
ref
294
ref
appTerm
296
ref
appTerm
appTerm
24
ref
295
ref
appTerm
297
ref
appTerm
appTerm
appTerm
absTerm
299
def
297
ref
appTerm
300
def
betaConv
291
ref
260
ref
299
ref
appTerm
301
def
absTerm
302
def
296
ref
appTerm
303
def
betaConv
290
ref
260
ref
302
ref
appTerm
304
def
absTerm
305
def
295
ref
appTerm
306
def
betaConv
293
ref
260
ref
305
ref
appTerm
307
def
absTerm
308
def
294
ref
appTerm
309
def
betaConv
nil
260
ref
308
ref
appTerm
310
def
axiom
nil
91
ref
310
remove
nil
cons
cons
94
ref
309
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
308
remove
nil
cons
cons
262
ref
294
ref
nil
cons
cons
nil
cons
311
def
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
307
remove
nil
cons
cons
94
ref
306
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
305
remove
nil
cons
cons
262
ref
295
ref
nil
cons
cons
nil
cons
312
def
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
304
remove
nil
cons
cons
94
ref
303
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
302
remove
nil
cons
cons
262
ref
296
ref
nil
cons
cons
nil
cons
313
def
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
301
remove
nil
cons
cons
94
ref
300
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
299
remove
nil
cons
cons
262
ref
297
ref
nil
cons
cons
nil
cons
314
def
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
absThm
eqMp
nil
91
ref
13
ref
278
remove
appTerm
nil
cons
cons
275
remove
cons
nil
cons
cons
173
ref
subst
proveHyp
12
ref
refl
315
def
13
ref
refl
316
def
69
ref
315
ref
194
ref
70
ref
appTerm
317
def
betaConv
318
def
appThm
77
ref
70
ref
appTerm
betaConv
319
def
appThm
absThm
appThm
appThm
315
ref
33
ref
refl
320
def
69
ref
318
ref
absThm
appThm
appThm
320
ref
69
ref
319
remove
absThm
appThm
appThm
appThm
nil
"p"
6
ref
var
321
def
194
ref
nil
cons
322
def
cons
"q"
6
ref
var
323
def
77
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
245
ref
"q"
217
ref
var
324
def
12
ref
219
ref
225
ref
12
ref
224
ref
265
ref
appTerm
325
def
appTerm
326
def
324
ref
varTerm
327
def
265
ref
appTerm
328
def
appTerm
absTerm
appTerm
appTerm
12
ref
32
ref
218
ref
constTerm
329
def
225
ref
325
ref
absTerm
330
def
appTerm
331
def
appTerm
329
ref
225
ref
328
ref
absTerm
332
def
appTerm
333
def
appTerm
appTerm
absTerm
334
def
327
ref
appTerm
335
def
betaConv
223
ref
0
ref
229
remove
constTerm
336
def
334
ref
appTerm
337
def
absTerm
338
def
224
ref
appTerm
339
def
betaConv
nil
336
ref
338
ref
appTerm
340
def
axiom
nil
91
ref
340
remove
nil
cons
cons
94
ref
339
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
"A"
217
ref
nil
cons
341
def
cons
nil
cons
342
def
"P"
218
remove
var
343
def
338
remove
nil
cons
cons
"x"
217
ref
var
344
def
224
ref
nil
cons
345
def
cons
nil
cons
346
def
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
337
remove
nil
cons
cons
94
ref
335
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
342
ref
343
ref
334
remove
nil
cons
cons
344
remove
327
ref
nil
cons
cons
nil
cons
347
def
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
subst
eqMp
eqMp
eqMp
nil
91
ref
24
ref
272
remove
appTerm
274
remove
appTerm
nil
cons
cons
94
ref
247
ref
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
289
ref
78
remove
nil
cons
cons
290
ref
263
ref
cons
291
ref
195
remove
nil
cons
348
def
cons
293
ref
263
ref
cons
nil
cons
cons
cons
cons
nil
cons
cons
289
remove
298
remove
12
ref
14
ref
294
ref
appTerm
296
ref
appTerm
appTerm
14
ref
295
ref
appTerm
297
ref
appTerm
appTerm
appTerm
absTerm
349
def
297
remove
appTerm
350
def
betaConv
291
remove
260
ref
349
ref
appTerm
351
def
absTerm
352
def
296
remove
appTerm
353
def
betaConv
290
remove
260
ref
352
ref
appTerm
354
def
absTerm
355
def
295
remove
appTerm
356
def
betaConv
293
remove
260
ref
355
ref
appTerm
357
def
absTerm
358
def
294
remove
appTerm
359
def
betaConv
nil
260
ref
358
ref
appTerm
360
def
axiom
nil
91
ref
360
remove
nil
cons
cons
94
ref
359
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
358
remove
nil
cons
cons
311
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
357
remove
nil
cons
cons
94
ref
356
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
355
remove
nil
cons
cons
312
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
354
remove
nil
cons
cons
94
ref
353
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
352
remove
nil
cons
cons
313
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
351
remove
nil
cons
cons
94
ref
350
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
349
remove
nil
cons
cons
314
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
absThm
eqMp
eqMp
nil
149
ref
237
ref
cons
151
ref
239
ref
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
24
ref
refl
361
def
nil
91
ref
178
ref
nil
cons
362
def
cons
94
ref
13
ref
3
ref
271
remove
186
ref
appTerm
363
def
absTerm
364
def
appTerm
365
def
nil
cons
366
def
cons
nil
cons
cons
nil
cons
cons
367
def
315
ref
27
ref
108
ref
appTerm
368
def
110
ref
appTerm
369
def
assume
370
def
appThm
118
ref
appThm
sym
nil
91
ref
145
ref
cons
371
def
94
ref
145
ref
cons
nil
cons
372
def
cons
nil
cons
cons
373
def
123
ref
subst
373
remove
203
ref
subst
147
remove
eqMp
nil
149
ref
145
ref
cons
152
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
374
def
eqMp
375
def
nil
91
ref
111
ref
nil
cons
376
def
cons
377
def
94
ref
12
ref
110
ref
appTerm
378
def
108
ref
appTerm
nil
cons
379
def
cons
nil
cons
380
def
cons
nil
cons
cons
203
ref
subst
proveHyp
378
ref
refl
370
remove
appThm
sym
374
remove
eqMp
381
def
eqMp
nil
371
ref
257
ref
cons
nil
cons
cons
173
ref
subst
nil
149
ref
376
ref
cons
382
def
151
ref
379
remove
cons
nil
cons
383
def
cons
nil
cons
cons
384
def
153
ref
157
remove
168
ref
appTerm
betaConv
168
remove
154
ref
appTerm
betaConv
159
ref
appThm
167
remove
156
ref
appTerm
betaConv
trans
trans
appThm
169
remove
appThm
164
remove
170
remove
appThm
eqMp
sym
142
ref
eqMp
385
def
subst
eqMp
173
ref
384
remove
165
ref
subst
eqMp
deductAntisym
deductAntisym
386
def
subst
367
ref
123
ref
subst
367
remove
203
ref
subst
nil
241
ref
364
ref
nil
cons
cons
387
def
nil
cons
nil
cons
cons
246
ref
subst
388
def
3
ref
nil
136
ref
363
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
389
def
nil
91
ref
263
ref
cons
390
def
94
ref
186
ref
nil
cons
391
def
cons
nil
cons
392
def
cons
nil
cons
cons
393
def
123
ref
subst
394
def
393
ref
203
ref
subst
395
def
175
ref
refl
396
def
67
remove
assume
appThm
sym
178
ref
assume
eqMp
eqMp
nil
149
ref
263
remove
cons
397
def
151
ref
391
ref
cons
nil
cons
398
def
cons
nil
cons
cons
165
ref
subst
399
def
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
149
ref
362
ref
cons
151
ref
366
ref
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
91
ref
12
ref
178
ref
appTerm
365
ref
appTerm
nil
cons
cons
94
ref
12
ref
365
ref
appTerm
178
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
203
ref
subst
proveHyp
nil
91
ref
366
ref
cons
400
def
94
ref
362
ref
cons
nil
cons
401
def
cons
nil
cons
cons
402
def
123
ref
subst
402
remove
203
ref
subst
66
ref
refl
403
def
nil
91
ref
18
ref
66
ref
appTerm
404
def
66
ref
appTerm
nil
cons
cons
401
remove
cons
nil
cons
cons
173
ref
subst
proveHyp
364
ref
66
ref
appTerm
405
def
betaConv
nil
400
ref
94
ref
405
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
244
ref
387
ref
44
ref
66
ref
nil
cons
406
def
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
149
ref
366
remove
cons
407
def
151
ref
362
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
appThm
nil
91
ref
184
ref
nil
cons
408
def
cons
409
def
94
ref
13
ref
3
ref
13
ref
69
ref
276
remove
186
ref
appTerm
410
def
absTerm
411
def
appTerm
412
def
absTerm
413
def
appTerm
414
def
nil
cons
415
def
cons
nil
cons
cons
nil
cons
cons
416
def
386
ref
subst
416
ref
123
ref
subst
416
remove
203
ref
subst
nil
241
ref
413
ref
nil
cons
cons
417
def
nil
cons
nil
cons
cons
246
ref
subst
3
ref
nil
136
ref
412
ref
nil
cons
418
def
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
241
ref
411
ref
nil
cons
cons
419
def
nil
cons
nil
cons
cons
246
ref
subst
420
def
69
ref
nil
136
ref
410
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
421
def
nil
91
ref
193
ref
nil
cons
422
def
cons
423
def
392
ref
cons
nil
cons
cons
424
def
123
ref
subst
425
def
424
ref
203
ref
subst
426
def
396
remove
nil
149
ref
281
remove
cons
151
ref
292
ref
cons
nil
cons
cons
nil
cons
cons
427
def
165
ref
subst
appThm
sym
427
remove
385
ref
subst
nil
91
ref
292
ref
cons
94
ref
181
ref
nil
cons
428
def
cons
nil
cons
429
def
cons
nil
cons
cons
430
def
173
ref
subst
proveHyp
183
ref
70
ref
appTerm
431
def
betaConv
nil
409
remove
94
ref
431
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
244
ref
241
ref
183
remove
nil
cons
cons
432
def
44
ref
284
ref
cons
nil
cons
433
def
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
eqMp
eqMp
nil
149
ref
422
remove
cons
434
def
398
ref
cons
nil
cons
cons
165
ref
subst
435
def
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
149
ref
408
ref
cons
151
ref
415
ref
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
91
ref
12
ref
184
ref
appTerm
414
ref
appTerm
nil
cons
cons
94
ref
12
ref
414
remove
appTerm
184
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
203
ref
subst
proveHyp
nil
91
ref
415
ref
cons
436
def
94
ref
408
ref
cons
nil
cons
cons
nil
cons
cons
437
def
123
ref
subst
437
remove
203
ref
subst
nil
432
remove
nil
cons
nil
cons
cons
246
ref
subst
69
ref
nil
136
ref
182
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
430
ref
123
ref
subst
430
remove
203
ref
subst
71
ref
refl
nil
91
ref
18
ref
71
ref
appTerm
438
def
71
ref
appTerm
439
def
nil
cons
cons
94
ref
292
ref
cons
nil
cons
cons
nil
cons
cons
203
ref
subst
proveHyp
179
ref
assume
eqMp
nil
91
ref
24
ref
439
remove
appTerm
179
remove
appTerm
nil
cons
cons
429
remove
cons
nil
cons
cons
173
ref
subst
proveHyp
"i'"
2
ref
var
440
def
12
ref
24
ref
438
remove
56
ref
440
remove
varTerm
441
def
appTerm
appTerm
appTerm
175
ref
441
remove
appTerm
appTerm
appTerm
181
remove
appTerm
absTerm
442
def
70
ref
appTerm
443
def
betaConv
413
remove
71
ref
appTerm
444
def
betaConv
nil
436
remove
94
ref
444
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
244
ref
417
remove
44
ref
71
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
13
ref
442
ref
appTerm
nil
cons
cons
94
ref
443
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
241
ref
442
remove
nil
cons
cons
433
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
149
ref
292
remove
cons
151
ref
428
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
149
ref
415
remove
cons
151
ref
408
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
316
ref
3
ref
nil
91
ref
418
ref
cons
445
def
94
ref
273
ref
186
ref
appTerm
446
def
nil
cons
447
def
cons
nil
cons
cons
nil
cons
cons
448
def
386
ref
subst
448
ref
123
ref
subst
448
remove
203
ref
subst
nil
91
ref
348
ref
cons
449
def
392
ref
cons
nil
cons
cons
450
def
123
ref
subst
451
def
450
ref
203
ref
subst
452
def
nil
445
ref
392
ref
cons
nil
cons
cons
453
def
173
ref
subst
nil
449
ref
94
ref
12
ref
412
ref
appTerm
454
def
186
ref
appTerm
455
def
nil
cons
456
def
cons
nil
cons
457
def
cons
nil
cons
cons
173
ref
subst
nil
241
ref
69
ref
12
ref
317
ref
appTerm
455
ref
appTerm
458
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
246
ref
subst
69
ref
nil
136
ref
458
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
91
ref
317
ref
nil
cons
459
def
cons
457
ref
cons
nil
cons
cons
460
def
123
ref
subst
460
remove
203
ref
subst
318
ref
317
remove
assume
eqMp
nil
423
remove
457
remove
cons
nil
cons
cons
461
def
173
ref
subst
proveHyp
461
ref
123
ref
subst
461
remove
203
ref
subst
453
ref
123
ref
subst
453
remove
203
ref
subst
424
remove
173
ref
subst
411
remove
70
ref
appTerm
462
def
betaConv
nil
445
remove
94
ref
462
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
244
ref
419
remove
433
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
149
ref
418
ref
cons
463
def
398
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
nil
434
remove
151
ref
456
remove
cons
nil
cons
464
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
149
ref
459
remove
cons
464
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
91
ref
13
ref
44
ref
12
ref
194
remove
46
ref
appTerm
appTerm
455
ref
appTerm
absTerm
appTerm
nil
cons
cons
94
ref
273
remove
455
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
241
ref
322
remove
cons
465
def
464
remove
cons
nil
cons
cons
nil
91
ref
219
ref
225
ref
12
ref
266
ref
appTerm
466
def
156
ref
appTerm
467
def
absTerm
468
def
appTerm
469
def
nil
cons
470
def
cons
471
def
94
ref
12
ref
329
ref
221
ref
appTerm
472
def
appTerm
473
def
156
ref
appTerm
nil
cons
474
def
cons
nil
cons
cons
nil
cons
cons
475
def
123
ref
subst
475
remove
203
ref
subst
nil
91
ref
472
ref
nil
cons
476
def
cons
477
def
94
ref
156
ref
nil
cons
478
def
cons
nil
cons
479
def
cons
nil
cons
cons
480
def
123
ref
subst
480
remove
203
ref
subst
nil
471
ref
479
ref
cons
nil
cons
cons
481
def
173
ref
subst
94
ref
12
ref
219
ref
225
ref
466
remove
110
ref
appTerm
absTerm
appTerm
appTerm
110
ref
appTerm
absTerm
482
def
156
ref
appTerm
483
def
betaConv
nil
477
remove
94
ref
260
ref
482
ref
appTerm
484
def
nil
cons
485
def
cons
nil
cons
cons
nil
cons
cons
486
def
173
ref
subst
27
ref
472
remove
appTerm
487
def
refl
223
ref
260
ref
94
ref
12
ref
219
ref
225
ref
326
ref
110
ref
appTerm
absTerm
appTerm
appTerm
110
ref
appTerm
absTerm
appTerm
absTerm
488
def
221
ref
appTerm
betaConv
appThm
nil
230
remove
329
ref
appTerm
488
remove
appTerm
axiom
231
remove
appThm
eqMp
489
def
nil
91
ref
487
remove
484
ref
appTerm
nil
cons
cons
94
ref
473
remove
484
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
486
remove
nil
91
ref
369
ref
nil
cons
490
def
cons
491
def
94
ref
376
ref
cons
nil
cons
492
def
cons
nil
cons
cons
493
def
123
ref
subst
493
remove
203
ref
subst
375
remove
eqMp
nil
149
ref
490
remove
cons
494
def
151
ref
376
remove
cons
nil
cons
495
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
496
def
subst
eqMp
eqMp
nil
91
ref
485
remove
cons
94
ref
483
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
482
remove
nil
cons
cons
262
ref
478
ref
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
149
ref
476
remove
cons
151
ref
478
ref
cons
nil
cons
497
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
nil
149
ref
470
ref
cons
498
def
151
ref
474
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
499
def
subst
eqMp
eqMp
eqMp
eqMp
nil
149
ref
348
ref
cons
500
def
398
ref
cons
nil
cons
cons
165
ref
subst
501
def
deductAntisym
eqMp
eqMp
nil
463
remove
151
ref
447
ref
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
91
ref
454
remove
446
ref
appTerm
nil
cons
cons
94
ref
12
ref
446
ref
appTerm
412
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
203
ref
subst
proveHyp
nil
91
ref
447
ref
cons
94
ref
418
ref
cons
nil
cons
cons
nil
cons
cons
502
def
123
ref
subst
502
remove
203
ref
subst
420
remove
69
ref
421
remove
425
remove
426
remove
318
remove
sym
193
remove
assume
eqMp
244
ref
465
remove
433
ref
cons
nil
cons
cons
489
remove
sym
nil
251
ref
151
ref
12
ref
469
ref
appTerm
503
def
156
ref
appTerm
504
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
255
ref
subst
151
ref
nil
136
ref
504
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
481
ref
123
ref
subst
481
remove
203
ref
subst
nil
91
ref
267
ref
cons
479
ref
cons
nil
cons
cons
505
def
173
ref
subst
506
def
468
ref
265
ref
appTerm
507
def
betaConv
nil
471
ref
94
ref
507
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
"A"
216
ref
nil
cons
508
def
cons
509
def
nil
cons
510
def
220
ref
468
remove
nil
cons
cons
511
def
225
ref
265
ref
nil
cons
512
def
cons
nil
cons
513
def
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
514
def
eqMp
eqMp
nil
498
ref
497
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
515
def
subst
proveHyp
450
remove
173
ref
subst
516
def
proveHyp
446
ref
assume
eqMp
eqMp
435
remove
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
149
ref
447
ref
cons
151
ref
418
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
absThm
appThm
trans
appThm
nil
91
ref
24
ref
365
remove
appTerm
13
ref
3
ref
446
remove
absTerm
517
def
appTerm
518
def
appTerm
519
def
nil
cons
520
def
cons
521
def
94
ref
13
ref
3
ref
205
ref
186
ref
appTerm
522
def
absTerm
523
def
appTerm
524
def
nil
cons
525
def
cons
nil
cons
cons
nil
cons
cons
526
def
386
ref
subst
526
ref
123
ref
subst
526
remove
203
ref
subst
nil
241
ref
523
ref
nil
cons
cons
527
def
nil
cons
nil
cons
cons
246
ref
subst
528
def
3
ref
nil
136
ref
522
remove
nil
cons
529
def
cons
nil
cons
nil
cons
cons
143
ref
subst
530
def
nil
91
ref
196
ref
nil
cons
531
def
cons
532
def
392
ref
cons
nil
cons
cons
533
def
123
ref
subst
534
def
533
ref
203
ref
subst
535
def
nil
521
remove
392
ref
cons
nil
cons
cons
536
def
173
ref
subst
nil
449
remove
94
ref
12
ref
519
ref
appTerm
537
def
186
ref
appTerm
nil
cons
538
def
cons
nil
cons
539
def
cons
nil
cons
cons
540
def
123
ref
subst
540
remove
203
ref
subst
536
ref
123
ref
subst
541
def
536
remove
203
ref
subst
542
def
516
remove
517
ref
19
ref
appTerm
543
def
betaConv
nil
407
remove
151
ref
518
remove
nil
cons
544
def
cons
nil
cons
cons
nil
cons
cons
545
def
385
ref
subst
nil
91
ref
544
ref
cons
94
ref
543
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
241
ref
517
remove
nil
cons
cons
546
def
288
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
149
ref
520
ref
cons
547
def
398
ref
cons
nil
cons
cons
165
ref
subst
548
def
deductAntisym
eqMp
eqMp
nil
500
remove
151
ref
538
ref
cons
nil
cons
549
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
390
remove
539
remove
cons
nil
cons
cons
550
def
123
ref
subst
550
remove
203
ref
subst
541
remove
542
remove
393
remove
173
ref
subst
364
remove
19
ref
appTerm
551
def
betaConv
545
remove
165
ref
subst
nil
400
ref
94
ref
551
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
387
remove
288
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
eqMp
548
remove
deductAntisym
eqMp
eqMp
nil
397
ref
549
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
397
ref
151
ref
348
remove
cons
552
def
"R"
4
ref
var
553
def
538
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
91
ref
12
ref
156
ref
appTerm
554
def
553
ref
varTerm
555
def
appTerm
556
def
nil
cons
cons
94
ref
555
ref
nil
cons
557
def
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
nil
91
ref
12
ref
154
ref
appTerm
558
def
555
ref
appTerm
nil
cons
cons
94
ref
12
ref
556
remove
appTerm
555
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
"r"
4
ref
var
559
def
12
ref
558
ref
559
ref
varTerm
560
def
appTerm
appTerm
561
def
12
ref
554
ref
560
ref
appTerm
appTerm
560
ref
appTerm
appTerm
absTerm
562
def
555
remove
appTerm
563
def
betaConv
27
ref
14
ref
154
ref
appTerm
564
def
156
ref
appTerm
565
def
appTerm
refl
94
ref
260
ref
559
ref
561
remove
12
ref
378
ref
560
ref
appTerm
566
def
appTerm
567
def
560
ref
appTerm
568
def
appTerm
absTerm
appTerm
absTerm
156
ref
appTerm
betaConv
appThm
132
ref
564
remove
appTerm
refl
91
ref
94
ref
260
ref
559
ref
12
ref
109
ref
560
ref
appTerm
569
def
appTerm
568
remove
appTerm
absTerm
appTerm
absTerm
absTerm
570
def
154
ref
appTerm
betaConv
appThm
nil
120
remove
14
ref
appTerm
570
remove
appTerm
axiom
163
ref
appThm
eqMp
159
remove
appThm
eqMp
571
def
565
remove
assume
eqMp
nil
91
ref
260
ref
562
ref
appTerm
nil
cons
cons
94
ref
563
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
562
remove
nil
cons
cons
262
ref
557
remove
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
eqMp
572
def
subst
proveHyp
proveHyp
eqMp
eqMp
nil
149
ref
531
ref
cons
398
ref
cons
nil
cons
cons
165
ref
subst
573
def
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
547
remove
151
ref
525
ref
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
91
ref
537
remove
524
ref
appTerm
nil
cons
cons
94
ref
12
ref
524
remove
appTerm
519
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
203
ref
subst
proveHyp
nil
91
ref
525
ref
cons
574
def
94
ref
520
ref
cons
nil
cons
cons
nil
cons
cons
575
def
123
ref
subst
575
remove
203
ref
subst
388
remove
3
ref
389
remove
394
remove
395
remove
nil
574
ref
392
remove
cons
nil
cons
cons
576
def
173
ref
subst
577
def
nil
397
remove
552
remove
nil
cons
cons
nil
cons
cons
578
def
571
remove
sym
579
def
nil
251
ref
136
ref
12
ref
558
ref
139
ref
appTerm
580
def
appTerm
12
ref
554
remove
139
ref
appTerm
581
def
appTerm
139
ref
appTerm
582
def
appTerm
583
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
255
ref
subst
584
def
136
ref
nil
136
ref
583
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
585
def
nil
91
ref
580
ref
nil
cons
586
def
cons
94
ref
582
remove
nil
cons
587
def
cons
nil
cons
cons
nil
cons
cons
588
def
123
ref
subst
589
def
588
remove
203
ref
subst
590
def
nil
91
ref
581
ref
nil
cons
591
def
cons
94
ref
139
ref
nil
cons
592
def
cons
nil
cons
593
def
cons
nil
cons
cons
594
def
123
ref
subst
595
def
594
remove
203
ref
subst
596
def
nil
91
ref
154
ref
nil
cons
597
def
cons
598
def
593
ref
cons
nil
cons
cons
173
ref
subst
580
remove
assume
eqMp
eqMp
nil
149
ref
591
remove
cons
151
ref
592
ref
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
599
def
deductAntisym
eqMp
eqMp
nil
149
ref
586
remove
cons
151
ref
587
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
600
def
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
subst
576
ref
123
ref
subst
576
remove
203
ref
subst
533
remove
173
ref
subst
523
remove
19
ref
appTerm
601
def
betaConv
nil
574
remove
94
ref
601
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
244
ref
527
remove
288
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
149
ref
525
remove
cons
602
def
398
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
603
def
proveHyp
eqMp
eqMp
399
remove
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
400
remove
94
ref
544
remove
cons
nil
cons
cons
nil
cons
cons
203
ref
subst
proveHyp
nil
546
remove
nil
cons
nil
cons
cons
246
ref
subst
3
ref
nil
136
ref
447
remove
cons
nil
cons
nil
cons
cons
143
ref
subst
451
remove
452
remove
577
remove
578
remove
579
remove
584
remove
136
ref
585
remove
589
remove
590
remove
595
remove
596
remove
nil
91
ref
478
remove
cons
593
remove
cons
nil
cons
cons
173
ref
subst
581
remove
assume
eqMp
eqMp
599
remove
deductAntisym
eqMp
eqMp
600
remove
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
subst
603
remove
proveHyp
eqMp
eqMp
501
remove
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
eqMp
nil
602
remove
151
ref
520
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
trans
sym
604
def
528
remove
3
ref
530
remove
534
remove
535
remove
192
ref
refl
88
remove
19
ref
appTerm
betaConv
appThm
176
remove
assume
19
ref
refl
appThm
eqMp
605
def
sym
nil
204
ref
86
ref
nil
cons
cons
606
def
nil
cons
nil
cons
cons
234
ref
subst
9
ref
nil
136
ref
85
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
91
ref
83
remove
nil
cons
607
def
cons
608
def
94
ref
80
ref
nil
cons
609
def
cons
nil
cons
610
def
cons
nil
cons
cons
611
def
123
ref
subst
611
ref
203
ref
subst
nil
532
ref
610
ref
cons
nil
cons
cons
173
ref
subst
82
ref
19
ref
appTerm
612
def
betaConv
nil
608
ref
94
ref
612
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
244
ref
241
ref
82
remove
nil
cons
cons
288
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
81
ref
nil
cons
cons
94
ref
205
remove
80
ref
appTerm
613
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
207
remove
19
ref
appTerm
614
def
betaConv
nil
287
remove
nil
cons
nil
cons
cons
246
ref
subst
3
ref
285
remove
nil
91
ref
391
ref
cons
615
def
610
remove
cons
nil
cons
cons
616
def
123
ref
subst
616
remove
203
ref
subst
611
remove
173
ref
subst
86
remove
74
ref
appTerm
617
def
betaConv
nil
615
ref
94
ref
87
ref
nil
cons
618
def
cons
nil
cons
cons
nil
cons
cons
619
def
173
ref
subst
605
remove
nil
91
ref
192
remove
87
ref
appTerm
nil
cons
cons
94
ref
187
ref
87
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
619
remove
496
ref
subst
eqMp
eqMp
nil
91
ref
618
remove
cons
94
ref
617
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
214
ref
606
remove
"x"
6
remove
var
620
def
74
ref
nil
cons
621
def
cons
nil
cons
622
def
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
149
ref
391
remove
cons
151
ref
609
ref
cons
nil
cons
623
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
624
def
240
remove
173
ref
subst
proveHyp
210
remove
74
remove
appTerm
625
def
betaConv
212
ref
175
ref
appTerm
626
def
betaConv
nil
91
ref
8
ref
212
ref
appTerm
nil
cons
cons
627
def
94
ref
626
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
214
ref
213
ref
620
ref
175
ref
nil
cons
cons
nil
cons
628
def
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
235
remove
cons
94
ref
625
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
214
ref
236
remove
622
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
nil
91
ref
239
remove
cons
94
ref
614
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
242
remove
288
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
247
remove
cons
94
ref
12
ref
81
remove
appTerm
613
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
532
remove
94
ref
79
ref
nil
cons
cons
559
ref
609
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
377
ref
94
ref
567
remove
569
ref
appTerm
nil
cons
629
def
cons
nil
cons
cons
nil
cons
cons
630
def
123
ref
subst
630
remove
203
ref
subst
nil
91
ref
566
ref
nil
cons
631
def
cons
94
ref
569
remove
nil
cons
632
def
cons
nil
cons
cons
nil
cons
cons
633
def
123
ref
subst
633
remove
203
ref
subst
nil
256
ref
94
ref
560
ref
nil
cons
634
def
cons
nil
cons
635
def
cons
nil
cons
cons
636
def
123
ref
subst
636
remove
203
ref
subst
172
ref
nil
371
ref
635
remove
cons
nil
cons
cons
173
ref
subst
proveHyp
566
remove
assume
eqMp
eqMp
nil
150
remove
151
ref
634
ref
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
nil
149
ref
631
remove
cons
151
ref
632
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
nil
382
ref
151
ref
629
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
eqMp
eqMp
nil
149
ref
607
remove
cons
637
def
623
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
eqMp
573
remove
deductAntisym
eqMp
638
def
eqMp
absThm
eqMp
639
def
eqMp
nil
91
ref
185
remove
nil
cons
cons
94
ref
200
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
203
ref
subst
proveHyp
8
ref
refl
9
ref
315
ref
nil
174
remove
621
remove
cons
nil
cons
nil
cons
cons
604
remove
subst
appThm
190
ref
refl
appThm
absThm
appThm
nil
204
ref
9
ref
84
remove
190
remove
appTerm
640
def
absTerm
641
def
nil
cons
cons
642
def
nil
cons
nil
cons
cons
234
remove
subst
9
ref
nil
136
ref
640
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
608
remove
94
ref
237
ref
cons
nil
cons
cons
nil
cons
cons
643
def
123
ref
subst
643
remove
203
ref
subst
624
remove
eqMp
nil
637
remove
151
ref
237
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
644
def
nil
91
ref
8
ref
641
ref
appTerm
nil
cons
645
def
cons
646
def
94
ref
199
remove
nil
cons
647
def
cons
nil
cons
648
def
cons
nil
cons
cons
203
ref
subst
proveHyp
nil
241
ref
198
remove
nil
cons
cons
nil
cons
nil
cons
cons
246
ref
subst
3
ref
nil
136
ref
197
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
615
remove
94
ref
531
remove
cons
nil
cons
cons
nil
cons
cons
386
ref
subst
3
ref
187
ref
196
ref
appTerm
649
def
absTerm
650
def
19
ref
appTerm
651
def
betaConv
316
ref
3
ref
187
ref
refl
3
ref
196
ref
absTerm
652
def
19
ref
appTerm
653
def
betaConv
654
def
appThm
absThm
appThm
316
ref
3
ref
12
ref
68
remove
33
ref
69
ref
73
remove
652
ref
70
ref
appTerm
appTerm
absTerm
appTerm
appTerm
appTerm
655
def
refl
654
ref
appThm
absThm
appThm
sym
316
ref
3
ref
315
ref
654
remove
appThm
186
ref
refl
appThm
absThm
appThm
sym
639
remove
eqMp
nil
91
ref
13
ref
3
ref
12
ref
653
ref
appTerm
656
def
186
remove
appTerm
absTerm
appTerm
nil
cons
cons
94
ref
13
ref
3
ref
655
ref
196
remove
appTerm
absTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
9
remove
12
ref
13
ref
3
ref
656
remove
80
remove
appTerm
absTerm
appTerm
appTerm
13
ref
3
ref
655
ref
79
remove
appTerm
absTerm
appTerm
appTerm
absTerm
657
def
175
remove
appTerm
658
def
betaConv
212
remove
652
ref
appTerm
659
def
betaConv
nil
627
remove
94
ref
659
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
214
ref
213
remove
620
ref
652
ref
nil
cons
cons
nil
cons
660
def
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
8
remove
657
ref
appTerm
nil
cons
cons
94
ref
658
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
214
ref
204
ref
657
remove
nil
cons
cons
628
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
91
ref
13
ref
3
ref
655
remove
653
ref
appTerm
absTerm
appTerm
nil
cons
cons
94
ref
13
ref
3
ref
187
remove
653
remove
appTerm
absTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
641
remove
652
remove
appTerm
661
def
betaConv
644
remove
nil
646
remove
94
ref
661
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
214
ref
642
remove
660
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
91
ref
13
ref
650
ref
appTerm
nil
cons
cons
94
ref
651
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
241
ref
650
remove
nil
cons
cons
288
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
649
remove
nil
cons
cons
94
ref
529
remove
cons
nil
cons
cons
nil
cons
cons
203
ref
subst
proveHyp
638
remove
eqMp
eqMp
eqMp
absThm
eqMp
662
def
eqMp
nil
149
ref
645
remove
cons
151
ref
647
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
proveHyp
eqMp
nil
91
ref
191
remove
nil
cons
cons
648
remove
cons
nil
cons
cons
203
ref
subst
proveHyp
662
remove
eqMp
eqMp
proveHyp
eqMp
nil
149
ref
177
remove
cons
151
ref
201
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
subst
eqMp
663
def
nil
149
ref
100
ref
nil
cons
664
def
cons
665
def
151
ref
107
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
666
def
165
ref
subst
proveHyp
667
def
nil
149
ref
95
remove
nil
cons
668
def
cons
669
def
151
ref
99
remove
nil
cons
670
def
cons
nil
cons
cons
nil
cons
cons
671
def
165
ref
subst
672
def
proveHyp
673
def
defineTypeOp
674
def
pop
675
def
pop
676
def
pop
677
def
pop
nil
opType
678
def
5
ref
cons
opType
679
def
5
ref
cons
opType
680
def
constTerm
681
def
refl
682
def
"n"
678
ref
var
683
def
45
ref
refl
684
def
15
ref
1
ref
678
ref
679
ref
nil
cons
685
def
cons
opType
constTerm
686
def
refl
687
def
nil
"_1901"
678
ref
var
688
def
683
ref
varTerm
689
def
nil
cons
690
def
cons
nil
cons
nil
cons
cons
"Number.Natural.suc"
688
ref
677
remove
1
ref
2
ref
678
ref
nil
cons
691
def
cons
opType
constTerm
692
def
56
ref
676
remove
1
ref
678
ref
22
ref
cons
opType
constTerm
693
def
688
remove
varTerm
694
def
appTerm
appTerm
appTerm
absTerm
695
def
defineConst
696
def
pop
697
def
pop
696
remove
694
ref
refl
appThm
695
remove
694
remove
appTerm
betaConv
trans
subst
698
def
appThm
"Number.Natural.zero"
692
ref
66
ref
appTerm
699
def
defineConst
700
def
pop
701
def
pop
700
ref
appThm
appThm
absThm
appThm
sym
nil
91
ref
681
ref
683
ref
45
ref
686
ref
692
ref
56
ref
693
ref
689
ref
appTerm
702
def
appTerm
703
def
appTerm
704
def
appTerm
699
ref
appTerm
705
def
appTerm
absTerm
706
def
appTerm
707
def
nil
cons
cons
nil
cons
nil
cons
cons
368
ref
refl
708
def
nil
136
ref
45
ref
108
ref
appTerm
709
def
nil
cons
710
def
cons
nil
cons
nil
cons
cons
136
ref
27
ref
12
ref
139
ref
appTerm
711
def
"Data.Bool.F"
const
4
ref
constTerm
712
def
appTerm
appTerm
45
ref
139
ref
appTerm
713
def
appTerm
absTerm
714
def
139
ref
appTerm
715
def
betaConv
nil
260
ref
714
ref
appTerm
716
def
axiom
nil
91
ref
716
remove
nil
cons
cons
94
ref
715
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
714
remove
nil
cons
cons
262
ref
592
remove
cons
nil
cons
717
def
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
718
def
subst
appThm
sym
708
remove
138
ref
136
ref
27
ref
45
ref
713
ref
appTerm
appTerm
139
ref
appTerm
absTerm
719
def
139
ref
appTerm
720
def
betaConv
nil
260
ref
719
ref
appTerm
721
def
axiom
nil
91
ref
721
remove
nil
cons
cons
94
ref
720
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
719
remove
nil
cons
cons
717
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
722
def
subst
723
def
appThm
nil
262
ref
137
ref
cons
nil
cons
724
def
nil
cons
cons
254
remove
nil
136
ref
15
ref
1
ref
216
ref
341
remove
cons
opType
constTerm
725
def
265
ref
appTerm
726
def
265
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
269
remove
eqMp
727
def
subst
728
def
subst
trans
sym
142
ref
eqMp
eqMp
729
def
subst
sym
nil
91
ref
45
ref
707
remove
appTerm
730
def
nil
cons
731
def
cons
732
def
94
ref
712
ref
nil
cons
733
def
cons
nil
cons
734
def
cons
nil
cons
cons
735
def
123
ref
subst
735
remove
203
ref
subst
667
ref
nil
91
ref
664
ref
cons
734
ref
cons
nil
cons
cons
736
def
173
ref
subst
proveHyp
nil
"P"
679
ref
var
737
def
"a"
678
ref
var
738
def
686
ref
692
ref
693
ref
738
ref
varTerm
739
def
appTerm
appTerm
740
def
appTerm
739
ref
appTerm
741
def
absTerm
742
def
nil
cons
cons
743
def
nil
cons
nil
cons
cons
"A"
691
ref
cons
nil
cons
744
def
215
ref
cons
745
def
233
ref
subst
746
def
subst
738
ref
nil
136
ref
741
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
687
ref
738
ref
740
remove
absTerm
739
ref
appTerm
betaConv
appThm
738
ref
739
ref
absTerm
739
ref
appTerm
betaConv
appThm
675
remove
739
remove
refl
appThm
eqMp
747
def
eqMp
absThm
eqMp
nil
91
ref
681
ref
742
ref
appTerm
748
def
nil
cons
749
def
cons
750
def
94
ref
12
ref
100
ref
appTerm
712
ref
appTerm
751
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
241
ref
"r"
2
ref
var
752
def
27
ref
93
ref
752
ref
varTerm
753
def
appTerm
754
def
appTerm
18
ref
693
ref
692
ref
753
ref
appTerm
appTerm
appTerm
753
ref
appTerm
755
def
appTerm
756
def
absTerm
757
def
nil
cons
cons
nil
cons
nil
cons
cons
246
ref
subst
752
ref
nil
136
ref
756
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
153
ref
752
ref
755
ref
absTerm
753
ref
appTerm
betaConv
appThm
752
ref
754
ref
absTerm
753
ref
appTerm
betaConv
appThm
674
remove
753
ref
refl
appThm
eqMp
758
def
sym
759
def
eqMp
absThm
eqMp
nil
91
ref
13
ref
757
remove
appTerm
760
def
nil
cons
761
def
cons
762
def
94
ref
12
ref
748
remove
appTerm
763
def
751
remove
appTerm
764
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
61
remove
refl
316
ref
44
ref
684
ref
62
ref
refl
18
ref
64
ref
appTerm
66
ref
appTerm
assume
sym
404
remove
64
ref
appTerm
assume
sym
deductAntisym
65
remove
eqMp
appThm
appThm
absThm
appThm
appThm
63
ref
64
remove
appTerm
765
def
betaConv
320
ref
23
ref
361
ref
316
ref
25
ref
316
ref
26
ref
153
ref
18
ref
refl
766
def
15
ref
1
ref
28
ref
29
ref
nil
cons
cons
opType
constTerm
767
def
54
ref
appTerm
56
ref
appTerm
assume
sym
767
remove
56
ref
appTerm
54
ref
appTerm
assume
sym
deductAntisym
55
remove
eqMp
768
def
35
ref
refl
appThm
appThm
768
ref
36
ref
refl
appThm
appThm
appThm
39
ref
refl
appThm
absThm
appThm
absThm
appThm
appThm
316
ref
44
ref
684
ref
766
ref
768
remove
46
ref
refl
769
def
appThm
appThm
48
ref
refl
appThm
appThm
absThm
appThm
appThm
absThm
appThm
53
ref
54
remove
appTerm
770
def
betaConv
nil
32
ref
1
ref
29
ref
5
ref
cons
opType
771
def
constTerm
772
def
31
ref
24
ref
"Function.injective"
const
773
def
29
ref
constTerm
34
ref
appTerm
appTerm
45
ref
"Function.surjective"
const
774
def
29
ref
constTerm
34
ref
appTerm
appTerm
appTerm
775
def
absTerm
776
def
appTerm
777
def
axiom
nil
91
ref
777
ref
nil
cons
cons
94
ref
772
ref
53
ref
appTerm
778
def
nil
cons
779
def
cons
nil
cons
780
def
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
"P"
29
ref
var
781
def
31
ref
12
ref
776
ref
34
ref
appTerm
782
def
appTerm
778
ref
appTerm
783
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
30
remove
cons
nil
cons
784
def
215
ref
cons
785
def
233
ref
subst
786
def
subst
31
ref
nil
136
ref
783
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
91
ref
782
ref
nil
cons
787
def
cons
780
ref
cons
nil
cons
cons
788
def
123
ref
subst
788
remove
203
ref
subst
782
ref
betaConv
782
remove
assume
eqMp
nil
91
ref
775
remove
nil
cons
789
def
cons
790
def
780
remove
cons
nil
cons
cons
791
def
173
ref
subst
proveHyp
791
ref
123
ref
subst
791
remove
203
ref
subst
53
ref
34
ref
appTerm
betaConv
sym
nil
790
remove
94
ref
52
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
315
ref
361
ref
243
remove
"B"
22
remove
cons
792
def
nil
cons
cons
215
ref
cons
793
def
"f"
1
ref
216
ref
"B"
varType
794
def
nil
cons
cons
opType
795
def
var
796
def
27
ref
773
remove
1
ref
795
ref
5
ref
cons
opType
797
def
constTerm
796
ref
varTerm
798
def
appTerm
appTerm
219
ref
"x1"
216
ref
var
799
def
219
ref
"x2"
216
ref
var
800
def
12
ref
15
ref
1
ref
794
ref
1
ref
794
ref
5
ref
cons
opType
801
def
nil
cons
802
def
cons
opType
constTerm
803
def
798
ref
799
remove
varTerm
804
def
appTerm
appTerm
798
ref
800
remove
varTerm
805
def
appTerm
appTerm
appTerm
725
ref
804
remove
appTerm
805
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
806
def
798
ref
appTerm
807
def
betaConv
nil
0
ref
1
ref
797
ref
5
ref
cons
opType
808
def
constTerm
809
def
806
ref
appTerm
810
def
axiom
nil
91
ref
810
remove
nil
cons
cons
94
ref
807
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
"A"
795
ref
nil
cons
cons
nil
cons
811
def
"P"
797
ref
var
812
def
806
remove
nil
cons
cons
"x"
795
ref
var
813
def
798
ref
nil
cons
cons
nil
cons
814
def
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
appThm
684
ref
793
remove
796
ref
27
ref
774
remove
797
ref
constTerm
798
ref
appTerm
appTerm
0
ref
1
ref
801
remove
5
ref
cons
opType
815
def
constTerm
"y"
794
remove
var
816
def
329
ref
225
ref
803
ref
816
ref
varTerm
817
def
appTerm
798
ref
265
ref
appTerm
818
def
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
819
def
798
ref
appTerm
820
def
betaConv
nil
809
ref
819
ref
appTerm
821
def
axiom
nil
91
ref
821
remove
nil
cons
cons
94
ref
820
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
811
ref
812
ref
819
remove
nil
cons
cons
814
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
appThm
appThm
appThm
52
ref
refl
appThm
sym
nil
91
ref
12
ref
24
ref
13
ref
25
ref
13
ref
26
ref
12
ref
38
ref
appTerm
39
ref
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
45
ref
13
ref
"y"
2
ref
var
822
def
33
ref
44
ref
18
ref
822
ref
varTerm
823
def
appTerm
824
def
47
remove
appTerm
825
def
absTerm
826
def
appTerm
absTerm
827
def
appTerm
appTerm
appTerm
828
def
appTerm
829
def
52
remove
appTerm
830
def
nil
cons
cons
nil
cons
nil
cons
cons
729
ref
subst
sym
831
def
31
ref
12
ref
45
ref
830
remove
appTerm
appTerm
712
ref
appTerm
absTerm
832
def
34
ref
appTerm
833
def
betaConv
0
ref
771
remove
constTerm
834
def
refl
31
ref
831
remove
829
ref
refl
153
ref
320
ref
23
ref
43
ref
refl
835
def
23
ref
51
remove
absTerm
836
def
48
ref
appTerm
betaConv
837
def
appThm
absThm
appThm
appThm
835
remove
320
ref
23
ref
837
ref
absThm
appThm
appThm
appThm
nil
323
ref
836
ref
nil
cons
838
def
cons
91
ref
42
remove
nil
cons
cons
839
def
nil
cons
cons
nil
cons
cons
245
ref
324
ref
27
ref
329
ref
225
ref
113
ref
328
ref
appTerm
absTerm
appTerm
840
def
appTerm
113
ref
333
ref
appTerm
841
def
appTerm
absTerm
842
def
327
ref
appTerm
843
def
betaConv
91
ref
336
ref
842
ref
appTerm
844
def
absTerm
845
def
108
ref
appTerm
846
def
betaConv
nil
260
ref
845
ref
appTerm
847
def
axiom
nil
91
ref
847
remove
nil
cons
cons
94
ref
846
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
845
remove
nil
cons
cons
724
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
844
remove
nil
cons
cons
94
ref
843
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
342
ref
343
ref
842
remove
nil
cons
cons
347
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
subst
eqMp
appThm
trans
absThm
appThm
sym
nil
781
ref
31
ref
829
remove
43
remove
33
ref
836
remove
appTerm
848
def
appTerm
849
def
appTerm
850
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
786
ref
subst
31
remove
nil
136
ref
850
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
91
ref
828
ref
nil
cons
851
def
cons
94
ref
849
ref
nil
cons
852
def
cons
nil
cons
cons
nil
cons
cons
853
def
123
ref
subst
853
remove
203
ref
subst
nil
91
ref
852
ref
cons
nil
cons
nil
cons
cons
729
remove
subst
sym
nil
91
ref
45
ref
849
remove
appTerm
854
def
nil
cons
855
def
cons
734
ref
cons
nil
cons
cons
856
def
123
ref
subst
856
remove
203
ref
subst
nil
839
remove
94
ref
848
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
91
ref
368
ref
712
ref
appTerm
857
def
nil
cons
858
def
cons
859
def
94
ref
27
ref
45
ref
114
remove
appTerm
appTerm
14
ref
709
ref
appTerm
860
def
45
ref
110
ref
appTerm
861
def
appTerm
appTerm
nil
cons
862
def
cons
nil
cons
863
def
cons
nil
cons
cons
864
def
123
ref
subst
864
remove
203
ref
subst
27
ref
"_530"
4
ref
var
865
def
27
ref
45
ref
24
ref
865
remove
varTerm
866
def
appTerm
110
ref
appTerm
appTerm
appTerm
14
ref
45
ref
866
remove
appTerm
appTerm
861
ref
appTerm
appTerm
absTerm
867
def
108
ref
appTerm
868
def
appTerm
refl
869
def
867
ref
712
ref
appTerm
betaConv
appThm
153
ref
868
remove
betaConv
appThm
870
def
27
ref
45
ref
24
ref
712
ref
appTerm
871
def
110
ref
appTerm
appTerm
appTerm
14
ref
45
ref
712
ref
appTerm
872
def
appTerm
873
def
861
ref
appTerm
appTerm
refl
appThm
trans
867
remove
refl
874
def
857
remove
assume
875
def
appThm
eqMp
sym
153
ref
684
ref
146
ref
136
ref
27
ref
871
ref
139
ref
appTerm
appTerm
712
ref
appTerm
absTerm
876
def
139
ref
appTerm
877
def
betaConv
nil
260
ref
876
ref
appTerm
878
def
axiom
nil
91
ref
878
remove
nil
cons
cons
94
ref
877
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
876
remove
nil
cons
cons
717
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
879
def
subst
880
def
appThm
nil
27
ref
872
ref
appTerm
128
ref
appTerm
axiom
881
def
trans
appThm
14
ref
refl
882
def
881
ref
appThm
883
def
861
ref
refl
884
def
appThm
nil
136
ref
861
ref
nil
cons
885
def
cons
nil
cons
nil
cons
cons
886
def
136
ref
27
ref
14
ref
128
ref
appTerm
887
def
139
ref
appTerm
appTerm
128
ref
appTerm
absTerm
888
def
139
ref
appTerm
889
def
betaConv
nil
260
ref
888
ref
appTerm
890
def
axiom
nil
91
ref
890
remove
nil
cons
cons
94
ref
889
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
888
remove
nil
cons
cons
717
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
891
def
subst
892
def
trans
appThm
nil
136
ref
128
ref
nil
cons
893
def
cons
nil
cons
nil
cons
cons
894
def
136
ref
27
ref
27
ref
128
ref
appTerm
895
def
139
ref
appTerm
appTerm
139
ref
appTerm
absTerm
896
def
139
ref
appTerm
897
def
betaConv
nil
260
ref
896
ref
appTerm
898
def
axiom
nil
91
ref
898
remove
nil
cons
cons
94
ref
897
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
896
remove
nil
cons
cons
717
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
899
def
subst
900
def
trans
sym
142
ref
eqMp
eqMp
eqMp
nil
149
ref
858
ref
cons
901
def
151
ref
862
ref
cons
nil
cons
902
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
91
ref
368
ref
128
ref
appTerm
903
def
nil
cons
904
def
cons
905
def
863
remove
cons
nil
cons
cons
906
def
123
ref
subst
906
remove
203
ref
subst
869
remove
"_528"
4
ref
var
907
def
27
ref
45
ref
24
ref
907
remove
varTerm
908
def
appTerm
110
ref
appTerm
appTerm
appTerm
14
ref
45
ref
908
remove
appTerm
appTerm
861
ref
appTerm
appTerm
absTerm
128
ref
appTerm
betaConv
appThm
870
remove
27
ref
45
ref
24
ref
128
ref
appTerm
909
def
110
ref
appTerm
appTerm
appTerm
14
ref
45
ref
128
ref
appTerm
910
def
appTerm
911
def
861
ref
appTerm
appTerm
refl
appThm
trans
874
remove
903
remove
assume
912
def
appThm
eqMp
sym
153
ref
684
ref
146
ref
136
ref
27
ref
909
ref
139
ref
appTerm
appTerm
139
ref
appTerm
absTerm
913
def
139
ref
appTerm
914
def
betaConv
nil
260
ref
913
ref
appTerm
915
def
axiom
nil
91
ref
915
remove
nil
cons
cons
94
ref
914
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
913
remove
nil
cons
cons
717
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
916
def
subst
917
def
appThm
appThm
882
ref
nil
27
ref
910
ref
appTerm
712
ref
appTerm
axiom
918
def
appThm
919
def
884
remove
appThm
886
ref
136
ref
27
ref
14
ref
712
ref
appTerm
920
def
139
ref
appTerm
appTerm
139
ref
appTerm
absTerm
921
def
139
ref
appTerm
922
def
betaConv
nil
260
ref
921
ref
appTerm
923
def
axiom
nil
91
ref
923
remove
nil
cons
cons
94
ref
922
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
921
remove
nil
cons
cons
717
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
924
def
subst
925
def
trans
appThm
nil
262
ref
885
remove
cons
nil
cons
nil
cons
cons
728
ref
subst
926
def
trans
sym
142
ref
eqMp
eqMp
eqMp
nil
149
ref
904
remove
cons
927
def
902
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
136
ref
14
ref
141
remove
appTerm
140
remove
712
ref
appTerm
appTerm
absTerm
928
def
108
ref
appTerm
929
def
betaConv
nil
260
ref
928
ref
appTerm
930
def
axiom
931
def
nil
91
ref
930
remove
nil
cons
cons
932
def
94
ref
929
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
928
ref
nil
cons
cons
933
def
724
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
934
def
nil
927
ref
151
ref
858
remove
cons
935
def
553
ref
862
remove
cons
nil
cons
cons
cons
nil
cons
cons
572
ref
subst
proveHyp
proveHyp
proveHyp
subst
882
ref
nil
241
ref
41
ref
nil
cons
cons
nil
cons
nil
cons
cons
245
ref
153
ref
684
ref
219
ref
refl
nil
"t"
217
ref
var
936
def
221
remove
nil
cons
937
def
cons
nil
cons
nil
cons
cons
509
remove
"B"
5
ref
cons
938
def
nil
cons
cons
215
ref
cons
939
def
"t"
795
ref
var
940
def
15
remove
1
ref
795
remove
797
remove
nil
cons
cons
opType
constTerm
941
def
940
ref
varTerm
942
def
appTerm
225
ref
942
ref
265
ref
appTerm
absTerm
943
def
appTerm
944
def
absTerm
945
def
942
ref
appTerm
946
def
betaConv
809
ref
refl
940
ref
944
remove
assume
sym
941
remove
943
remove
appTerm
942
ref
appTerm
947
def
assume
sym
deductAntisym
absThm
appThm
nil
809
ref
940
remove
947
remove
absTerm
948
def
appTerm
949
def
axiom
950
def
eqMp
nil
91
ref
809
ref
945
ref
appTerm
nil
cons
cons
94
ref
946
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
811
ref
812
ref
945
remove
nil
cons
cons
813
remove
942
ref
nil
cons
cons
nil
cons
951
def
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
subst
952
def
appThm
appThm
appThm
329
ref
225
ref
45
ref
266
ref
appTerm
absTerm
953
def
appTerm
refl
appThm
sym
nil
223
ref
937
ref
cons
nil
cons
nil
cons
cons
954
def
223
ref
27
ref
45
ref
219
ref
330
remove
appTerm
955
def
appTerm
appTerm
329
ref
225
ref
45
ref
325
ref
appTerm
absTerm
956
def
appTerm
appTerm
absTerm
957
def
224
ref
appTerm
958
def
betaConv
nil
336
ref
957
ref
appTerm
959
def
axiom
nil
91
ref
959
remove
nil
cons
cons
94
ref
958
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
342
ref
343
ref
957
remove
nil
cons
cons
346
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
eqMp
960
def
subst
961
def
subst
320
ref
25
ref
684
ref
41
remove
35
ref
appTerm
betaConv
appThm
nil
241
ref
40
ref
nil
cons
cons
nil
cons
nil
cons
cons
961
ref
subst
320
ref
26
ref
684
ref
40
remove
36
ref
appTerm
betaConv
appThm
nil
91
ref
38
ref
nil
cons
962
def
cons
94
ref
39
ref
nil
cons
963
def
cons
nil
cons
cons
nil
cons
cons
964
def
nil
859
ref
94
ref
27
ref
45
ref
369
ref
appTerm
appTerm
14
ref
113
remove
861
ref
appTerm
appTerm
24
ref
709
ref
appTerm
110
ref
appTerm
appTerm
appTerm
nil
cons
965
def
cons
nil
cons
966
def
cons
nil
cons
cons
967
def
123
ref
subst
967
remove
203
ref
subst
27
ref
"_550"
4
ref
var
968
def
27
ref
45
ref
27
ref
968
remove
varTerm
969
def
appTerm
110
ref
appTerm
appTerm
appTerm
14
ref
24
ref
969
ref
appTerm
861
ref
appTerm
appTerm
24
ref
45
ref
969
remove
appTerm
appTerm
110
ref
appTerm
appTerm
appTerm
absTerm
970
def
108
ref
appTerm
971
def
appTerm
refl
972
def
970
ref
712
ref
appTerm
betaConv
appThm
153
ref
971
remove
betaConv
appThm
973
def
27
ref
45
ref
27
ref
712
ref
appTerm
974
def
110
ref
appTerm
975
def
appTerm
appTerm
14
ref
871
remove
861
ref
appTerm
appTerm
24
ref
872
ref
appTerm
976
def
110
ref
appTerm
appTerm
appTerm
refl
appThm
trans
970
remove
refl
977
def
875
ref
appThm
eqMp
sym
153
ref
684
ref
146
ref
136
ref
27
ref
974
ref
139
ref
appTerm
appTerm
713
ref
appTerm
absTerm
978
def
139
ref
appTerm
979
def
betaConv
nil
260
ref
978
ref
appTerm
980
def
axiom
nil
91
ref
980
remove
nil
cons
cons
94
ref
979
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
978
remove
nil
cons
cons
717
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
981
def
subst
982
def
appThm
146
ref
722
ref
subst
trans
appThm
882
ref
886
ref
879
ref
subst
appThm
361
ref
881
ref
appThm
983
def
118
ref
appThm
917
ref
trans
appThm
146
ref
924
ref
subst
984
def
trans
appThm
nil
262
ref
145
ref
cons
nil
cons
985
def
nil
cons
cons
728
ref
subst
986
def
trans
sym
142
ref
eqMp
eqMp
eqMp
nil
901
ref
151
ref
965
ref
cons
nil
cons
987
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
905
ref
966
remove
cons
nil
cons
cons
988
def
123
ref
subst
988
remove
203
ref
subst
972
remove
"_548"
4
ref
var
989
def
27
ref
45
ref
27
ref
989
remove
varTerm
990
def
appTerm
110
ref
appTerm
appTerm
appTerm
14
ref
24
ref
990
ref
appTerm
861
ref
appTerm
appTerm
24
ref
45
ref
990
remove
appTerm
appTerm
110
ref
appTerm
appTerm
appTerm
absTerm
128
ref
appTerm
betaConv
appThm
973
remove
27
ref
45
ref
895
remove
110
ref
appTerm
991
def
appTerm
appTerm
14
ref
909
remove
861
ref
appTerm
appTerm
24
ref
910
ref
appTerm
992
def
110
ref
appTerm
appTerm
appTerm
refl
appThm
trans
977
remove
912
ref
appThm
eqMp
sym
153
ref
684
ref
146
ref
899
remove
subst
993
def
appThm
appThm
882
ref
886
ref
916
ref
subst
appThm
361
ref
918
ref
appThm
994
def
118
ref
appThm
880
remove
trans
appThm
886
ref
136
ref
27
ref
14
ref
139
ref
appTerm
995
def
712
ref
appTerm
appTerm
139
ref
appTerm
absTerm
996
def
139
ref
appTerm
997
def
betaConv
nil
260
ref
996
ref
appTerm
998
def
axiom
nil
91
ref
998
remove
nil
cons
cons
94
ref
997
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
996
remove
nil
cons
cons
717
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
999
def
subst
trans
appThm
926
ref
trans
sym
142
ref
eqMp
eqMp
eqMp
nil
927
ref
987
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
934
ref
nil
927
ref
935
ref
553
ref
965
remove
cons
nil
cons
cons
cons
nil
cons
cons
572
ref
subst
proveHyp
proveHyp
proveHyp
subst
trans
absThm
appThm
trans
trans
absThm
appThm
trans
appThm
nil
241
ref
838
remove
cons
nil
cons
nil
cons
cons
245
ref
153
ref
684
ref
329
ref
refl
1000
def
952
remove
appThm
appThm
appThm
219
ref
953
remove
appTerm
refl
appThm
sym
954
remove
223
ref
27
ref
45
ref
331
ref
appTerm
appTerm
219
ref
956
remove
appTerm
appTerm
absTerm
1001
def
224
ref
appTerm
1002
def
betaConv
nil
336
ref
1001
ref
appTerm
1003
def
axiom
nil
91
ref
1003
remove
nil
cons
cons
94
ref
1002
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
342
ref
343
ref
1001
remove
nil
cons
cons
346
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
eqMp
subst
1004
def
subst
316
ref
23
ref
684
ref
837
remove
appThm
nil
241
ref
50
ref
nil
cons
cons
nil
cons
nil
cons
cons
961
ref
subst
320
ref
44
ref
684
ref
50
remove
46
ref
appTerm
betaConv
appThm
nil
91
ref
49
ref
nil
cons
cons
nil
cons
nil
cons
cons
723
ref
subst
trans
absThm
appThm
trans
trans
absThm
appThm
trans
appThm
trans
882
ref
320
ref
25
ref
153
ref
320
ref
26
ref
882
ref
26
ref
24
ref
38
ref
appTerm
45
ref
39
ref
appTerm
1005
def
appTerm
1006
def
absTerm
1007
def
36
ref
appTerm
betaConv
1008
def
appThm
26
ref
24
ref
45
ref
38
remove
appTerm
1009
def
appTerm
39
ref
appTerm
1010
def
absTerm
1011
def
36
ref
appTerm
betaConv
1012
def
appThm
absThm
appThm
1013
def
appThm
882
ref
320
ref
26
ref
1008
remove
absThm
appThm
appThm
320
ref
26
ref
1012
remove
absThm
appThm
appThm
1014
def
appThm
nil
321
ref
1007
ref
nil
cons
cons
323
ref
1011
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
1015
def
245
ref
324
ref
27
ref
329
ref
225
ref
14
ref
325
ref
appTerm
1016
def
328
ref
appTerm
absTerm
appTerm
1017
def
appTerm
14
ref
331
ref
appTerm
1018
def
333
ref
appTerm
1019
def
appTerm
absTerm
1020
def
327
ref
appTerm
1021
def
betaConv
223
ref
336
ref
1020
ref
appTerm
1022
def
absTerm
1023
def
224
ref
appTerm
1024
def
betaConv
nil
336
ref
1023
ref
appTerm
1025
def
axiom
nil
91
ref
1025
remove
nil
cons
cons
94
ref
1024
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
342
ref
343
ref
1023
remove
nil
cons
cons
346
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
1022
remove
nil
cons
cons
94
ref
1021
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
342
ref
343
ref
1020
remove
nil
cons
cons
347
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
1026
def
subst
eqMp
absThm
appThm
153
ref
320
ref
25
ref
882
ref
25
ref
33
ref
1007
remove
appTerm
absTerm
1027
def
35
ref
appTerm
betaConv
1028
def
appThm
25
ref
33
ref
1011
remove
appTerm
absTerm
1029
def
35
ref
appTerm
betaConv
1030
def
appThm
absThm
appThm
1031
def
appThm
882
ref
320
ref
25
ref
1028
remove
absThm
appThm
appThm
320
ref
25
ref
1030
remove
absThm
appThm
appThm
1032
def
appThm
nil
321
ref
1027
remove
nil
cons
cons
323
ref
1029
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
1033
def
1026
remove
subst
eqMp
trans
appThm
13
ref
23
ref
33
ref
44
ref
49
remove
absTerm
1034
def
appTerm
absTerm
appTerm
refl
appThm
882
ref
153
ref
1032
remove
appThm
1031
remove
appThm
1033
remove
245
ref
324
ref
27
ref
1019
remove
appTerm
1017
remove
appTerm
absTerm
1035
def
327
ref
appTerm
1036
def
betaConv
223
ref
336
ref
1035
ref
appTerm
1037
def
absTerm
1038
def
224
ref
appTerm
1039
def
betaConv
nil
336
ref
1038
ref
appTerm
1040
def
axiom
nil
91
ref
1040
remove
nil
cons
cons
94
ref
1039
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
342
ref
343
ref
1038
remove
nil
cons
cons
346
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
1037
remove
nil
cons
cons
94
ref
1036
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
342
ref
343
ref
1035
remove
nil
cons
cons
347
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
1041
def
subst
eqMp
320
ref
25
ref
153
ref
1014
remove
appThm
1013
remove
appThm
1015
remove
1041
remove
subst
eqMp
absThm
appThm
trans
appThm
153
ref
316
ref
23
ref
320
ref
44
ref
23
ref
1034
ref
absTerm
1042
def
48
ref
appTerm
betaConv
1043
def
769
ref
appThm
1034
ref
46
ref
appTerm
betaConv
trans
absThm
appThm
absThm
appThm
appThm
772
ref
refl
1044
def
"f'"
28
ref
var
1045
def
316
ref
23
ref
1043
remove
1045
ref
varTerm
1046
def
48
ref
appTerm
1047
def
refl
appThm
1034
remove
1047
ref
appTerm
betaConv
trans
absThm
appThm
absThm
appThm
appThm
nil
"r"
17
remove
var
1042
remove
nil
cons
cons
nil
cons
nil
cons
cons
792
remove
244
ref
cons
215
ref
cons
"r"
1
ref
216
ref
802
remove
cons
opType
1048
def
var
1049
def
27
ref
219
ref
225
ref
32
ref
815
remove
constTerm
816
remove
1049
remove
varTerm
1050
def
265
ref
appTerm
1051
def
817
remove
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
32
ref
808
remove
constTerm
796
ref
219
ref
225
ref
1051
remove
818
ref
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
1052
def
1050
ref
appTerm
1053
def
betaConv
nil
0
ref
1
ref
1
ref
1048
ref
5
ref
cons
opType
1054
def
5
ref
cons
opType
constTerm
1052
ref
appTerm
1055
def
axiom
nil
91
ref
1055
remove
nil
cons
cons
94
ref
1053
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
"A"
1048
ref
nil
cons
cons
nil
cons
"P"
1054
remove
var
1052
remove
nil
cons
cons
"x"
1048
remove
var
1050
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
subst
eqMp
appThm
153
ref
882
ref
320
ref
25
ref
25
ref
33
ref
26
ref
14
ref
1006
ref
appTerm
1010
ref
appTerm
1056
def
absTerm
1057
def
appTerm
absTerm
1058
def
35
ref
appTerm
betaConv
1059
def
absThm
appThm
appThm
772
ref
1045
ref
13
ref
23
ref
18
ref
34
ref
1047
remove
appTerm
appTerm
48
ref
appTerm
absTerm
1060
def
appTerm
1061
def
absTerm
1062
def
appTerm
1063
def
refl
1064
def
appThm
appThm
320
ref
25
ref
882
ref
1059
remove
appThm
1064
ref
appThm
absThm
appThm
appThm
nil
321
ref
1058
remove
nil
cons
cons
94
ref
1063
remove
nil
cons
cons
nil
cons
1065
def
cons
nil
cons
cons
245
ref
94
ref
27
ref
1018
remove
110
ref
appTerm
appTerm
329
ref
225
ref
1016
remove
110
ref
appTerm
absTerm
appTerm
appTerm
absTerm
1066
def
110
ref
appTerm
1067
def
betaConv
223
ref
260
ref
1066
ref
appTerm
1068
def
absTerm
1069
def
224
ref
appTerm
1070
def
betaConv
nil
336
ref
1069
ref
appTerm
1071
def
axiom
nil
91
ref
1071
remove
nil
cons
cons
94
ref
1070
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
342
ref
343
ref
1069
remove
nil
cons
cons
346
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
1068
remove
nil
cons
cons
94
ref
1067
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
1066
remove
nil
cons
cons
985
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
1072
def
subst
eqMp
320
ref
25
ref
153
ref
882
ref
320
ref
26
ref
1057
ref
36
ref
appTerm
betaConv
1073
def
absThm
appThm
appThm
1064
ref
appThm
appThm
320
ref
26
ref
882
ref
1073
remove
appThm
1064
remove
appThm
absThm
appThm
appThm
nil
321
ref
1057
remove
nil
cons
cons
1065
remove
cons
nil
cons
cons
1072
remove
subst
eqMp
320
ref
26
ref
153
ref
14
ref
1056
ref
appTerm
1074
def
refl
1075
def
1044
ref
1045
ref
1062
ref
1046
ref
appTerm
betaConv
1076
def
absThm
appThm
appThm
appThm
1044
remove
1045
ref
1075
remove
1076
remove
appThm
absThm
appThm
appThm
nil
"q"
29
ref
var
1062
remove
nil
cons
cons
91
ref
1056
remove
nil
cons
1077
def
cons
1078
def
nil
cons
cons
nil
cons
cons
785
remove
324
ref
27
ref
14
ref
108
ref
appTerm
1079
def
333
remove
appTerm
appTerm
329
ref
225
ref
1079
ref
328
ref
appTerm
absTerm
appTerm
appTerm
absTerm
1080
def
327
ref
appTerm
1081
def
betaConv
91
ref
336
ref
1080
ref
appTerm
1082
def
absTerm
1083
def
108
ref
appTerm
1084
def
betaConv
nil
260
ref
1083
ref
appTerm
1085
def
axiom
nil
91
ref
1085
remove
nil
cons
cons
94
ref
1084
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
1083
remove
nil
cons
cons
724
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
1082
remove
nil
cons
cons
94
ref
1081
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
342
ref
343
ref
1080
remove
nil
cons
cons
347
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
subst
eqMp
absThm
appThm
trans
absThm
appThm
trans
trans
trans
trans
854
remove
assume
eqMp
nil
91
ref
33
ref
25
ref
33
ref
26
ref
772
remove
1045
ref
1074
remove
1061
ref
appTerm
1086
def
absTerm
1087
def
appTerm
1088
def
absTerm
1089
def
appTerm
1090
def
absTerm
1091
def
appTerm
1092
def
nil
cons
cons
734
ref
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
241
ref
25
ref
12
ref
1091
ref
35
ref
appTerm
1093
def
appTerm
712
ref
appTerm
1094
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
246
ref
subst
25
ref
nil
136
ref
1094
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
91
ref
1093
ref
nil
cons
1095
def
cons
734
ref
cons
nil
cons
cons
1096
def
123
ref
subst
1096
remove
203
ref
subst
1093
ref
betaConv
1093
remove
assume
eqMp
nil
91
ref
1090
ref
nil
cons
cons
734
ref
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
241
ref
26
ref
12
ref
1089
ref
36
ref
appTerm
1097
def
appTerm
712
ref
appTerm
1098
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
246
ref
subst
26
ref
nil
136
ref
1098
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
91
ref
1097
ref
nil
cons
1099
def
cons
734
ref
cons
nil
cons
cons
1100
def
123
ref
subst
1100
remove
203
ref
subst
1097
ref
betaConv
1097
remove
assume
eqMp
nil
91
ref
1088
ref
nil
cons
cons
734
ref
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
781
ref
1045
ref
12
ref
1087
ref
1046
ref
appTerm
1101
def
appTerm
712
ref
appTerm
1102
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
786
remove
subst
1045
remove
nil
136
ref
1102
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
91
ref
1101
ref
nil
cons
1103
def
cons
734
ref
cons
nil
cons
cons
1104
def
123
ref
subst
1104
remove
203
ref
subst
1101
ref
betaConv
1101
remove
assume
eqMp
nil
91
ref
1086
remove
nil
cons
1105
def
cons
734
ref
cons
nil
cons
cons
1106
def
173
ref
subst
proveHyp
1106
ref
123
ref
subst
1106
remove
203
ref
subst
361
ref
316
ref
25
ref
316
ref
26
ref
964
ref
nil
859
ref
94
ref
112
ref
860
remove
110
ref
appTerm
1107
def
appTerm
nil
cons
1108
def
cons
nil
cons
1109
def
cons
nil
cons
cons
1110
def
123
ref
subst
1110
remove
203
ref
subst
27
ref
"_538"
4
ref
var
1111
def
27
ref
12
ref
1111
remove
varTerm
1112
def
appTerm
110
ref
appTerm
appTerm
14
ref
45
ref
1112
remove
appTerm
appTerm
110
ref
appTerm
appTerm
absTerm
1113
def
108
ref
appTerm
1114
def
appTerm
refl
1115
def
1113
ref
712
ref
appTerm
betaConv
appThm
153
ref
1114
remove
betaConv
appThm
1116
def
27
ref
12
ref
712
ref
appTerm
1117
def
110
ref
appTerm
appTerm
873
ref
110
ref
appTerm
1118
def
appTerm
refl
appThm
trans
1113
remove
refl
1119
def
875
ref
appThm
eqMp
sym
153
ref
146
ref
136
ref
27
ref
1117
ref
139
ref
appTerm
appTerm
128
ref
appTerm
absTerm
1120
def
139
ref
appTerm
1121
def
betaConv
nil
260
ref
1120
ref
appTerm
1122
def
axiom
nil
91
ref
1122
remove
nil
cons
cons
94
ref
1121
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
1120
remove
nil
cons
cons
717
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
appThm
883
remove
118
ref
appThm
146
ref
891
ref
subst
trans
1123
def
appThm
900
ref
trans
sym
142
ref
eqMp
eqMp
eqMp
nil
901
ref
151
ref
1108
ref
cons
nil
cons
1124
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
905
ref
1109
remove
cons
nil
cons
cons
1125
def
123
ref
subst
1125
remove
203
ref
subst
1115
remove
"_536"
4
ref
var
1126
def
27
ref
12
ref
1126
remove
varTerm
1127
def
appTerm
110
ref
appTerm
appTerm
14
ref
45
ref
1127
remove
appTerm
appTerm
110
ref
appTerm
appTerm
absTerm
128
ref
appTerm
betaConv
appThm
1116
remove
27
ref
12
ref
128
ref
appTerm
1128
def
110
ref
appTerm
appTerm
911
ref
110
ref
appTerm
1129
def
appTerm
refl
appThm
trans
1119
remove
912
ref
appThm
eqMp
sym
153
ref
146
remove
136
ref
27
ref
1128
remove
139
ref
appTerm
appTerm
139
ref
appTerm
absTerm
1130
def
139
ref
appTerm
1131
def
betaConv
nil
260
ref
1130
ref
appTerm
1132
def
axiom
nil
91
ref
1132
remove
nil
cons
cons
94
ref
1131
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
1130
remove
nil
cons
cons
717
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
1133
def
subst
appThm
919
remove
118
remove
appThm
984
remove
trans
1134
def
appThm
986
ref
trans
sym
142
ref
eqMp
eqMp
eqMp
nil
927
ref
1124
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
934
ref
nil
927
ref
935
ref
553
ref
1108
remove
cons
nil
cons
cons
cons
nil
cons
cons
572
ref
subst
proveHyp
proveHyp
proveHyp
1135
def
subst
absThm
appThm
absThm
appThm
appThm
nil
241
ref
827
ref
nil
cons
cons
nil
cons
nil
cons
cons
961
remove
subst
320
ref
822
ref
684
ref
827
remove
823
ref
appTerm
betaConv
appThm
nil
241
ref
826
ref
nil
cons
cons
nil
cons
nil
cons
cons
1004
remove
subst
316
ref
44
ref
684
ref
826
remove
46
ref
appTerm
betaConv
appThm
absThm
appThm
trans
trans
absThm
appThm
trans
appThm
153
ref
24
ref
13
ref
25
ref
13
ref
26
ref
14
ref
1009
ref
appTerm
39
remove
appTerm
absTerm
appTerm
absTerm
1136
def
appTerm
1137
def
appTerm
1138
def
refl
1139
def
320
ref
822
ref
822
ref
13
ref
44
ref
45
ref
825
remove
appTerm
absTerm
1140
def
appTerm
1141
def
absTerm
1142
def
823
ref
appTerm
betaConv
1143
def
absThm
appThm
appThm
appThm
320
remove
822
ref
1139
remove
1143
remove
appThm
absThm
appThm
appThm
nil
323
ref
1142
remove
nil
cons
cons
91
ref
1137
remove
nil
cons
1144
def
cons
1145
def
nil
cons
cons
nil
cons
cons
245
ref
324
ref
27
ref
841
remove
appTerm
840
remove
appTerm
absTerm
1146
def
327
ref
appTerm
1147
def
betaConv
91
ref
336
ref
1146
ref
appTerm
1148
def
absTerm
1149
def
108
ref
appTerm
1150
def
betaConv
nil
260
ref
1149
ref
appTerm
1151
def
axiom
nil
91
ref
1151
remove
nil
cons
cons
94
ref
1150
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
1149
remove
nil
cons
cons
724
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
1148
remove
nil
cons
cons
94
ref
1147
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
342
ref
343
ref
1146
remove
nil
cons
cons
347
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
subst
eqMp
trans
828
remove
assume
eqMp
nil
91
ref
33
ref
822
ref
1138
remove
1141
ref
appTerm
1152
def
absTerm
1153
def
appTerm
1154
def
nil
cons
cons
734
ref
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
241
ref
822
ref
12
ref
1153
ref
823
ref
appTerm
1155
def
appTerm
712
ref
appTerm
1156
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
246
ref
subst
822
ref
nil
136
ref
1156
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
91
ref
1155
ref
nil
cons
1157
def
cons
734
ref
cons
nil
cons
cons
1158
def
123
ref
subst
1158
remove
203
ref
subst
1155
ref
betaConv
1155
remove
assume
eqMp
nil
91
ref
1152
remove
nil
cons
1159
def
cons
734
ref
cons
nil
cons
cons
1160
def
173
ref
subst
proveHyp
1160
ref
123
ref
subst
1160
remove
203
ref
subst
nil
91
ref
1061
remove
nil
cons
1161
def
cons
1162
def
734
ref
cons
nil
cons
cons
1163
def
123
ref
subst
1163
remove
203
ref
subst
nil
"_1880"
2
ref
var
1164
def
823
ref
nil
cons
cons
nil
cons
nil
cons
cons
1060
ref
1164
remove
varTerm
1165
def
appTerm
1166
def
betaConv
nil
1162
remove
94
ref
1166
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
244
ref
241
ref
1060
remove
nil
cons
cons
44
ref
1165
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
nil
91
ref
18
ref
34
ref
1046
remove
823
ref
appTerm
1167
def
appTerm
1168
def
appTerm
1169
def
823
ref
appTerm
1170
def
nil
cons
cons
94
ref
1169
remove
1168
ref
appTerm
1171
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
203
ref
subst
proveHyp
nil
44
ref
1168
ref
nil
cons
1172
def
cons
nil
cons
1173
def
nil
cons
cons
769
ref
subst
eqMp
nil
91
ref
24
ref
1170
remove
appTerm
1171
remove
appTerm
nil
cons
cons
94
ref
824
ref
1168
remove
appTerm
nil
cons
1174
def
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
23
ref
1172
remove
cons
1173
remove
cons
nil
cons
cons
nil
"b"
4
ref
var
1175
def
14
ref
45
ref
18
ref
46
ref
appTerm
1176
def
823
remove
appTerm
1177
def
appTerm
1178
def
appTerm
1179
def
45
ref
1176
remove
48
ref
appTerm
1180
def
appTerm
1181
def
appTerm
nil
cons
cons
"a"
4
ref
var
1182
def
824
ref
48
remove
appTerm
1183
def
nil
cons
1184
def
cons
nil
cons
cons
nil
cons
cons
nil
91
ref
27
ref
1182
ref
varTerm
1185
def
appTerm
1186
def
712
ref
appTerm
1187
def
nil
cons
1188
def
cons
1189
def
94
ref
27
ref
14
ref
1185
ref
appTerm
1175
ref
varTerm
1190
def
appTerm
1191
def
appTerm
12
ref
45
ref
1190
ref
appTerm
1192
def
appTerm
1193
def
1185
ref
appTerm
appTerm
nil
cons
1194
def
cons
nil
cons
1195
def
cons
nil
cons
cons
1196
def
123
ref
subst
1196
remove
203
ref
subst
27
ref
"_606"
4
ref
var
1197
def
27
ref
14
ref
1197
remove
varTerm
1198
def
appTerm
1190
ref
appTerm
appTerm
1193
ref
1198
remove
appTerm
appTerm
absTerm
1199
def
1185
ref
appTerm
1200
def
appTerm
refl
1201
def
1199
ref
712
ref
appTerm
betaConv
appThm
153
ref
1200
remove
betaConv
appThm
1202
def
27
ref
920
ref
1190
ref
appTerm
1203
def
appTerm
1193
ref
712
ref
appTerm
appTerm
refl
appThm
trans
1199
remove
refl
1204
def
1187
remove
assume
1205
def
appThm
eqMp
sym
153
ref
nil
136
ref
1190
ref
nil
cons
1206
def
cons
nil
cons
nil
cons
cons
1207
def
924
ref
subst
1208
def
appThm
nil
136
ref
1192
ref
nil
cons
1209
def
cons
nil
cons
nil
cons
cons
1210
def
718
ref
subst
1207
ref
722
ref
subst
trans
appThm
nil
262
ref
1206
remove
cons
nil
cons
nil
cons
cons
728
ref
subst
trans
sym
142
ref
eqMp
eqMp
eqMp
nil
149
ref
1188
ref
cons
1211
def
151
ref
1194
ref
cons
nil
cons
1212
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
91
ref
1186
remove
128
ref
appTerm
1213
def
nil
cons
1214
def
cons
1215
def
1195
remove
cons
nil
cons
cons
1216
def
123
ref
subst
1216
remove
203
ref
subst
1201
remove
"_604"
4
ref
var
1217
def
27
ref
14
ref
1217
remove
varTerm
1218
def
appTerm
1190
ref
appTerm
appTerm
1193
ref
1218
remove
appTerm
appTerm
absTerm
128
ref
appTerm
betaConv
appThm
1202
remove
27
ref
887
ref
1190
ref
appTerm
1219
def
appTerm
1193
remove
128
ref
appTerm
appTerm
refl
appThm
trans
1204
remove
1213
remove
assume
1220
def
appThm
eqMp
sym
153
ref
1207
remove
891
ref
subst
1221
def
appThm
1210
ref
136
ref
27
ref
711
ref
128
ref
appTerm
appTerm
128
ref
appTerm
absTerm
1222
def
139
ref
appTerm
1223
def
betaConv
nil
260
ref
1222
ref
appTerm
1224
def
axiom
nil
91
ref
1224
remove
nil
cons
cons
94
ref
1223
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
1222
remove
nil
cons
cons
717
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
1225
def
subst
appThm
900
remove
trans
sym
142
ref
eqMp
eqMp
eqMp
nil
149
ref
1214
remove
cons
1226
def
1212
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
928
ref
1185
ref
appTerm
1227
def
betaConv
931
ref
nil
932
ref
94
ref
1227
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
933
ref
262
ref
1185
ref
nil
cons
1228
def
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
1229
def
nil
1226
ref
151
ref
1188
remove
cons
1230
def
553
ref
1194
remove
cons
nil
cons
cons
cons
nil
cons
cons
572
ref
subst
proveHyp
proveHyp
proveHyp
1231
def
subst
315
ref
nil
1175
ref
1181
remove
nil
cons
1232
def
cons
1182
ref
1178
remove
nil
cons
1233
def
cons
nil
cons
cons
nil
cons
cons
nil
1189
remove
94
ref
27
ref
45
ref
1191
remove
appTerm
appTerm
24
ref
45
ref
1185
ref
appTerm
appTerm
1192
ref
appTerm
appTerm
nil
cons
1234
def
cons
nil
cons
1235
def
cons
nil
cons
cons
1236
def
123
ref
subst
1236
remove
203
ref
subst
27
ref
"_610"
4
ref
var
1237
def
27
ref
45
ref
14
ref
1237
remove
varTerm
1238
def
appTerm
1190
ref
appTerm
appTerm
appTerm
24
ref
45
ref
1238
remove
appTerm
appTerm
1192
ref
appTerm
appTerm
absTerm
1239
def
1185
remove
appTerm
1240
def
appTerm
refl
1241
def
1239
ref
712
ref
appTerm
betaConv
appThm
153
ref
1240
remove
betaConv
appThm
1242
def
27
ref
45
ref
1203
remove
appTerm
appTerm
976
remove
1192
ref
appTerm
appTerm
refl
appThm
trans
1239
remove
refl
1243
def
1205
remove
appThm
eqMp
sym
153
ref
684
ref
1208
remove
appThm
appThm
983
remove
1192
ref
refl
1244
def
appThm
1210
ref
916
ref
subst
trans
appThm
nil
262
ref
1209
remove
cons
nil
cons
nil
cons
cons
728
ref
subst
trans
sym
142
ref
eqMp
eqMp
eqMp
nil
1211
remove
151
ref
1234
ref
cons
nil
cons
1245
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
1215
remove
1235
remove
cons
nil
cons
cons
1246
def
123
ref
subst
1246
remove
203
ref
subst
1241
remove
"_608"
4
ref
var
1247
def
27
ref
45
ref
14
ref
1247
remove
varTerm
1248
def
appTerm
1190
remove
appTerm
appTerm
appTerm
24
ref
45
ref
1248
remove
appTerm
appTerm
1192
ref
appTerm
appTerm
absTerm
128
ref
appTerm
betaConv
appThm
1242
remove
27
ref
45
ref
1219
remove
appTerm
appTerm
992
remove
1192
remove
appTerm
appTerm
refl
appThm
trans
1243
remove
1220
remove
appThm
eqMp
sym
153
ref
684
ref
1221
remove
appThm
918
ref
trans
appThm
994
remove
1244
remove
appThm
1210
remove
879
remove
subst
trans
appThm
nil
136
ref
733
ref
cons
nil
cons
nil
cons
cons
981
remove
subst
881
ref
trans
trans
sym
142
ref
eqMp
eqMp
eqMp
nil
1226
ref
1245
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
1229
remove
nil
1226
remove
1230
remove
553
ref
1234
remove
cons
nil
cons
cons
cons
nil
cons
cons
572
ref
subst
proveHyp
proveHyp
proveHyp
subst
361
ref
nil
1182
ref
1177
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
136
ref
1228
remove
cons
nil
cons
nil
cons
cons
722
remove
subst
1249
def
subst
appThm
nil
1182
ref
1180
remove
nil
cons
cons
nil
cons
nil
cons
cons
1249
ref
subst
appThm
trans
appThm
1183
remove
refl
appThm
trans
1179
remove
refl
nil
94
ref
1184
remove
cons
1250
def
91
ref
1232
ref
cons
nil
cons
cons
nil
cons
cons
nil
"t2"
4
ref
var
1251
def
145
ref
cons
"t1"
4
ref
var
1252
def
137
ref
cons
nil
cons
cons
1253
def
nil
cons
cons
1251
ref
27
ref
14
ref
1252
ref
varTerm
1254
def
appTerm
1255
def
1251
ref
varTerm
1256
def
appTerm
1257
def
appTerm
14
ref
1256
ref
appTerm
1258
def
1254
ref
appTerm
appTerm
absTerm
1259
def
1256
ref
appTerm
1260
def
betaConv
1252
ref
260
ref
1259
ref
appTerm
1261
def
absTerm
1262
def
1254
ref
appTerm
1263
def
betaConv
nil
260
ref
1262
ref
appTerm
1264
def
axiom
nil
91
ref
1264
remove
nil
cons
cons
94
ref
1263
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
1262
remove
nil
cons
cons
262
ref
1254
ref
nil
cons
cons
nil
cons
1265
def
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
1261
remove
nil
cons
cons
94
ref
1260
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
1259
remove
nil
cons
cons
262
ref
1256
ref
nil
cons
cons
nil
cons
1266
def
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
1267
def
subst
appThm
nil
559
remove
1232
remove
cons
1250
remove
91
ref
1233
remove
cons
nil
cons
cons
cons
nil
cons
cons
153
ref
nil
"t3"
4
ref
var
1268
def
634
remove
cons
1269
def
1253
remove
cons
nil
cons
cons
1268
ref
27
ref
1255
remove
1258
remove
1268
ref
varTerm
1270
def
appTerm
appTerm
1271
def
appTerm
14
ref
1257
remove
appTerm
1270
ref
appTerm
1272
def
appTerm
1273
def
absTerm
1274
def
1270
ref
appTerm
1275
def
betaConv
1251
ref
260
ref
1274
ref
appTerm
1276
def
absTerm
1277
def
1256
remove
appTerm
1278
def
betaConv
1252
ref
260
ref
1277
ref
appTerm
1279
def
absTerm
1280
def
1254
remove
appTerm
1281
def
betaConv
260
ref
refl
1282
def
1252
ref
1282
ref
1251
ref
1282
remove
1268
ref
1273
remove
assume
sym
27
ref
1272
remove
appTerm
1271
remove
appTerm
1283
def
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
absThm
appThm
nil
260
ref
1252
ref
260
ref
1251
ref
260
ref
1268
remove
1283
remove
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
91
ref
260
ref
1280
ref
appTerm
nil
cons
cons
94
ref
1281
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
1280
remove
nil
cons
cons
1265
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
1279
remove
nil
cons
cons
94
ref
1278
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
1277
remove
nil
cons
cons
1266
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
1276
remove
nil
cons
cons
94
ref
1275
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
1274
remove
nil
cons
cons
262
ref
1270
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
1284
def
subst
appThm
nil
1269
remove
1251
remove
137
remove
cons
1252
remove
145
remove
cons
nil
cons
cons
cons
nil
cons
cons
1284
remove
subst
appThm
sym
882
ref
1267
ref
appThm
560
remove
refl
appThm
eqMp
subst
trans
245
ref
nil
91
ref
45
ref
726
ref
"y"
216
ref
var
1285
def
varTerm
1286
def
appTerm
1287
def
appTerm
1288
def
nil
cons
1289
def
cons
1290
def
94
ref
14
ref
1288
remove
appTerm
14
ref
45
ref
726
remove
"z"
216
remove
var
varTerm
1291
def
appTerm
appTerm
appTerm
725
ref
1286
ref
appTerm
1291
ref
appTerm
1292
def
appTerm
1293
def
appTerm
nil
cons
1294
def
cons
nil
cons
1295
def
cons
nil
cons
cons
1296
def
123
ref
subst
1296
remove
203
ref
subst
882
ref
684
ref
nil
1290
remove
94
ref
27
ref
1287
ref
appTerm
712
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
nil
149
ref
1287
ref
nil
cons
1297
def
cons
1298
def
nil
cons
nil
cons
cons
nil
91
ref
45
ref
154
ref
appTerm
1299
def
nil
cons
1300
def
cons
94
ref
27
ref
154
ref
appTerm
712
ref
appTerm
nil
cons
1301
def
cons
nil
cons
cons
nil
cons
cons
1302
def
123
ref
subst
1302
remove
203
ref
subst
nil
598
remove
734
ref
cons
nil
cons
cons
386
ref
subst
27
ref
1299
ref
appTerm
refl
91
ref
109
ref
712
ref
appTerm
absTerm
1303
def
154
ref
appTerm
betaConv
appThm
nil
132
remove
45
ref
appTerm
1303
remove
appTerm
axiom
163
remove
appThm
eqMp
1299
remove
assume
eqMp
nil
91
ref
558
remove
712
ref
appTerm
nil
cons
cons
94
ref
1117
remove
154
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
203
ref
subst
proveHyp
nil
91
ref
733
ref
cons
94
ref
597
ref
cons
nil
cons
cons
nil
cons
cons
1304
def
123
ref
subst
1304
remove
203
ref
subst
91
ref
108
ref
absTerm
1305
def
154
remove
appTerm
1306
def
betaConv
nil
974
remove
260
ref
1305
ref
appTerm
1307
def
appTerm
axiom
712
ref
assume
eqMp
nil
91
ref
1307
remove
nil
cons
cons
94
ref
1306
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
1305
remove
nil
cons
cons
262
ref
597
ref
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
nil
149
ref
733
ref
cons
151
ref
597
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
149
ref
1300
remove
cons
151
ref
1301
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
subst
eqMp
appThm
881
ref
trans
appThm
1293
ref
refl
appThm
nil
136
ref
1293
remove
nil
cons
cons
nil
cons
nil
cons
cons
891
remove
subst
trans
sym
142
ref
eqMp
eqMp
nil
149
ref
1289
ref
cons
151
ref
1294
ref
cons
nil
cons
1308
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
91
ref
1297
ref
cons
1295
remove
cons
nil
cons
cons
1309
def
123
ref
subst
1309
remove
203
ref
subst
882
ref
684
ref
725
remove
refl
1287
ref
assume
appThm
1310
def
1286
ref
refl
appThm
nil
225
ref
1286
ref
nil
cons
cons
nil
cons
1311
def
nil
cons
cons
727
ref
subst
trans
appThm
918
remove
trans
appThm
882
remove
684
ref
1310
remove
1291
remove
refl
appThm
appThm
appThm
1292
ref
refl
appThm
appThm
nil
136
ref
14
ref
45
ref
1292
ref
appTerm
appTerm
1292
ref
appTerm
nil
cons
1312
def
cons
nil
cons
nil
cons
cons
924
remove
subst
trans
sym
nil
91
ref
27
ref
1292
ref
appTerm
1313
def
712
ref
appTerm
1314
def
nil
cons
1315
def
cons
94
ref
1312
ref
cons
nil
cons
1316
def
cons
nil
cons
cons
1317
def
123
ref
subst
1317
remove
203
ref
subst
27
ref
"_626"
4
ref
var
1318
def
14
ref
45
ref
1318
remove
varTerm
1319
def
appTerm
appTerm
1319
remove
appTerm
absTerm
1320
def
1292
ref
appTerm
1321
def
appTerm
refl
1322
def
1320
ref
712
ref
appTerm
betaConv
appThm
153
ref
1321
remove
betaConv
appThm
1323
def
873
remove
712
ref
appTerm
refl
appThm
trans
1320
remove
refl
1324
def
1314
remove
assume
appThm
eqMp
sym
nil
136
ref
872
remove
nil
cons
cons
nil
cons
nil
cons
cons
999
remove
subst
881
remove
trans
sym
142
ref
eqMp
eqMp
eqMp
nil
149
ref
1315
ref
cons
151
ref
1312
ref
cons
nil
cons
1325
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
91
ref
1313
remove
128
ref
appTerm
1326
def
nil
cons
1327
def
cons
1316
remove
cons
nil
cons
cons
1328
def
123
ref
subst
1328
remove
203
ref
subst
1322
remove
"_624"
4
ref
var
1329
def
14
ref
45
ref
1329
remove
varTerm
1330
def
appTerm
appTerm
1330
remove
appTerm
absTerm
128
ref
appTerm
betaConv
appThm
1323
remove
911
remove
128
ref
appTerm
refl
appThm
trans
1324
remove
1326
remove
assume
appThm
eqMp
sym
nil
136
ref
910
remove
nil
cons
cons
nil
cons
nil
cons
cons
136
ref
27
ref
995
ref
128
ref
appTerm
appTerm
128
ref
appTerm
absTerm
1331
def
139
ref
appTerm
1332
def
betaConv
nil
260
ref
1331
ref
appTerm
1333
def
axiom
nil
91
ref
1333
remove
nil
cons
cons
94
ref
1332
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
1331
remove
nil
cons
cons
717
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
sym
142
ref
eqMp
eqMp
eqMp
nil
149
ref
1327
remove
cons
1334
def
1325
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
928
remove
1292
ref
appTerm
1335
def
betaConv
931
remove
nil
932
remove
94
ref
1335
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
933
remove
262
ref
1292
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
1334
remove
151
ref
1315
remove
cons
553
ref
1312
remove
cons
nil
cons
cons
cons
nil
cons
cons
572
ref
subst
proveHyp
proveHyp
proveHyp
eqMp
eqMp
nil
1298
ref
1308
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
136
ref
995
remove
713
remove
appTerm
absTerm
1336
def
1287
remove
appTerm
1337
def
betaConv
nil
260
ref
1336
ref
appTerm
1338
def
axiom
nil
91
ref
1338
remove
nil
cons
cons
94
ref
1337
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
1336
remove
nil
cons
cons
262
ref
1297
remove
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
1298
remove
151
ref
1289
remove
cons
553
ref
1294
remove
cons
nil
cons
cons
cons
nil
cons
cons
572
ref
subst
proveHyp
proveHyp
proveHyp
subst
eqMp
eqMp
1339
def
subst
eqMp
nil
91
ref
1174
remove
cons
734
ref
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
"_1879"
2
ref
var
1340
def
1167
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
91
ref
824
remove
34
ref
1340
remove
varTerm
1341
def
appTerm
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
27
ref
709
remove
appTerm
refl
138
remove
718
ref
subst
appThm
nil
262
ref
710
remove
cons
nil
cons
nil
cons
cons
728
remove
subst
trans
sym
142
ref
eqMp
1342
def
subst
1140
ref
1341
ref
appTerm
1343
def
betaConv
nil
149
ref
1144
remove
cons
151
ref
1141
remove
nil
cons
1344
def
cons
nil
cons
cons
nil
cons
cons
1345
def
385
ref
subst
nil
91
ref
1344
remove
cons
94
ref
1343
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
241
ref
1140
remove
nil
cons
cons
44
ref
1341
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
subst
eqMp
eqMp
nil
149
ref
1161
ref
cons
151
ref
733
ref
cons
nil
cons
1346
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
1078
remove
734
ref
cons
nil
cons
cons
1347
def
123
ref
subst
1347
remove
203
ref
subst
nil
91
ref
1010
remove
nil
cons
1348
def
cons
734
ref
cons
nil
cons
cons
1349
def
123
ref
subst
1349
remove
203
ref
subst
nil
44
ref
37
ref
nil
cons
cons
nil
cons
nil
cons
cons
769
remove
subst
nil
91
ref
18
ref
37
ref
appTerm
37
ref
appTerm
1350
def
nil
cons
cons
1351
def
734
ref
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
1351
remove
nil
cons
nil
cons
cons
1342
ref
subst
27
ref
"_1887"
2
ref
var
1352
def
45
ref
18
ref
34
ref
1352
remove
varTerm
appTerm
appTerm
37
ref
appTerm
appTerm
absTerm
1353
def
35
ref
appTerm
1354
def
appTerm
refl
1353
ref
36
ref
appTerm
betaConv
appThm
153
ref
1354
remove
betaConv
appThm
45
ref
1350
remove
appTerm
refl
appThm
trans
1353
remove
refl
nil
149
ref
1009
remove
nil
cons
cons
151
ref
963
ref
cons
nil
cons
cons
nil
cons
cons
1355
def
385
ref
subst
appThm
eqMp
1355
remove
165
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
149
ref
1348
ref
cons
1346
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
91
ref
1006
remove
nil
cons
1356
def
cons
734
ref
cons
nil
cons
cons
1357
def
123
ref
subst
1357
remove
203
ref
subst
nil
149
ref
962
remove
cons
151
ref
1005
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
1358
def
165
ref
subst
964
remove
173
ref
subst
proveHyp
nil
"_1872"
2
ref
var
1359
def
36
ref
nil
cons
1360
def
cons
"_1871"
2
ref
var
1361
def
35
ref
nil
cons
1362
def
cons
nil
cons
cons
nil
cons
cons
nil
1175
ref
45
ref
18
ref
34
ref
1361
remove
varTerm
1363
def
appTerm
appTerm
1364
def
34
ref
1359
remove
varTerm
1365
def
appTerm
appTerm
1366
def
appTerm
nil
cons
1367
def
cons
1182
ref
18
ref
1363
ref
appTerm
1368
def
1365
ref
appTerm
1369
def
nil
cons
1370
def
cons
nil
cons
cons
nil
cons
cons
1231
ref
subst
315
ref
nil
1182
ref
1366
remove
nil
cons
cons
nil
cons
nil
cons
cons
1249
ref
subst
appThm
1369
remove
refl
appThm
trans
nil
94
ref
1370
remove
cons
91
ref
1367
remove
cons
nil
cons
cons
nil
cons
cons
1267
ref
subst
26
ref
14
ref
45
ref
1364
remove
37
remove
appTerm
appTerm
appTerm
1368
remove
36
ref
appTerm
appTerm
absTerm
1371
def
1365
ref
appTerm
1372
def
betaConv
1136
ref
1363
ref
appTerm
1373
def
betaConv
1345
remove
165
ref
subst
nil
1145
remove
94
ref
1373
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
241
ref
1136
remove
nil
cons
cons
44
ref
1363
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
13
ref
1371
ref
appTerm
nil
cons
cons
94
ref
1372
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
241
ref
1371
remove
nil
cons
cons
44
ref
1365
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
eqMp
subst
eqMp
nil
91
ref
963
remove
cons
1374
def
734
ref
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
1374
remove
nil
cons
nil
cons
cons
1342
ref
subst
1358
remove
385
ref
subst
eqMp
eqMp
eqMp
nil
149
ref
1356
remove
cons
1375
def
1346
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
1375
remove
151
ref
1348
remove
cons
553
ref
733
remove
cons
nil
cons
1376
def
cons
cons
nil
cons
cons
572
ref
subst
proveHyp
proveHyp
eqMp
nil
149
ref
1077
remove
cons
1377
def
1346
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
1377
remove
151
ref
1161
remove
cons
1376
remove
cons
cons
nil
cons
cons
572
ref
subst
proveHyp
proveHyp
eqMp
nil
149
ref
1159
remove
cons
1346
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
149
ref
1157
remove
cons
1346
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
91
ref
13
ref
44
ref
12
ref
1153
ref
46
ref
appTerm
appTerm
712
ref
appTerm
absTerm
appTerm
nil
cons
cons
94
ref
12
ref
1154
remove
appTerm
712
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
241
ref
1153
remove
nil
cons
cons
1346
ref
cons
nil
cons
cons
499
ref
subst
eqMp
eqMp
eqMp
nil
149
ref
1105
remove
cons
1346
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
149
ref
1103
remove
cons
1346
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
91
ref
834
ref
"x"
28
remove
var
1378
def
12
ref
1087
ref
1378
ref
varTerm
1379
def
appTerm
appTerm
712
ref
appTerm
absTerm
appTerm
nil
cons
cons
94
ref
12
ref
1088
remove
appTerm
712
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
784
ref
781
ref
1087
remove
nil
cons
cons
1346
ref
cons
nil
cons
cons
499
ref
subst
eqMp
eqMp
eqMp
nil
149
ref
1099
remove
cons
1346
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
91
ref
13
ref
44
ref
12
ref
1089
ref
46
ref
appTerm
appTerm
712
ref
appTerm
absTerm
appTerm
nil
cons
cons
94
ref
12
ref
1090
remove
appTerm
712
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
241
ref
1089
remove
nil
cons
cons
1346
ref
cons
nil
cons
cons
499
ref
subst
eqMp
eqMp
eqMp
nil
149
ref
1095
remove
cons
1346
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
91
ref
13
ref
44
ref
12
ref
1091
ref
46
remove
appTerm
appTerm
712
ref
appTerm
absTerm
appTerm
nil
cons
cons
94
ref
12
ref
1092
remove
appTerm
712
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
241
ref
1091
remove
nil
cons
cons
1346
ref
cons
nil
cons
cons
499
ref
subst
eqMp
eqMp
eqMp
nil
149
ref
855
remove
cons
1346
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
149
ref
851
remove
cons
151
ref
852
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
91
ref
834
ref
832
ref
appTerm
nil
cons
cons
94
ref
833
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
784
ref
781
ref
832
remove
nil
cons
cons
1378
ref
34
remove
nil
cons
cons
nil
cons
1380
def
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
784
ref
781
ref
53
remove
nil
cons
1381
def
cons
1380
remove
cons
nil
cons
cons
515
ref
subst
proveHyp
eqMp
nil
149
ref
789
remove
cons
151
ref
779
ref
cons
nil
cons
1382
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
149
ref
787
remove
cons
1382
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
91
ref
834
remove
1378
remove
12
ref
776
ref
1379
remove
appTerm
appTerm
778
ref
appTerm
absTerm
appTerm
nil
cons
cons
94
ref
12
ref
777
remove
appTerm
778
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
784
ref
781
remove
776
remove
nil
cons
cons
1382
remove
cons
nil
cons
cons
499
ref
subst
eqMp
eqMp
nil
91
ref
779
remove
cons
94
ref
770
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
784
remove
"p"
29
remove
var
1381
remove
cons
nil
cons
nil
cons
cons
nil
91
ref
329
ref
224
ref
appTerm
1383
def
nil
cons
1384
def
cons
1385
def
94
ref
27
ref
224
ref
21
remove
1
ref
217
ref
508
remove
cons
opType
constTerm
224
ref
appTerm
appTerm
1386
def
appTerm
1387
def
128
ref
appTerm
1388
def
nil
cons
1389
def
cons
nil
cons
1390
def
cons
nil
cons
cons
1391
def
123
ref
subst
1391
remove
203
ref
subst
1000
remove
nil
936
remove
345
ref
cons
nil
cons
nil
cons
cons
939
remove
948
ref
942
remove
appTerm
1392
def
betaConv
950
remove
nil
91
ref
949
remove
nil
cons
cons
94
ref
1392
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
811
ref
812
ref
948
remove
nil
cons
cons
951
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
subst
appThm
nil
136
ref
1384
ref
cons
nil
cons
nil
cons
cons
1393
def
143
ref
subst
1383
ref
assume
eqMp
trans
sym
142
ref
eqMp
nil
91
ref
331
remove
nil
cons
cons
1390
ref
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
220
ref
345
remove
cons
151
ref
1389
remove
cons
nil
cons
1394
def
cons
nil
cons
cons
nil
471
remove
94
ref
12
ref
329
remove
225
ref
266
ref
absTerm
1395
def
appTerm
1396
def
appTerm
156
ref
appTerm
1397
def
nil
cons
1398
def
cons
nil
cons
1399
def
cons
nil
cons
cons
1400
def
386
ref
subst
1400
ref
123
ref
subst
1400
remove
203
ref
subst
nil
220
ref
225
ref
12
ref
1395
ref
265
ref
appTerm
1401
def
appTerm
156
remove
appTerm
1402
def
absTerm
1403
def
nil
cons
cons
nil
cons
nil
cons
cons
233
ref
subst
225
ref
nil
136
ref
1402
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
91
ref
1401
ref
nil
cons
1404
def
cons
479
ref
cons
nil
cons
cons
1405
def
123
ref
subst
1405
remove
203
ref
subst
nil
"f"
217
remove
var
937
remove
cons
1285
ref
512
remove
cons
nil
cons
cons
nil
cons
cons
938
remove
510
ref
cons
215
ref
cons
1285
remove
803
remove
225
ref
818
remove
absTerm
1286
ref
appTerm
appTerm
798
ref
1286
ref
appTerm
appTerm
absTerm
1406
def
1286
remove
appTerm
1407
def
betaConv
796
remove
219
ref
1406
ref
appTerm
1408
def
absTerm
1409
def
798
remove
appTerm
1410
def
betaConv
nil
809
remove
1409
ref
appTerm
1411
def
axiom
nil
91
ref
1411
remove
nil
cons
cons
94
ref
1410
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
811
remove
812
remove
1409
remove
nil
cons
cons
814
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
1408
remove
nil
cons
cons
94
ref
1407
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
510
ref
220
ref
1406
remove
nil
cons
cons
1311
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
subst
1412
def
1401
remove
assume
eqMp
506
remove
proveHyp
514
remove
eqMp
eqMp
nil
149
ref
1404
remove
cons
497
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
91
ref
219
ref
1403
remove
appTerm
nil
cons
cons
1399
remove
cons
nil
cons
cons
173
ref
subst
proveHyp
510
ref
220
ref
1395
remove
nil
cons
cons
1413
def
497
ref
cons
nil
cons
cons
499
ref
subst
eqMp
eqMp
nil
498
remove
151
ref
1398
ref
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
91
ref
503
remove
1397
ref
appTerm
nil
cons
cons
94
ref
12
ref
1397
ref
appTerm
469
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
203
ref
subst
proveHyp
nil
91
ref
1398
ref
cons
94
ref
470
ref
cons
nil
cons
cons
nil
cons
cons
1414
def
123
ref
subst
1414
remove
203
ref
subst
nil
511
remove
nil
cons
nil
cons
cons
233
ref
subst
225
ref
nil
136
ref
467
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
505
ref
123
ref
subst
505
remove
203
ref
subst
1412
remove
sym
266
remove
assume
eqMp
510
ref
1413
remove
513
ref
cons
nil
cons
cons
515
remove
subst
proveHyp
nil
91
ref
1396
remove
nil
cons
cons
479
remove
cons
nil
cons
cons
173
ref
subst
1397
remove
assume
eqMp
proveHyp
eqMp
nil
149
ref
267
remove
cons
497
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
149
ref
1398
remove
cons
151
ref
470
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
subst
nil
220
ref
225
ref
326
ref
1388
ref
appTerm
1415
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
233
ref
subst
225
ref
nil
136
ref
1415
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
91
ref
325
ref
nil
cons
1416
def
cons
1417
def
1390
remove
cons
nil
cons
cons
1418
def
123
ref
subst
1418
remove
203
ref
subst
nil
136
ref
1386
ref
nil
cons
1419
def
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
1417
remove
94
ref
1419
remove
cons
1420
def
nil
cons
cons
nil
cons
cons
173
ref
subst
225
ref
326
remove
1386
ref
appTerm
absTerm
1421
def
265
remove
appTerm
1422
def
betaConv
223
ref
219
ref
1421
ref
appTerm
1423
def
absTerm
1424
def
224
ref
appTerm
1425
def
betaConv
nil
336
ref
1424
ref
appTerm
1426
def
axiom
nil
91
ref
1426
remove
nil
cons
cons
94
ref
1425
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
342
ref
343
ref
1424
remove
nil
cons
cons
346
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
1423
remove
nil
cons
cons
94
ref
1422
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
510
remove
220
remove
1421
remove
nil
cons
cons
513
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
eqMp
eqMp
nil
149
ref
1416
remove
cons
1394
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
eqMp
eqMp
nil
149
ref
1384
ref
cons
1394
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
91
ref
12
ref
1383
ref
appTerm
1427
def
1388
remove
appTerm
nil
cons
cons
94
ref
27
ref
1427
ref
1386
remove
appTerm
appTerm
1428
def
1427
ref
128
ref
appTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
"q'"
4
ref
var
1429
def
893
remove
cons
nil
cons
nil
cons
cons
1383
ref
refl
nil
91
ref
27
ref
1383
ref
appTerm
1430
def
1383
remove
appTerm
nil
cons
cons
94
ref
12
ref
1427
ref
1387
remove
1429
ref
varTerm
1431
def
appTerm
1432
def
appTerm
appTerm
1428
ref
1427
remove
1431
ref
appTerm
appTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
"p'"
4
ref
var
1433
def
1384
remove
cons
nil
cons
nil
cons
cons
1429
ref
12
ref
1430
remove
1433
ref
varTerm
1434
def
appTerm
appTerm
12
ref
12
ref
1434
ref
appTerm
1435
def
1432
remove
appTerm
appTerm
1428
remove
1435
ref
1431
ref
appTerm
1436
def
appTerm
appTerm
appTerm
absTerm
1437
def
1431
ref
appTerm
1438
def
betaConv
1433
ref
260
ref
1437
ref
appTerm
1439
def
absTerm
1440
def
1434
ref
appTerm
1441
def
betaConv
nil
1420
remove
1385
remove
nil
cons
cons
nil
cons
cons
nil
251
ref
1433
ref
260
ref
1429
ref
12
ref
368
remove
1434
ref
appTerm
1442
def
appTerm
12
ref
1435
ref
27
ref
110
ref
appTerm
1431
ref
appTerm
1443
def
appTerm
1444
def
appTerm
112
remove
1436
ref
appTerm
1445
def
appTerm
1446
def
appTerm
1447
def
absTerm
1448
def
appTerm
1449
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
255
ref
subst
1433
remove
nil
136
ref
1449
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
251
ref
1448
remove
nil
cons
cons
nil
cons
nil
cons
cons
255
remove
subst
1429
remove
nil
136
ref
1447
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
91
ref
1442
remove
nil
cons
1450
def
cons
1451
def
94
ref
1446
remove
nil
cons
1452
def
cons
nil
cons
cons
nil
cons
cons
1453
def
123
ref
subst
1453
remove
203
ref
subst
nil
91
ref
1444
ref
nil
cons
1454
def
cons
94
ref
1445
remove
nil
cons
1455
def
cons
nil
cons
cons
nil
cons
cons
1456
def
123
ref
subst
1456
remove
203
ref
subst
nil
377
remove
94
ref
1436
ref
nil
cons
1457
def
cons
nil
cons
cons
nil
cons
cons
1458
def
386
ref
subst
1458
ref
123
ref
subst
1458
remove
203
ref
subst
nil
91
ref
1434
ref
nil
cons
1459
def
cons
1460
def
94
ref
1431
ref
nil
cons
1461
def
cons
nil
cons
1462
def
cons
nil
cons
cons
1463
def
123
ref
subst
1463
ref
203
ref
subst
nil
1451
ref
94
ref
109
remove
1434
remove
appTerm
1464
def
nil
cons
1465
def
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
nil
256
remove
94
ref
1459
ref
cons
nil
cons
cons
nil
cons
cons
1466
def
496
ref
subst
eqMp
1467
def
nil
91
ref
1465
ref
cons
1468
def
1462
ref
cons
nil
cons
cons
1469
def
173
ref
subst
proveHyp
nil
1451
remove
94
ref
1435
remove
108
ref
appTerm
1470
def
nil
cons
1471
def
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
1466
ref
nil
491
remove
380
remove
cons
nil
cons
cons
1472
def
123
ref
subst
1472
remove
203
ref
subst
381
remove
eqMp
nil
494
remove
383
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
1473
def
subst
eqMp
1474
def
nil
91
ref
1471
ref
cons
1475
def
94
ref
12
ref
1464
ref
appTerm
1476
def
1431
ref
appTerm
nil
cons
1477
def
cons
nil
cons
cons
nil
cons
cons
1478
def
173
ref
subst
proveHyp
1478
ref
123
ref
subst
1478
remove
203
ref
subst
1469
ref
123
ref
subst
1469
remove
203
ref
subst
nil
1460
ref
257
remove
cons
nil
cons
cons
173
ref
subst
1470
remove
assume
eqMp
1479
def
1466
remove
173
ref
subst
1464
remove
assume
eqMp
1480
def
1479
remove
proveHyp
proveHyp
nil
1460
remove
94
ref
1443
remove
nil
cons
1481
def
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
1444
remove
assume
eqMp
1482
def
nil
91
ref
1481
remove
cons
1483
def
94
ref
378
remove
1431
ref
appTerm
1484
def
nil
cons
1485
def
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
371
remove
1462
ref
cons
nil
cons
cons
1486
def
496
remove
subst
eqMp
1487
def
nil
91
ref
1485
ref
cons
1488
def
1462
remove
cons
nil
cons
cons
1489
def
173
ref
subst
proveHyp
1482
remove
nil
1483
remove
94
ref
12
ref
1431
ref
appTerm
110
ref
appTerm
1490
def
nil
cons
1491
def
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
1486
ref
1473
remove
subst
eqMp
1492
def
nil
91
ref
1491
ref
cons
1493
def
94
ref
12
ref
1484
ref
appTerm
1494
def
1431
remove
appTerm
nil
cons
1495
def
cons
nil
cons
cons
nil
cons
cons
1496
def
173
ref
subst
proveHyp
1496
ref
123
ref
subst
1496
remove
203
ref
subst
1489
ref
123
ref
subst
1489
remove
203
ref
subst
172
remove
1486
remove
173
ref
subst
1484
remove
assume
eqMp
proveHyp
eqMp
nil
149
ref
1485
remove
cons
1497
def
151
ref
1461
ref
cons
nil
cons
1498
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
nil
149
ref
1491
remove
cons
1499
def
151
ref
1495
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
proveHyp
eqMp
nil
149
ref
1465
remove
cons
1500
def
1498
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
nil
149
ref
1471
remove
cons
1501
def
151
ref
1477
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
149
ref
1459
ref
cons
1498
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
nil
382
remove
151
ref
1457
ref
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
91
ref
12
ref
111
ref
appTerm
1436
ref
appTerm
nil
cons
cons
94
ref
12
ref
1436
ref
appTerm
111
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
203
ref
subst
proveHyp
nil
91
ref
1457
ref
cons
492
remove
cons
nil
cons
cons
1502
def
123
ref
subst
1502
remove
203
ref
subst
123
ref
203
ref
1467
remove
nil
1468
remove
372
ref
cons
nil
cons
cons
1503
def
173
ref
subst
proveHyp
1474
remove
nil
1475
remove
94
ref
1476
remove
110
ref
appTerm
nil
cons
1504
def
cons
nil
cons
cons
nil
cons
cons
1505
def
173
ref
subst
proveHyp
1505
ref
123
ref
subst
1505
remove
203
ref
subst
1503
ref
123
ref
subst
1503
remove
203
ref
subst
1480
remove
1487
remove
nil
1488
remove
372
ref
cons
nil
cons
cons
1506
def
173
ref
subst
proveHyp
1492
remove
nil
1493
remove
94
ref
1494
remove
110
ref
appTerm
nil
cons
1507
def
cons
nil
cons
cons
nil
cons
cons
1508
def
173
ref
subst
proveHyp
1508
ref
123
ref
subst
1508
remove
203
ref
subst
1506
ref
123
ref
subst
1506
remove
203
ref
subst
1463
remove
173
ref
subst
1436
remove
assume
eqMp
nil
91
ref
1461
ref
cons
372
remove
cons
nil
cons
cons
173
ref
subst
1490
remove
assume
eqMp
proveHyp
eqMp
nil
1497
remove
152
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
nil
1499
remove
151
ref
1507
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
proveHyp
eqMp
nil
1500
remove
152
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
nil
1501
remove
151
ref
1504
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
166
remove
deductAntisym
eqMp
eqMp
nil
149
ref
1457
remove
cons
495
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
149
ref
1454
remove
cons
151
ref
1455
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
nil
149
ref
1450
remove
cons
151
ref
1452
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
subst
nil
91
ref
260
ref
1440
ref
appTerm
nil
cons
cons
94
ref
1441
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
1440
remove
nil
cons
cons
262
ref
1459
remove
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
1439
remove
nil
cons
cons
94
ref
1438
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
1437
remove
nil
cons
cons
262
remove
1461
remove
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
eqMp
subst
eqMp
1393
remove
1225
remove
subst
trans
sym
142
ref
eqMp
1509
def
subst
eqMp
eqMp
eqMp
nil
91
ref
33
remove
63
ref
appTerm
nil
cons
cons
94
ref
765
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
321
ref
63
remove
nil
cons
cons
nil
cons
nil
cons
cons
1509
remove
subst
eqMp
eqMp
eqMp
1510
def
nil
149
ref
60
remove
nil
cons
1511
def
cons
151
ref
13
ref
44
ref
45
ref
62
remove
66
ref
appTerm
appTerm
absTerm
1512
def
appTerm
1513
def
nil
cons
1514
def
cons
nil
cons
cons
nil
cons
cons
1515
def
385
ref
subst
proveHyp
nil
91
ref
1514
ref
cons
1516
def
94
ref
12
ref
760
ref
appTerm
1517
def
764
remove
appTerm
1518
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
732
ref
94
ref
12
ref
1513
remove
appTerm
1519
def
1518
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
12
ref
730
ref
appTerm
refl
1519
ref
refl
1517
ref
refl
763
ref
refl
nil
136
ref
664
remove
cons
nil
cons
nil
cons
cons
718
remove
subst
1520
def
appThm
appThm
appThm
appThm
sym
nil
732
remove
94
ref
1519
remove
1517
remove
763
remove
45
ref
100
ref
appTerm
1521
def
appTerm
1522
def
appTerm
1523
def
appTerm
nil
cons
1524
def
cons
nil
cons
cons
nil
cons
cons
1525
def
123
ref
subst
1525
remove
203
ref
subst
nil
1516
ref
94
ref
1523
remove
nil
cons
1526
def
cons
nil
cons
cons
nil
cons
cons
1527
def
123
ref
subst
1527
remove
203
ref
subst
nil
762
remove
94
ref
1522
remove
nil
cons
1528
def
cons
nil
cons
cons
nil
cons
cons
1529
def
123
ref
subst
1529
remove
203
ref
subst
nil
750
ref
94
ref
1521
remove
nil
cons
1530
def
cons
nil
cons
cons
nil
cons
cons
1531
def
123
ref
subst
1531
remove
203
ref
subst
1520
remove
736
ref
123
ref
subst
736
remove
203
ref
subst
nil
737
ref
706
ref
nil
cons
cons
nil
cons
nil
cons
cons
745
remove
960
remove
subst
subst
32
remove
680
ref
constTerm
1532
def
refl
683
ref
684
remove
706
remove
689
ref
appTerm
betaConv
appThm
nil
91
ref
705
ref
nil
cons
1533
def
cons
1534
def
nil
cons
nil
cons
cons
723
remove
subst
trans
absThm
appThm
trans
730
remove
assume
eqMp
nil
91
ref
1532
remove
683
ref
705
remove
absTerm
1535
def
appTerm
1536
def
nil
cons
cons
734
ref
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
737
ref
683
ref
12
ref
1535
ref
689
ref
appTerm
1537
def
appTerm
712
ref
appTerm
1538
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
746
ref
subst
683
ref
nil
136
ref
1538
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
91
ref
1537
ref
nil
cons
1539
def
cons
734
ref
cons
nil
cons
cons
1540
def
123
ref
subst
1540
remove
203
ref
subst
1537
ref
betaConv
1537
remove
assume
eqMp
nil
1534
ref
734
ref
cons
nil
cons
cons
1541
def
173
ref
subst
proveHyp
1541
ref
123
ref
subst
1541
remove
203
ref
subst
nil
1534
remove
94
ref
18
ref
693
ref
704
ref
appTerm
1542
def
appTerm
1543
def
693
ref
699
ref
appTerm
1544
def
appTerm
1545
def
nil
cons
1546
def
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
nil
"_1914"
678
ref
var
1547
def
699
ref
nil
cons
cons
"_1913"
678
ref
var
1548
def
704
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
91
ref
686
ref
1548
ref
varTerm
1549
def
appTerm
1547
ref
varTerm
1550
def
appTerm
1551
def
nil
cons
1552
def
cons
94
ref
18
ref
693
ref
1549
remove
appTerm
appTerm
693
ref
1550
remove
appTerm
appTerm
nil
cons
1553
def
cons
nil
cons
cons
nil
cons
cons
1554
def
123
ref
subst
1554
remove
203
ref
subst
693
ref
refl
1555
def
1551
remove
assume
appThm
eqMp
nil
149
ref
1552
remove
cons
151
ref
1553
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
1556
def
subst
eqMp
nil
91
ref
1546
remove
cons
94
ref
1543
remove
703
ref
appTerm
1557
def
nil
cons
cons
nil
cons
1558
def
cons
nil
cons
cons
203
ref
subst
proveHyp
nil
"_1907"
678
ref
var
1559
def
690
ref
cons
nil
cons
nil
cons
cons
742
remove
1559
remove
varTerm
1560
def
appTerm
1561
def
betaConv
nil
750
remove
94
ref
1561
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
744
ref
743
remove
"x"
678
ref
var
1562
def
1560
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
nil
91
ref
686
ref
692
ref
702
ref
appTerm
1563
def
appTerm
689
ref
appTerm
nil
cons
cons
94
ref
18
ref
693
ref
1563
ref
appTerm
appTerm
702
ref
appTerm
nil
cons
1564
def
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
1547
remove
690
ref
cons
1548
remove
1563
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
1556
remove
subst
eqMp
nil
91
ref
1564
remove
cons
94
ref
93
ref
702
ref
appTerm
1565
def
nil
cons
1566
def
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
"_1909"
2
ref
var
1567
def
702
ref
nil
cons
1568
def
cons
nil
cons
nil
cons
cons
nil
1175
ref
45
ref
18
ref
693
ref
692
ref
1567
remove
varTerm
1569
def
appTerm
appTerm
appTerm
1569
ref
appTerm
1570
def
appTerm
nil
cons
cons
1182
ref
93
ref
1569
ref
appTerm
1571
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
1231
ref
subst
315
ref
nil
1182
ref
1570
remove
nil
cons
cons
nil
cons
nil
cons
cons
1249
ref
subst
appThm
1571
remove
refl
appThm
trans
752
ref
14
ref
754
ref
appTerm
45
ref
755
ref
appTerm
appTerm
absTerm
1572
def
1569
ref
appTerm
1573
def
betaConv
316
ref
752
ref
nil
91
ref
754
ref
nil
cons
cons
94
ref
755
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
859
remove
94
ref
27
ref
369
remove
appTerm
24
ref
1079
remove
861
ref
appTerm
appTerm
1107
remove
appTerm
appTerm
nil
cons
1574
def
cons
nil
cons
1575
def
cons
nil
cons
cons
1576
def
123
ref
subst
1576
remove
203
ref
subst
27
ref
"_554"
4
ref
var
1577
def
27
ref
27
ref
1577
remove
varTerm
1578
def
appTerm
110
ref
appTerm
appTerm
24
ref
14
ref
1578
ref
appTerm
861
ref
appTerm
appTerm
14
ref
45
ref
1578
remove
appTerm
appTerm
110
ref
appTerm
appTerm
appTerm
absTerm
1579
def
108
remove
appTerm
1580
def
appTerm
refl
1581
def
1579
ref
712
ref
appTerm
betaConv
appThm
153
ref
1580
remove
betaConv
appThm
1582
def
27
ref
975
remove
appTerm
24
ref
920
remove
861
ref
appTerm
appTerm
1118
remove
appTerm
appTerm
refl
appThm
trans
1579
remove
refl
1583
def
875
remove
appThm
eqMp
sym
153
ref
982
remove
appThm
361
ref
925
remove
appThm
1123
remove
appThm
886
remove
136
ref
27
ref
24
ref
139
ref
appTerm
128
ref
appTerm
appTerm
139
ref
appTerm
absTerm
1584
def
139
ref
appTerm
1585
def
betaConv
nil
260
ref
1584
ref
appTerm
1586
def
axiom
nil
91
ref
1586
remove
nil
cons
cons
94
ref
1585
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
1584
remove
nil
cons
cons
717
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
trans
appThm
926
remove
trans
sym
142
ref
eqMp
eqMp
eqMp
nil
901
remove
151
ref
1574
ref
cons
nil
cons
1587
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
905
remove
1575
remove
cons
nil
cons
cons
1588
def
123
ref
subst
1588
remove
203
ref
subst
1581
remove
"_552"
4
remove
var
1589
def
27
ref
27
ref
1589
remove
varTerm
1590
def
appTerm
110
ref
appTerm
appTerm
24
ref
14
ref
1590
ref
appTerm
861
ref
appTerm
appTerm
14
ref
45
ref
1590
remove
appTerm
appTerm
110
remove
appTerm
appTerm
appTerm
absTerm
128
remove
appTerm
betaConv
appThm
1582
remove
27
ref
991
remove
appTerm
24
ref
887
remove
861
remove
appTerm
appTerm
1129
remove
appTerm
appTerm
refl
appThm
trans
1583
remove
912
remove
appThm
eqMp
sym
153
ref
993
remove
appThm
361
ref
892
remove
appThm
1134
remove
appThm
917
remove
trans
appThm
986
remove
trans
sym
142
ref
eqMp
eqMp
eqMp
nil
927
ref
1587
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
934
remove
nil
927
remove
935
remove
553
remove
1574
remove
cons
nil
cons
cons
cons
nil
cons
cons
572
remove
subst
proveHyp
proveHyp
proveHyp
subst
absThm
appThm
153
ref
316
ref
752
ref
361
ref
1572
ref
753
ref
appTerm
betaConv
1591
def
appThm
752
ref
14
ref
45
ref
754
remove
appTerm
appTerm
755
remove
appTerm
absTerm
1592
def
753
remove
appTerm
betaConv
1593
def
appThm
absThm
appThm
appThm
361
ref
316
ref
752
ref
1591
remove
absThm
appThm
appThm
316
ref
752
ref
1593
remove
absThm
appThm
appThm
appThm
nil
321
remove
1572
ref
nil
cons
1594
def
cons
323
remove
1592
ref
nil
cons
1595
def
cons
nil
cons
cons
nil
cons
cons
245
ref
324
remove
27
ref
219
ref
225
ref
24
ref
325
remove
appTerm
328
remove
appTerm
absTerm
appTerm
appTerm
24
ref
955
remove
appTerm
219
ref
332
remove
appTerm
appTerm
appTerm
absTerm
1596
def
327
remove
appTerm
1597
def
betaConv
223
remove
336
ref
1596
ref
appTerm
1598
def
absTerm
1599
def
224
remove
appTerm
1600
def
betaConv
nil
336
remove
1599
ref
appTerm
1601
def
axiom
nil
91
ref
1601
remove
nil
cons
cons
94
ref
1600
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
342
ref
343
ref
1599
remove
nil
cons
cons
346
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
1598
remove
nil
cons
cons
94
ref
1597
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
342
remove
343
remove
1596
remove
nil
cons
cons
347
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
subst
eqMp
trans
760
remove
assume
eqMp
1602
def
nil
149
ref
13
ref
1572
remove
appTerm
nil
cons
1603
def
cons
151
ref
13
ref
1592
ref
appTerm
nil
cons
1604
def
cons
nil
cons
cons
nil
cons
cons
1605
def
165
ref
subst
proveHyp
nil
91
ref
1603
remove
cons
94
ref
1573
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
241
ref
1594
remove
cons
44
ref
1569
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
subst
eqMp
nil
91
ref
1566
remove
cons
94
ref
93
ref
703
ref
appTerm
nil
cons
1606
def
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
"_1908"
2
ref
var
1607
def
1568
ref
cons
nil
cons
nil
cons
cons
nil
1175
ref
45
ref
93
ref
1607
remove
varTerm
1608
def
appTerm
1609
def
appTerm
nil
cons
1610
def
cons
1182
ref
93
ref
56
ref
1608
ref
appTerm
appTerm
1611
def
nil
cons
1612
def
cons
nil
cons
cons
nil
cons
cons
1231
ref
subst
315
ref
nil
1182
ref
1609
remove
nil
cons
cons
nil
cons
nil
cons
cons
1249
ref
subst
appThm
1611
remove
refl
appThm
trans
nil
94
ref
1612
remove
cons
91
ref
1610
remove
cons
nil
cons
cons
nil
cons
cons
1267
ref
subst
69
ref
14
remove
45
ref
96
ref
appTerm
appTerm
97
ref
appTerm
absTerm
1613
def
1608
ref
appTerm
1614
def
betaConv
361
ref
93
ref
refl
403
remove
appThm
appThm
316
ref
69
ref
nil
91
ref
96
ref
nil
cons
1615
def
cons
94
ref
97
ref
nil
cons
1616
def
cons
nil
cons
cons
nil
cons
cons
1617
def
1135
remove
subst
absThm
appThm
appThm
100
remove
assume
eqMp
nil
669
remove
151
ref
13
ref
1613
ref
appTerm
nil
cons
1618
def
cons
nil
cons
cons
nil
cons
cons
385
ref
subst
proveHyp
nil
91
ref
1618
remove
cons
94
ref
1614
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
241
ref
1613
remove
nil
cons
cons
44
ref
1608
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
eqMp
subst
eqMp
nil
91
ref
1606
remove
cons
1558
remove
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
"_1910"
2
ref
var
1619
def
703
ref
nil
cons
1620
def
cons
nil
cons
nil
cons
cons
nil
1175
remove
45
ref
93
ref
1619
ref
varTerm
1621
def
appTerm
1622
def
appTerm
nil
cons
1623
def
cons
1182
ref
18
ref
693
ref
692
ref
1621
ref
appTerm
appTerm
appTerm
1621
ref
appTerm
1624
def
nil
cons
1625
def
cons
nil
cons
cons
nil
cons
cons
1231
remove
subst
315
ref
nil
1182
remove
1622
remove
nil
cons
cons
nil
cons
nil
cons
cons
1249
remove
subst
appThm
1624
remove
refl
appThm
trans
nil
94
ref
1625
remove
cons
91
ref
1623
remove
cons
nil
cons
cons
nil
cons
cons
1267
remove
subst
1592
remove
1621
ref
appTerm
1626
def
betaConv
1602
remove
1605
remove
385
ref
subst
proveHyp
nil
91
ref
1604
remove
cons
94
ref
1626
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
241
ref
1595
remove
cons
44
ref
1621
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
eqMp
1627
def
subst
eqMp
eqMp
nil
91
ref
24
ref
1545
remove
appTerm
1557
remove
appTerm
nil
cons
cons
94
ref
18
ref
1544
ref
appTerm
1628
def
703
ref
appTerm
1629
def
nil
cons
1630
def
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
23
ref
1620
ref
cons
822
ref
1544
remove
nil
cons
1631
def
cons
44
ref
1542
ref
nil
cons
cons
nil
cons
cons
cons
nil
cons
cons
1339
ref
subst
eqMp
nil
91
ref
1630
remove
cons
94
ref
1628
remove
66
ref
appTerm
1632
def
nil
cons
cons
nil
cons
1633
def
cons
nil
cons
cons
203
ref
subst
proveHyp
672
remove
nil
91
ref
668
ref
cons
1633
remove
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
1619
remove
406
ref
cons
nil
cons
nil
cons
cons
1627
remove
subst
eqMp
eqMp
nil
91
ref
24
ref
1629
remove
appTerm
1632
remove
appTerm
nil
cons
cons
94
ref
18
ref
703
remove
appTerm
66
ref
appTerm
nil
cons
1634
def
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
23
remove
406
remove
cons
822
remove
1620
remove
cons
44
ref
1631
remove
cons
nil
cons
cons
cons
nil
cons
cons
1339
remove
subst
eqMp
nil
91
ref
1634
remove
cons
734
remove
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
"_1906"
2
remove
var
1635
def
1568
ref
cons
nil
cons
nil
cons
cons
nil
91
ref
18
ref
56
ref
1635
remove
varTerm
1636
def
appTerm
appTerm
66
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
1342
remove
subst
1512
ref
1636
ref
appTerm
1637
def
betaConv
nil
1516
remove
94
ref
1637
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
244
ref
241
ref
1512
remove
nil
cons
cons
44
ref
1636
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
subst
eqMp
eqMp
nil
149
ref
1533
remove
cons
1346
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
149
ref
1539
remove
cons
1346
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
91
ref
681
ref
1562
ref
12
ref
1535
ref
1562
ref
varTerm
appTerm
appTerm
712
ref
appTerm
absTerm
appTerm
nil
cons
cons
94
ref
12
ref
1536
remove
appTerm
712
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
744
ref
737
ref
1535
remove
nil
cons
cons
1346
ref
cons
nil
cons
cons
499
remove
subst
eqMp
eqMp
eqMp
nil
665
remove
1346
ref
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
149
ref
749
remove
cons
151
ref
1530
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
nil
149
ref
761
remove
cons
151
ref
1528
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
nil
149
ref
1514
remove
cons
151
ref
1526
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
nil
149
ref
731
remove
cons
1638
def
151
ref
1524
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
nil
1638
remove
1346
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
681
ref
683
ref
45
remove
686
ref
697
remove
1
ref
678
ref
691
remove
cons
opType
constTerm
1639
def
689
ref
appTerm
1640
def
appTerm
701
remove
678
ref
constTerm
1641
def
appTerm
appTerm
absTerm
appTerm
thm
nil
737
ref
"m"
678
ref
var
1642
def
681
ref
683
ref
27
ref
686
ref
1639
ref
1642
ref
varTerm
1643
def
appTerm
appTerm
1640
ref
appTerm
appTerm
686
ref
1643
ref
appTerm
689
ref
appTerm
1644
def
appTerm
1645
def
absTerm
1646
def
appTerm
1647
def
absTerm
1648
def
nil
cons
cons
nil
cons
nil
cons
cons
746
ref
subst
1642
remove
nil
136
ref
1647
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
737
ref
1646
remove
nil
cons
cons
nil
cons
nil
cons
cons
746
ref
subst
683
ref
nil
136
ref
1645
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
153
ref
687
ref
nil
683
ref
1643
ref
nil
cons
1649
def
cons
nil
cons
nil
cons
cons
698
ref
subst
appThm
698
ref
appThm
appThm
1644
ref
refl
1650
def
appThm
sym
nil
91
ref
686
ref
692
ref
56
ref
693
ref
1643
remove
appTerm
1651
def
appTerm
appTerm
1652
def
appTerm
704
remove
appTerm
1653
def
nil
cons
1654
def
cons
94
ref
1644
ref
nil
cons
1655
def
cons
nil
cons
1656
def
cons
nil
cons
cons
1657
def
386
remove
subst
1657
ref
123
ref
subst
1657
remove
203
ref
subst
1555
ref
1653
ref
assume
appThm
nil
91
ref
18
ref
693
ref
1652
remove
appTerm
appTerm
1542
remove
appTerm
1658
def
nil
cons
cons
1656
ref
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
737
ref
"p"
678
ref
var
1659
def
93
ref
56
ref
693
ref
1659
ref
varTerm
1660
def
appTerm
1661
def
appTerm
1662
def
appTerm
1663
def
absTerm
1664
def
nil
cons
cons
nil
cons
nil
cons
cons
746
ref
subst
1659
ref
nil
136
ref
1663
remove
nil
cons
1665
def
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
752
ref
1661
ref
nil
cons
1666
def
cons
nil
cons
nil
cons
cons
759
ref
subst
766
ref
1555
ref
nil
738
ref
1660
ref
nil
cons
1667
def
cons
nil
cons
nil
cons
cons
747
ref
subst
appThm
appThm
1661
ref
refl
appThm
nil
44
ref
1666
ref
cons
nil
cons
nil
cons
cons
245
ref
727
remove
subst
1668
def
subst
trans
trans
sym
142
ref
eqMp
nil
91
ref
93
remove
1661
remove
appTerm
nil
cons
cons
94
ref
1665
remove
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
nil
69
ref
1666
remove
cons
nil
cons
nil
cons
cons
98
ref
70
ref
appTerm
1669
def
betaConv
667
remove
671
remove
385
ref
subst
proveHyp
nil
91
ref
670
remove
cons
94
ref
1669
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
241
ref
98
remove
nil
cons
cons
433
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
1670
def
subst
eqMp
eqMp
absThm
eqMp
nil
91
ref
681
ref
1664
remove
appTerm
nil
cons
cons
94
ref
12
ref
1658
remove
appTerm
1644
ref
appTerm
1671
def
nil
cons
1672
def
cons
nil
cons
1673
def
cons
nil
cons
cons
173
ref
subst
315
ref
682
remove
1659
ref
nil
752
ref
1662
ref
nil
cons
cons
nil
cons
nil
cons
cons
759
ref
subst
absThm
appThm
appThm
1671
remove
refl
appThm
sym
nil
91
ref
681
ref
1659
ref
18
ref
693
ref
692
ref
1662
ref
appTerm
appTerm
appTerm
1662
remove
appTerm
absTerm
1674
def
appTerm
nil
cons
1675
def
cons
1676
def
1673
remove
cons
nil
cons
cons
1677
def
123
ref
subst
1677
remove
203
ref
subst
315
ref
766
ref
nil
1659
ref
1649
ref
cons
nil
cons
nil
cons
cons
1674
ref
1660
remove
appTerm
1678
def
betaConv
nil
1676
remove
94
ref
1678
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
744
ref
737
ref
1674
remove
nil
cons
cons
1562
ref
1667
remove
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
1679
def
subst
appThm
nil
1659
remove
690
ref
cons
nil
cons
nil
cons
cons
1679
remove
subst
appThm
nil
26
remove
1568
ref
cons
25
remove
1651
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
57
ref
36
remove
appTerm
1680
def
betaConv
59
ref
35
remove
appTerm
1681
def
betaConv
1510
remove
1515
remove
165
ref
subst
proveHyp
nil
91
ref
1511
remove
cons
94
ref
1681
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
241
ref
59
remove
nil
cons
cons
44
ref
1362
remove
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
58
remove
nil
cons
cons
94
ref
1680
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
244
ref
241
ref
57
remove
nil
cons
cons
44
ref
1360
remove
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
trans
appThm
1650
ref
appThm
sym
nil
91
ref
18
ref
1651
ref
appTerm
702
ref
appTerm
1682
def
nil
cons
1683
def
cons
1656
ref
cons
nil
cons
cons
1684
def
123
ref
subst
1684
remove
203
ref
subst
692
ref
refl
1685
def
1682
remove
assume
appThm
nil
91
ref
686
ref
692
ref
1651
remove
appTerm
appTerm
1563
ref
appTerm
nil
cons
cons
1656
remove
cons
nil
cons
cons
173
ref
subst
proveHyp
315
ref
687
remove
nil
738
ref
1649
remove
cons
nil
cons
nil
cons
cons
747
ref
subst
appThm
nil
738
remove
690
ref
cons
nil
cons
nil
cons
cons
747
remove
subst
1686
def
appThm
appThm
1650
remove
appThm
nil
136
ref
1655
ref
cons
nil
cons
nil
cons
cons
nil
136
ref
711
remove
139
ref
appTerm
1687
def
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
136
ref
1687
remove
absTerm
1688
def
139
ref
appTerm
1689
def
betaConv
259
remove
nil
91
ref
260
ref
1688
ref
appTerm
nil
cons
cons
94
ref
1689
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
ref
251
ref
1688
remove
nil
cons
cons
717
ref
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
1690
def
subst
trans
sym
142
ref
eqMp
eqMp
eqMp
nil
149
ref
1683
remove
cons
151
ref
1655
ref
cons
nil
cons
1691
def
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
149
ref
1675
remove
cons
151
ref
1672
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
proveHyp
eqMp
eqMp
nil
149
ref
1654
ref
cons
1691
remove
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
nil
91
ref
12
ref
1653
ref
appTerm
1644
ref
appTerm
nil
cons
cons
94
ref
12
ref
1644
ref
appTerm
1653
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
203
ref
subst
proveHyp
nil
91
ref
1655
ref
cons
94
ref
1654
ref
cons
nil
cons
cons
nil
cons
cons
1692
def
123
ref
subst
1692
remove
203
ref
subst
1685
ref
56
remove
refl
1693
def
1555
ref
1644
remove
assume
appThm
appThm
appThm
eqMp
nil
149
ref
1655
remove
cons
151
ref
1654
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
681
ref
1648
remove
appTerm
thm
nil
"P"
680
ref
var
"p"
679
remove
var
1694
def
12
ref
24
ref
1694
ref
varTerm
1695
def
1641
ref
appTerm
1696
def
appTerm
681
ref
683
ref
12
ref
1695
ref
689
ref
appTerm
1697
def
appTerm
1695
ref
1640
remove
appTerm
appTerm
absTerm
1698
def
appTerm
1699
def
appTerm
1700
def
appTerm
681
remove
683
ref
1697
ref
absTerm
1701
def
appTerm
1702
def
appTerm
1703
def
absTerm
1704
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
685
remove
cons
nil
cons
215
remove
cons
233
remove
subst
subst
1694
remove
nil
136
ref
1703
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
ref
subst
nil
91
ref
1700
remove
nil
cons
1705
def
cons
94
ref
1702
remove
nil
cons
1706
def
cons
nil
cons
cons
nil
cons
cons
1707
def
123
ref
subst
1707
remove
203
ref
subst
nil
149
ref
1696
ref
nil
cons
1708
def
cons
151
ref
1699
remove
nil
cons
1709
def
cons
nil
cons
cons
nil
cons
cons
1710
def
165
ref
subst
1710
remove
385
ref
subst
nil
737
ref
1701
ref
nil
cons
cons
nil
cons
nil
cons
cons
746
remove
subst
683
ref
nil
136
ref
1697
ref
nil
cons
1711
def
cons
nil
cons
nil
cons
cons
1712
def
143
ref
subst
104
ref
69
ref
24
ref
96
ref
appTerm
1695
ref
692
ref
70
ref
appTerm
1713
def
appTerm
1714
def
appTerm
1715
def
absTerm
1716
def
appTerm
1717
def
betaConv
663
remove
666
remove
385
ref
subst
proveHyp
nil
149
ref
105
remove
nil
cons
1718
def
cons
151
ref
106
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
proveHyp
nil
91
ref
1718
remove
cons
94
ref
1717
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
214
remove
204
remove
104
remove
nil
cons
cons
620
remove
1716
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
nil
91
ref
12
ref
24
ref
1716
ref
66
remove
appTerm
1719
def
appTerm
13
ref
69
ref
12
ref
1716
ref
70
ref
appTerm
1720
def
appTerm
1716
ref
71
ref
appTerm
1721
def
appTerm
absTerm
appTerm
appTerm
appTerm
13
ref
3
ref
103
ref
1716
remove
19
ref
appTerm
1722
def
appTerm
absTerm
appTerm
appTerm
nil
cons
cons
94
ref
1711
ref
cons
nil
cons
1723
def
cons
nil
cons
cons
173
ref
subst
proveHyp
315
ref
315
ref
361
ref
1719
remove
betaConv
361
ref
nil
136
ref
668
remove
cons
nil
cons
nil
cons
cons
143
ref
subst
673
remove
eqMp
appThm
1695
ref
refl
1724
def
686
ref
699
ref
appTerm
1641
ref
appTerm
assume
sym
686
ref
1641
remove
appTerm
699
remove
appTerm
assume
sym
deductAntisym
700
remove
eqMp
appThm
nil
136
ref
1708
remove
cons
nil
cons
nil
cons
cons
143
ref
subst
1696
remove
assume
eqMp
trans
appThm
894
ref
916
ref
subst
trans
trans
appThm
316
ref
69
ref
315
ref
1720
remove
betaConv
appThm
1721
remove
betaConv
appThm
absThm
appThm
appThm
nil
136
ref
13
ref
69
ref
12
ref
1715
ref
appTerm
24
ref
97
remove
appTerm
1695
ref
692
ref
71
remove
appTerm
1725
def
appTerm
1726
def
appTerm
1727
def
appTerm
1728
def
absTerm
1729
def
appTerm
nil
cons
1730
def
cons
nil
cons
nil
cons
cons
916
ref
subst
trans
appThm
316
ref
3
ref
103
ref
refl
1722
remove
betaConv
appThm
absThm
appThm
appThm
appThm
1697
remove
refl
1731
def
appThm
sym
nil
241
ref
1729
ref
nil
cons
cons
1732
def
nil
cons
nil
cons
cons
246
remove
subst
69
ref
nil
136
ref
1728
remove
nil
cons
cons
nil
cons
nil
cons
cons
143
remove
subst
1733
def
nil
91
ref
1715
remove
nil
cons
1734
def
cons
94
ref
1727
remove
nil
cons
1735
def
cons
nil
cons
cons
nil
cons
cons
1736
def
123
ref
subst
1736
remove
203
ref
subst
nil
149
ref
1615
remove
cons
151
ref
1714
remove
nil
cons
1737
def
cons
nil
cons
cons
nil
cons
cons
1738
def
165
ref
subst
1738
remove
385
remove
subst
1617
remove
173
ref
subst
1670
remove
eqMp
nil
91
ref
1616
remove
cons
94
ref
1726
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
203
ref
subst
proveHyp
686
remove
1725
ref
appTerm
1739
def
refl
nil
683
remove
1713
ref
nil
cons
cons
nil
cons
nil
cons
cons
1740
def
698
remove
subst
appThm
sym
1685
remove
1693
remove
18
ref
693
remove
1713
ref
appTerm
1741
def
appTerm
70
ref
appTerm
assume
sym
18
remove
70
ref
appTerm
1741
remove
appTerm
assume
sym
deductAntisym
sym
nil
752
ref
284
remove
cons
nil
cons
nil
cons
cons
758
remove
subst
sym
96
remove
assume
eqMp
eqMp
appThm
appThm
eqMp
27
ref
"_1919"
678
remove
var
1742
def
1695
ref
1742
remove
varTerm
appTerm
absTerm
1743
def
1725
remove
appTerm
1744
def
appTerm
refl
1743
remove
1639
remove
1713
remove
appTerm
1745
def
appTerm
betaConv
appThm
153
remove
1744
remove
betaConv
appThm
1695
ref
1745
ref
appTerm
1746
def
refl
appThm
trans
1701
remove
refl
1739
remove
1745
remove
appTerm
assume
appThm
eqMp
sym
nil
91
ref
1737
remove
cons
94
ref
1746
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
1740
remove
1698
ref
689
remove
appTerm
1747
def
betaConv
nil
91
ref
1709
remove
cons
94
ref
1747
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
744
remove
737
remove
1698
remove
nil
cons
cons
1562
remove
690
remove
cons
nil
cons
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
proveHyp
eqMp
proveHyp
proveHyp
eqMp
nil
149
ref
1734
remove
cons
151
ref
1735
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
315
ref
315
ref
316
remove
69
remove
1733
remove
1729
remove
70
remove
appTerm
1748
def
betaConv
nil
91
ref
1730
remove
cons
94
ref
1748
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
244
ref
1732
remove
433
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
eqMp
absThm
appThm
894
remove
245
remove
136
ref
27
remove
219
remove
225
remove
139
ref
absTerm
appTerm
appTerm
139
ref
appTerm
absTerm
1749
def
139
remove
appTerm
1750
def
betaConv
nil
260
remove
1749
ref
appTerm
1751
def
axiom
nil
91
ref
1751
remove
nil
cons
cons
94
ref
1750
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
proveHyp
253
remove
251
remove
1749
remove
nil
cons
cons
717
remove
cons
nil
cons
cons
270
ref
subst
eqMp
eqMp
subst
subst
trans
appThm
13
remove
3
remove
103
remove
24
ref
102
remove
appTerm
1695
ref
692
remove
19
remove
appTerm
appTerm
appTerm
appTerm
absTerm
1752
def
appTerm
1753
def
refl
appThm
nil
136
remove
1753
remove
nil
cons
1754
def
cons
nil
cons
nil
cons
cons
1133
ref
subst
trans
appThm
1731
ref
appThm
sym
nil
91
ref
1754
ref
cons
1755
def
1723
ref
cons
nil
cons
cons
1756
def
123
remove
subst
1756
remove
203
remove
subst
1752
ref
702
ref
appTerm
1757
def
betaConv
nil
1755
remove
94
remove
1757
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
173
ref
subst
244
remove
241
remove
1752
remove
nil
cons
cons
44
remove
1568
ref
cons
nil
cons
1758
def
cons
nil
cons
cons
270
remove
subst
eqMp
eqMp
nil
91
remove
12
remove
1565
ref
appTerm
24
remove
1565
remove
appTerm
1695
remove
1563
remove
appTerm
appTerm
appTerm
nil
cons
cons
1723
remove
cons
nil
cons
cons
173
remove
subst
proveHyp
315
ref
315
remove
nil
752
remove
1568
remove
cons
nil
cons
nil
cons
cons
759
remove
subst
766
remove
1555
remove
1686
ref
appThm
appThm
702
remove
refl
appThm
nil
1758
remove
nil
cons
cons
1668
remove
subst
trans
trans
1759
def
appThm
361
remove
1759
remove
appThm
1724
remove
1686
remove
appThm
appThm
1712
ref
916
remove
subst
trans
appThm
1712
ref
1133
remove
subst
trans
appThm
1731
remove
appThm
1712
remove
1690
remove
subst
trans
sym
142
remove
eqMp
eqMp
eqMp
nil
149
ref
1754
remove
cons
151
ref
1711
remove
cons
nil
cons
cons
nil
cons
cons
165
ref
subst
deductAntisym
eqMp
eqMp
proveHyp
eqMp
eqMp
eqMp
absThm
eqMp
proveHyp
proveHyp
eqMp
nil
149
remove
1705
remove
cons
151
remove
1706
remove
cons
nil
cons
cons
nil
cons
cons
165
remove
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
0
remove
1
remove
680
remove
5
remove
cons
opType
constTerm
1704
remove
appTerm
thm