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