6
version
"Set.finite"
"a"
"Set.set"
typeOp
"A"
varType
0
def
nil
cons
1
def
opType
2
def
var
3
def
"Data.Bool.!"
const
4
def
"->"
typeOp
5
def
5
ref
5
ref
2
ref
"bool"
typeOp
nil
opType
6
def
nil
cons
7
def
cons
opType
8
def
7
ref
cons
opType
9
def
7
ref
cons
opType
constTerm
10
def
"FINITE'"
8
ref
var
11
def
"Data.Bool.==>"
const
5
ref
6
ref
5
ref
6
ref
7
ref
cons
opType
12
def
nil
cons
cons
opType
13
def
constTerm
14
def
4
ref
9
ref
constTerm
15
def
3
ref
14
ref
"Data.Bool.\\/"
const
13
ref
constTerm
16
def
"="
const
17
def
5
ref
2
ref
8
ref
nil
cons
18
def
cons
opType
constTerm
19
def
3
ref
varTerm
20
def
appTerm
21
def
"Set.{}"
const
2
ref
constTerm
22
def
appTerm
23
def
appTerm
24
def
"Data.Bool.?"
const
25
def
5
ref
5
ref
0
ref
7
ref
cons
opType
26
def
7
ref
cons
opType
27
def
constTerm
28
def
"x"
0
ref
var
29
def
25
remove
9
ref
constTerm
30
def
"s"
2
ref
var
31
def
"Data.Bool./\\"
const
13
ref
constTerm
32
def
21
remove
"Set.insert"
const
5
ref
0
ref
5
ref
2
ref
2
ref
nil
cons
33
def
cons
opType
nil
cons
cons
opType
constTerm
34
def
29
ref
varTerm
35
def
appTerm
36
def
31
ref
varTerm
37
def
appTerm
38
def
appTerm
39
def
appTerm
40
def
11
ref
varTerm
41
def
37
ref
appTerm
42
def
appTerm
43
def
absTerm
44
def
appTerm
45
def
absTerm
46
def
appTerm
47
def
appTerm
48
def
appTerm
41
ref
20
ref
appTerm
49
def
appTerm
50
def
absTerm
51
def
appTerm
52
def
appTerm
53
def
49
ref
appTerm
54
def
absTerm
55
def
appTerm
56
def
absTerm
57
def
defineConst
58
def
pop
59
def
pop
58
remove
nil
"p"
6
ref
var
60
def
17
ref
5
ref
8
ref
9
ref
nil
cons
cons
opType
constTerm
61
def
59
remove
8
ref
constTerm
62
def
appTerm
57
ref
appTerm
nil
cons
cons
"q"
6
ref
var
63
def
32
ref
32
ref
62
ref
22
ref
appTerm
64
def
appTerm
4
ref
27
ref
constTerm
65
def
29
ref
15
ref
31
ref
14
ref
62
ref
37
ref
appTerm
66
def
appTerm
62
ref
38
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
67
def
appTerm
68
def
appTerm
32
ref
10
ref
11
ref
14
ref
32
ref
41
ref
22
ref
appTerm
appTerm
65
ref
29
ref
15
ref
31
ref
14
ref
42
ref
appTerm
41
ref
38
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
69
def
15
ref
3
ref
14
ref
62
ref
20
ref
appTerm
70
def
appTerm
71
def
49
ref
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
72
def
appTerm
15
ref
3
ref
17
ref
13
ref
constTerm
73
def
70
remove
appTerm
24
ref
28
ref
29
ref
30
ref
31
ref
40
ref
66
ref
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
absTerm
appTerm
74
def
appTerm
75
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
73
ref
14
ref
60
ref
varTerm
76
def
appTerm
77
def
63
ref
varTerm
78
def
appTerm
79
def
appTerm
refl
60
ref
63
ref
73
ref
32
ref
76
ref
appTerm
80
def
78
ref
appTerm
81
def
appTerm
82
def
76
ref
appTerm
absTerm
83
def
absTerm
84
def
76
ref
appTerm
betaConv
78
ref
refl
85
def
appThm
83
remove
78
ref
appTerm
betaConv
trans
appThm
nil
17
ref
5
ref
13
ref
5
ref
13
ref
7
ref
cons
opType
86
def
nil
cons
cons
opType
constTerm
87
def
14
ref
appTerm
84
remove
appTerm
axiom
76
ref
refl
88
def
appThm
85
ref
appThm
eqMp
89
def
sym
90
def
82
remove
refl
63
ref
17
ref
5
ref
86
ref
5
ref
86
remove
7
ref
cons
opType
nil
cons
cons
opType
constTerm
91
def
"f"
13
remove
var
92
def
92
ref
varTerm
93
def
76
ref
appTerm
78
ref
appTerm
absTerm
94
def
appTerm
92
ref
93
ref
"Data.Bool.T"
const
6
ref
constTerm
95
def
appTerm
95
ref
appTerm
absTerm
96
def
appTerm
absTerm
97
def
78
ref
appTerm
betaConv
appThm
17
ref
5
ref
12
ref
5
ref
12
ref
7
ref
cons
opType
98
def
nil
cons
cons
opType
constTerm
99
def
80
remove
appTerm
refl
60
ref
97
remove
absTerm
100
def
76
ref
appTerm
betaConv
appThm
nil
87
ref
32
ref
appTerm
100
ref
appTerm
axiom
101
def
88
remove
appThm
eqMp
85
ref
appThm
eqMp
102
def
sym
92
ref
93
ref
refl
nil
"t"
6
ref
var
103
def
76
ref
nil
cons
104
def
cons
nil
cons
nil
cons
cons
73
ref
103
ref
varTerm
105
def
appTerm
95
ref
appTerm
assume
sym
nil
95
ref
axiom
106
def
eqMp
105
ref
assume
106
ref
deductAntisym
deductAntisym
107
def
subst
76
ref
assume
108
def
eqMp
appThm
nil
103
ref
78
ref
nil
cons
109
def
cons
nil
cons
nil
cons
cons
107
ref
subst
78
ref
assume
110
def
eqMp
appThm
absThm
eqMp
111
def
nil
"P"
6
ref
var
112
def
104
ref
cons
113
def
"Q"
6
ref
var
114
def
109
ref
cons
nil
cons
115
def
cons
nil
cons
cons
73
ref
refl
116
def
92
ref
93
remove
112
ref
varTerm
117
def
appTerm
118
def
114
ref
varTerm
119
def
appTerm
absTerm
120
def
60
ref
63
ref
76
ref
absTerm
absTerm
121
def
appTerm
betaConv
121
ref
117
ref
appTerm
betaConv
119
ref
refl
122
def
appThm
63
ref
117
ref
absTerm
119
ref
appTerm
betaConv
trans
trans
appThm
96
ref
121
ref
appTerm
betaConv
121
ref
95
ref
appTerm
betaConv
95
ref
refl
123
def
appThm
63
ref
95
ref
absTerm
95
ref
appTerm
betaConv
trans
trans
appThm
73
ref
32
ref
117
ref
appTerm
124
def
119
ref
appTerm
125
def
appTerm
refl
63
ref
91
remove
92
remove
118
remove
78
ref
appTerm
absTerm
appTerm
96
ref
appTerm
absTerm
119
ref
appTerm
betaConv
appThm
99
ref
124
remove
appTerm
refl
100
remove
117
ref
appTerm
betaConv
appThm
101
remove
117
ref
refl
126
def
appThm
eqMp
122
ref
appThm
eqMp
125
remove
assume
eqMp
127
def
121
remove
refl
appThm
eqMp
sym
106
ref
eqMp
128
def
subst
deductAntisym
eqMp
89
remove
79
ref
assume
eqMp
sym
108
ref
eqMp
116
ref
94
remove
60
ref
63
ref
78
ref
absTerm
129
def
absTerm
130
def
appTerm
betaConv
130
ref
76
ref
appTerm
betaConv
85
ref
appThm
129
ref
78
ref
appTerm
betaConv
trans
trans
appThm
96
remove
130
ref
appTerm
betaConv
130
ref
95
ref
appTerm
betaConv
123
remove
appThm
129
ref
95
ref
appTerm
betaConv
trans
trans
131
def
appThm
102
remove
81
remove
assume
eqMp
130
ref
refl
132
def
appThm
eqMp
sym
106
ref
eqMp
133
def
proveHyp
134
def
deductAntisym
135
def
subst
proveHyp
nil
"FINITE"
8
ref
var
136
def
62
ref
nil
cons
cons
nil
cons
nil
cons
cons
nil
60
ref
61
remove
136
ref
varTerm
137
def
appTerm
57
ref
appTerm
138
def
nil
cons
139
def
cons
63
ref
32
ref
32
ref
137
ref
22
ref
appTerm
140
def
appTerm
65
ref
29
ref
15
ref
31
ref
14
ref
137
ref
37
ref
appTerm
141
def
appTerm
142
def
137
ref
38
ref
appTerm
143
def
appTerm
144
def
absTerm
145
def
appTerm
146
def
absTerm
147
def
appTerm
148
def
appTerm
149
def
appTerm
32
ref
10
ref
11
ref
69
remove
15
ref
3
ref
14
ref
137
ref
20
ref
appTerm
150
def
appTerm
151
def
49
ref
appTerm
152
def
absTerm
153
def
appTerm
154
def
appTerm
absTerm
appTerm
155
def
appTerm
15
ref
3
ref
73
ref
150
ref
appTerm
156
def
24
ref
28
ref
29
ref
30
ref
31
ref
40
ref
141
ref
appTerm
157
def
absTerm
158
def
appTerm
159
def
absTerm
160
def
appTerm
161
def
appTerm
162
def
appTerm
163
def
absTerm
164
def
appTerm
165
def
appTerm
166
def
appTerm
nil
cons
167
def
cons
nil
cons
cons
nil
cons
cons
168
def
90
ref
subst
168
remove
133
remove
111
remove
deductAntisym
169
def
subst
nil
"P"
9
remove
var
170
def
136
ref
10
ref
11
ref
14
ref
154
ref
appTerm
15
ref
3
ref
14
ref
162
ref
appTerm
171
def
48
ref
appTerm
172
def
absTerm
173
def
appTerm
174
def
appTerm
175
def
absTerm
176
def
appTerm
177
def
absTerm
178
def
nil
cons
cons
179
def
nil
cons
nil
cons
cons
"A"
18
remove
cons
nil
cons
180
def
nil
nil
cons
181
def
cons
73
ref
65
ref
"P"
26
ref
var
182
def
varTerm
183
def
appTerm
184
def
appTerm
refl
"p"
26
ref
var
185
def
17
ref
5
ref
26
ref
27
ref
nil
cons
cons
opType
constTerm
185
ref
varTerm
186
def
appTerm
29
ref
95
remove
absTerm
187
def
appTerm
absTerm
188
def
183
ref
appTerm
betaConv
189
def
appThm
nil
17
remove
5
ref
27
ref
5
remove
27
ref
7
ref
cons
opType
190
def
nil
cons
cons
opType
constTerm
191
def
65
ref
appTerm
188
remove
appTerm
axiom
183
ref
refl
192
def
appThm
193
def
eqMp
sym
194
def
subst
195
def
subst
136
ref
nil
103
ref
177
remove
nil
cons
196
def
cons
nil
cons
nil
cons
cons
107
ref
subst
nil
170
ref
176
ref
nil
cons
cons
197
def
nil
cons
nil
cons
cons
195
ref
subst
11
ref
nil
103
ref
175
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
nil
60
ref
154
ref
nil
cons
198
def
cons
199
def
63
ref
174
remove
nil
cons
200
def
cons
nil
cons
cons
nil
cons
cons
201
def
90
ref
subst
201
ref
169
ref
subst
nil
"P"
8
ref
var
202
def
173
ref
nil
cons
cons
203
def
nil
cons
nil
cons
cons
"A"
33
remove
cons
nil
cons
204
def
181
ref
cons
205
def
194
ref
subst
206
def
subst
3
ref
nil
103
ref
172
remove
nil
cons
207
def
cons
nil
cons
nil
cons
cons
107
ref
subst
60
ref
77
ref
76
ref
appTerm
208
def
absTerm
209
def
23
ref
appTerm
210
def
betaConv
nil
"P"
12
ref
var
211
def
209
ref
nil
cons
cons
212
def
nil
cons
nil
cons
cons
"A"
7
remove
cons
nil
cons
213
def
181
remove
cons
194
ref
subst
214
def
subst
60
ref
nil
103
ref
208
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
nil
60
ref
104
ref
cons
215
def
63
ref
104
ref
cons
nil
cons
216
def
cons
nil
cons
cons
217
def
90
ref
subst
217
remove
169
ref
subst
108
remove
eqMp
nil
113
ref
114
ref
104
remove
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
218
def
nil
60
ref
4
ref
98
remove
constTerm
219
def
209
ref
appTerm
nil
cons
cons
220
def
63
ref
210
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
213
ref
212
ref
"x"
6
ref
var
221
def
23
ref
nil
cons
222
def
cons
nil
cons
cons
nil
cons
cons
nil
60
ref
184
ref
nil
cons
223
def
cons
63
ref
183
ref
35
ref
appTerm
224
def
nil
cons
225
def
cons
nil
cons
cons
nil
cons
cons
226
def
90
ref
subst
226
remove
169
ref
subst
73
ref
224
ref
appTerm
refl
187
remove
35
ref
appTerm
betaConv
appThm
189
remove
193
remove
184
remove
assume
eqMp
eqMp
35
ref
refl
appThm
eqMp
sym
106
ref
eqMp
eqMp
nil
112
ref
223
remove
cons
114
ref
225
ref
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
227
def
subst
eqMp
eqMp
nil
60
ref
14
ref
23
ref
appTerm
228
def
23
ref
appTerm
229
def
nil
cons
cons
63
ref
14
ref
161
ref
appTerm
230
def
47
ref
appTerm
231
def
nil
cons
cons
nil
cons
232
def
cons
nil
cons
cons
169
ref
subst
proveHyp
nil
182
ref
29
ref
14
ref
159
ref
appTerm
233
def
45
remove
appTerm
234
def
absTerm
235
def
nil
cons
cons
nil
cons
nil
cons
cons
194
ref
subst
29
ref
nil
103
ref
234
remove
nil
cons
236
def
cons
nil
cons
nil
cons
cons
107
ref
subst
nil
202
ref
31
ref
14
ref
157
ref
appTerm
237
def
43
remove
appTerm
238
def
absTerm
239
def
nil
cons
cons
nil
cons
nil
cons
cons
206
ref
subst
31
ref
nil
103
ref
238
remove
nil
cons
240
def
cons
nil
cons
nil
cons
cons
107
ref
subst
209
remove
39
ref
appTerm
241
def
betaConv
218
remove
nil
220
remove
63
ref
241
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
213
ref
212
remove
221
ref
39
ref
nil
cons
242
def
cons
nil
cons
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
nil
60
ref
14
ref
39
ref
appTerm
39
remove
appTerm
243
def
nil
cons
cons
63
ref
142
remove
42
ref
appTerm
244
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
169
ref
subst
proveHyp
nil
3
ref
37
ref
nil
cons
245
def
cons
nil
cons
nil
cons
cons
nil
103
ref
152
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
246
def
153
ref
20
ref
appTerm
247
def
betaConv
nil
199
remove
63
ref
247
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
204
ref
202
ref
153
remove
nil
cons
cons
248
def
"x"
2
ref
var
249
def
20
ref
nil
cons
cons
nil
cons
250
def
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
eqMp
subst
sym
106
ref
eqMp
eqMp
nil
60
ref
32
ref
243
remove
appTerm
244
remove
appTerm
nil
cons
cons
63
ref
240
remove
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
nil
"q2"
6
ref
var
251
def
42
remove
nil
cons
cons
"p2"
6
ref
var
252
def
242
ref
cons
"q1"
6
ref
var
253
def
141
ref
nil
cons
254
def
cons
"p1"
6
ref
var
255
def
242
ref
cons
nil
cons
cons
cons
cons
nil
cons
cons
251
ref
14
ref
32
ref
14
ref
255
ref
varTerm
256
def
appTerm
252
ref
varTerm
257
def
appTerm
appTerm
14
ref
253
ref
varTerm
258
def
appTerm
251
ref
varTerm
259
def
appTerm
appTerm
appTerm
260
def
14
ref
32
ref
256
ref
appTerm
258
ref
appTerm
appTerm
32
ref
257
ref
appTerm
259
ref
appTerm
appTerm
appTerm
absTerm
261
def
259
ref
appTerm
262
def
betaConv
253
ref
219
ref
261
ref
appTerm
263
def
absTerm
264
def
258
ref
appTerm
265
def
betaConv
252
ref
219
ref
264
ref
appTerm
266
def
absTerm
267
def
257
ref
appTerm
268
def
betaConv
255
ref
219
ref
267
ref
appTerm
269
def
absTerm
270
def
256
ref
appTerm
271
def
betaConv
nil
219
ref
270
ref
appTerm
272
def
axiom
nil
60
ref
272
remove
nil
cons
cons
63
ref
271
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
213
ref
211
ref
270
remove
nil
cons
cons
221
ref
256
ref
nil
cons
cons
nil
cons
273
def
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
nil
60
ref
269
remove
nil
cons
cons
63
ref
268
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
213
ref
211
ref
267
remove
nil
cons
cons
221
ref
257
ref
nil
cons
cons
nil
cons
274
def
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
nil
60
ref
266
remove
nil
cons
cons
63
ref
265
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
213
ref
211
ref
264
remove
nil
cons
cons
221
ref
258
ref
nil
cons
cons
nil
cons
275
def
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
nil
60
ref
263
remove
nil
cons
cons
63
ref
262
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
213
ref
211
ref
261
remove
nil
cons
cons
221
ref
259
ref
nil
cons
cons
nil
cons
276
def
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
absThm
eqMp
nil
60
ref
15
ref
239
remove
appTerm
nil
cons
cons
63
ref
236
remove
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
14
ref
refl
277
def
15
ref
refl
278
def
31
ref
277
ref
158
ref
37
ref
appTerm
279
def
betaConv
280
def
appThm
44
ref
37
ref
appTerm
betaConv
281
def
appThm
absThm
appThm
appThm
277
ref
30
ref
refl
282
def
31
ref
280
ref
absThm
appThm
appThm
282
remove
31
ref
281
remove
absThm
appThm
appThm
appThm
nil
"p"
8
ref
var
283
def
158
ref
nil
cons
284
def
cons
"q"
8
ref
var
44
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
205
remove
"q"
26
ref
var
285
def
14
ref
65
ref
29
ref
14
ref
186
ref
35
ref
appTerm
286
def
appTerm
287
def
285
ref
varTerm
288
def
35
ref
appTerm
289
def
appTerm
absTerm
appTerm
appTerm
14
ref
28
ref
29
ref
286
remove
absTerm
appTerm
appTerm
28
ref
29
ref
289
remove
absTerm
appTerm
appTerm
appTerm
absTerm
290
def
288
ref
appTerm
291
def
betaConv
185
ref
4
remove
190
remove
constTerm
292
def
290
ref
appTerm
293
def
absTerm
294
def
186
ref
appTerm
295
def
betaConv
nil
292
remove
294
ref
appTerm
296
def
axiom
nil
60
ref
296
remove
nil
cons
cons
63
ref
295
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
"A"
26
ref
nil
cons
cons
nil
cons
297
def
"P"
27
remove
var
298
def
294
remove
nil
cons
cons
"x"
26
remove
var
299
def
186
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
nil
60
ref
293
remove
nil
cons
cons
63
ref
291
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
297
remove
298
remove
290
remove
nil
cons
cons
299
remove
288
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
300
def
subst
subst
eqMp
eqMp
eqMp
absThm
eqMp
nil
60
ref
65
ref
235
remove
appTerm
nil
cons
cons
232
remove
cons
nil
cons
cons
135
ref
subst
proveHyp
277
ref
65
ref
refl
29
ref
277
ref
160
ref
35
ref
appTerm
301
def
betaConv
302
def
appThm
46
ref
35
ref
appTerm
betaConv
303
def
appThm
absThm
appThm
appThm
277
ref
28
ref
refl
304
def
29
ref
302
ref
absThm
appThm
appThm
304
remove
29
ref
303
remove
absThm
appThm
appThm
appThm
nil
185
ref
160
remove
nil
cons
305
def
cons
285
remove
46
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
300
remove
subst
eqMp
eqMp
eqMp
nil
60
ref
32
ref
229
remove
appTerm
231
remove
appTerm
nil
cons
cons
63
ref
207
ref
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
nil
251
ref
47
remove
nil
cons
cons
252
ref
222
ref
cons
253
ref
161
remove
nil
cons
306
def
cons
255
ref
222
ref
cons
nil
cons
cons
cons
cons
nil
cons
cons
251
remove
260
remove
14
ref
16
ref
256
ref
appTerm
258
ref
appTerm
appTerm
16
ref
257
ref
appTerm
259
ref
appTerm
appTerm
appTerm
absTerm
307
def
259
remove
appTerm
308
def
betaConv
253
remove
219
ref
307
ref
appTerm
309
def
absTerm
310
def
258
remove
appTerm
311
def
betaConv
252
remove
219
ref
310
ref
appTerm
312
def
absTerm
313
def
257
remove
appTerm
314
def
betaConv
255
remove
219
ref
313
ref
appTerm
315
def
absTerm
316
def
256
remove
appTerm
317
def
betaConv
nil
219
ref
316
ref
appTerm
318
def
axiom
nil
60
ref
318
remove
nil
cons
cons
63
ref
317
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
213
ref
211
ref
316
remove
nil
cons
cons
273
remove
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
nil
60
ref
315
remove
nil
cons
cons
63
ref
314
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
213
ref
211
ref
313
remove
nil
cons
cons
274
remove
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
nil
60
ref
312
remove
nil
cons
cons
63
ref
311
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
213
ref
211
ref
310
remove
nil
cons
cons
275
remove
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
nil
60
ref
309
remove
nil
cons
cons
63
ref
308
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
213
ref
211
ref
307
remove
nil
cons
cons
276
remove
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
absThm
eqMp
eqMp
nil
112
ref
198
ref
cons
114
ref
200
ref
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
32
ref
refl
nil
60
ref
140
ref
nil
cons
319
def
cons
63
ref
15
ref
3
ref
228
remove
150
ref
appTerm
320
def
absTerm
321
def
appTerm
322
def
nil
cons
323
def
cons
nil
cons
cons
nil
cons
cons
324
def
277
ref
73
ref
76
ref
appTerm
78
ref
appTerm
325
def
assume
326
def
appThm
85
remove
appThm
sym
nil
60
ref
109
ref
cons
327
def
63
ref
109
ref
cons
nil
cons
cons
nil
cons
cons
328
def
90
ref
subst
328
remove
169
ref
subst
110
remove
eqMp
nil
112
ref
109
remove
cons
115
remove
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
329
def
eqMp
330
def
nil
60
ref
79
remove
nil
cons
331
def
cons
332
def
63
ref
14
ref
78
ref
appTerm
333
def
76
remove
appTerm
nil
cons
334
def
cons
nil
cons
cons
nil
cons
cons
169
ref
subst
proveHyp
333
ref
refl
326
remove
appThm
sym
329
remove
eqMp
eqMp
nil
327
ref
216
remove
cons
nil
cons
cons
135
ref
subst
nil
112
ref
331
ref
cons
335
def
114
ref
334
remove
cons
nil
cons
cons
nil
cons
cons
336
def
116
remove
120
remove
130
ref
appTerm
betaConv
130
remove
117
ref
appTerm
betaConv
122
ref
appThm
129
remove
119
ref
appTerm
betaConv
trans
trans
appThm
131
remove
appThm
127
remove
132
remove
appThm
eqMp
sym
106
remove
eqMp
337
def
subst
eqMp
135
ref
336
remove
128
ref
subst
eqMp
deductAntisym
deductAntisym
338
def
subst
324
ref
90
ref
subst
324
remove
169
ref
subst
nil
202
ref
321
ref
nil
cons
cons
339
def
nil
cons
nil
cons
cons
206
ref
subst
340
def
3
ref
nil
103
ref
320
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
341
def
nil
60
ref
222
ref
cons
342
def
63
ref
150
ref
nil
cons
343
def
cons
nil
cons
344
def
cons
nil
cons
cons
345
def
90
ref
subst
346
def
345
ref
169
ref
subst
347
def
137
ref
refl
348
def
23
remove
assume
appThm
sym
140
ref
assume
eqMp
eqMp
nil
112
ref
222
remove
cons
349
def
114
ref
343
ref
cons
nil
cons
350
def
cons
nil
cons
cons
128
ref
subst
351
def
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
112
ref
319
ref
cons
114
ref
323
ref
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
nil
60
ref
14
ref
140
ref
appTerm
322
ref
appTerm
nil
cons
cons
63
ref
14
ref
322
ref
appTerm
140
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
169
ref
subst
proveHyp
nil
60
ref
323
ref
cons
352
def
63
ref
319
ref
cons
nil
cons
353
def
cons
nil
cons
cons
354
def
90
ref
subst
354
remove
169
ref
subst
22
ref
refl
nil
60
ref
19
ref
22
ref
appTerm
22
ref
appTerm
nil
cons
cons
353
remove
cons
nil
cons
cons
135
ref
subst
proveHyp
321
ref
22
ref
appTerm
355
def
betaConv
nil
352
ref
63
ref
355
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
204
ref
339
ref
249
ref
22
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
112
ref
323
remove
cons
356
def
114
ref
319
remove
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
eqMp
appThm
nil
60
ref
148
ref
nil
cons
357
def
cons
358
def
63
ref
15
ref
3
ref
65
ref
29
ref
15
ref
31
ref
237
remove
150
ref
appTerm
359
def
absTerm
360
def
appTerm
361
def
absTerm
362
def
appTerm
363
def
absTerm
364
def
appTerm
365
def
nil
cons
366
def
cons
nil
cons
cons
nil
cons
cons
367
def
338
ref
subst
367
ref
90
ref
subst
367
remove
169
ref
subst
nil
202
ref
364
ref
nil
cons
cons
368
def
nil
cons
nil
cons
cons
206
ref
subst
3
ref
nil
103
ref
363
ref
nil
cons
369
def
cons
nil
cons
nil
cons
cons
107
ref
subst
nil
182
ref
362
ref
nil
cons
cons
370
def
nil
cons
nil
cons
cons
194
ref
subst
371
def
29
ref
nil
103
ref
361
remove
nil
cons
372
def
cons
nil
cons
nil
cons
cons
107
ref
subst
373
def
nil
202
ref
360
ref
nil
cons
cons
374
def
nil
cons
nil
cons
cons
206
ref
subst
375
def
31
ref
nil
103
ref
359
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
376
def
nil
60
ref
157
ref
nil
cons
377
def
cons
378
def
344
ref
cons
nil
cons
cons
379
def
90
ref
subst
380
def
379
ref
169
ref
subst
381
def
348
remove
nil
112
ref
242
remove
cons
114
ref
254
ref
cons
nil
cons
cons
nil
cons
cons
382
def
128
ref
subst
appThm
sym
382
remove
337
ref
subst
nil
60
ref
254
ref
cons
63
ref
143
ref
nil
cons
383
def
cons
nil
cons
384
def
cons
nil
cons
cons
385
def
135
ref
subst
proveHyp
145
ref
37
ref
appTerm
386
def
betaConv
147
ref
35
ref
appTerm
387
def
betaConv
nil
358
remove
63
ref
387
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
"A"
1
remove
cons
nil
cons
388
def
182
ref
147
remove
nil
cons
cons
389
def
29
ref
35
ref
nil
cons
cons
nil
cons
390
def
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
nil
60
ref
146
remove
nil
cons
391
def
cons
63
ref
386
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
204
ref
202
ref
145
remove
nil
cons
cons
392
def
249
ref
245
remove
cons
nil
cons
393
def
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
eqMp
eqMp
eqMp
nil
112
ref
377
remove
cons
394
def
350
ref
cons
nil
cons
cons
128
ref
subst
395
def
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
112
ref
357
ref
cons
114
ref
366
ref
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
nil
60
ref
14
ref
148
ref
appTerm
365
ref
appTerm
nil
cons
cons
63
ref
14
ref
365
remove
appTerm
148
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
169
ref
subst
proveHyp
nil
60
ref
366
ref
cons
396
def
63
ref
357
ref
cons
nil
cons
cons
nil
cons
cons
397
def
90
ref
subst
397
remove
169
ref
subst
nil
389
remove
nil
cons
nil
cons
cons
194
ref
subst
29
ref
nil
103
ref
391
remove
cons
nil
cons
nil
cons
cons
107
ref
subst
nil
392
remove
nil
cons
nil
cons
cons
206
ref
subst
31
ref
nil
103
ref
144
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
385
ref
90
ref
subst
385
remove
169
ref
subst
38
ref
refl
nil
60
ref
19
remove
38
ref
appTerm
398
def
38
ref
appTerm
399
def
nil
cons
cons
63
ref
254
ref
cons
nil
cons
cons
nil
cons
cons
169
ref
subst
proveHyp
141
ref
assume
eqMp
nil
60
ref
32
ref
399
remove
appTerm
141
remove
appTerm
nil
cons
cons
384
remove
cons
nil
cons
cons
135
ref
subst
proveHyp
"s'"
2
ref
var
400
def
14
ref
32
ref
398
ref
36
remove
400
ref
varTerm
401
def
appTerm
appTerm
appTerm
137
ref
401
ref
appTerm
402
def
appTerm
appTerm
143
ref
appTerm
absTerm
403
def
37
ref
appTerm
404
def
betaConv
"x'"
0
remove
var
405
def
15
ref
400
remove
14
ref
32
ref
398
remove
34
remove
405
remove
varTerm
appTerm
401
remove
appTerm
appTerm
appTerm
402
remove
appTerm
appTerm
143
remove
appTerm
absTerm
appTerm
absTerm
406
def
35
ref
appTerm
407
def
betaConv
364
remove
38
ref
appTerm
408
def
betaConv
nil
396
remove
63
ref
408
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
204
ref
368
remove
249
ref
38
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
nil
60
ref
65
ref
406
ref
appTerm
nil
cons
cons
63
ref
407
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
388
ref
182
ref
406
remove
nil
cons
cons
390
ref
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
nil
60
ref
15
ref
403
ref
appTerm
nil
cons
cons
63
ref
404
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
204
ref
202
ref
403
remove
nil
cons
cons
393
ref
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
112
ref
254
remove
cons
114
ref
383
remove
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
112
ref
366
remove
cons
114
ref
357
remove
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
eqMp
278
ref
3
ref
nil
60
ref
369
ref
cons
409
def
63
ref
230
ref
150
ref
appTerm
410
def
nil
cons
411
def
cons
nil
cons
cons
nil
cons
cons
412
def
338
ref
subst
412
ref
90
ref
subst
412
remove
169
ref
subst
nil
60
ref
306
ref
cons
413
def
344
ref
cons
nil
cons
cons
414
def
90
ref
subst
415
def
414
ref
169
ref
subst
416
def
nil
409
ref
344
ref
cons
nil
cons
cons
417
def
135
ref
subst
nil
413
ref
63
ref
14
ref
363
ref
appTerm
418
def
150
ref
appTerm
419
def
nil
cons
420
def
cons
nil
cons
421
def
cons
nil
cons
cons
135
ref
subst
nil
182
ref
29
ref
14
ref
301
ref
appTerm
419
ref
appTerm
422
def
absTerm
423
def
nil
cons
cons
nil
cons
nil
cons
cons
194
remove
subst
29
ref
nil
103
ref
422
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
nil
60
ref
301
ref
nil
cons
424
def
cons
421
ref
cons
nil
cons
cons
425
def
90
ref
subst
425
remove
169
ref
subst
302
ref
301
remove
assume
eqMp
nil
60
ref
159
remove
nil
cons
cons
421
ref
cons
nil
cons
cons
135
ref
subst
proveHyp
nil
202
ref
31
ref
14
ref
279
ref
appTerm
419
ref
appTerm
426
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
206
ref
subst
31
ref
nil
103
ref
426
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
nil
60
ref
279
ref
nil
cons
427
def
cons
421
ref
cons
nil
cons
cons
428
def
90
ref
subst
428
remove
169
ref
subst
280
ref
279
remove
assume
eqMp
nil
378
remove
421
remove
cons
nil
cons
cons
429
def
135
ref
subst
proveHyp
429
ref
90
ref
subst
429
remove
169
ref
subst
417
ref
90
ref
subst
417
remove
169
ref
subst
379
remove
135
ref
subst
360
remove
37
ref
appTerm
430
def
betaConv
362
remove
35
ref
appTerm
431
def
betaConv
nil
409
remove
63
ref
431
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
388
ref
370
remove
390
ref
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
nil
60
ref
372
remove
cons
63
ref
430
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
204
ref
374
remove
393
ref
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
112
ref
369
ref
cons
432
def
350
ref
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
nil
394
remove
114
ref
420
remove
cons
nil
cons
433
def
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
112
ref
427
remove
cons
433
ref
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
60
ref
15
ref
249
ref
14
ref
158
remove
249
remove
varTerm
appTerm
appTerm
419
ref
appTerm
absTerm
appTerm
nil
cons
cons
63
ref
233
remove
419
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
204
ref
202
ref
284
remove
cons
434
def
433
ref
cons
nil
cons
cons
nil
60
ref
65
ref
29
ref
14
ref
224
remove
appTerm
435
def
119
ref
appTerm
absTerm
436
def
appTerm
437
def
nil
cons
438
def
cons
439
def
63
ref
14
ref
28
ref
183
ref
appTerm
440
def
appTerm
441
def
119
ref
appTerm
nil
cons
442
def
cons
nil
cons
cons
nil
cons
cons
443
def
90
ref
subst
443
remove
169
ref
subst
nil
60
ref
440
ref
nil
cons
444
def
cons
445
def
63
ref
119
ref
nil
cons
446
def
cons
nil
cons
447
def
cons
nil
cons
cons
448
def
90
ref
subst
448
remove
169
ref
subst
nil
439
ref
447
ref
cons
nil
cons
cons
449
def
135
ref
subst
63
ref
14
ref
65
ref
29
ref
435
remove
78
ref
appTerm
absTerm
appTerm
appTerm
78
ref
appTerm
absTerm
450
def
119
ref
appTerm
451
def
betaConv
nil
445
remove
63
ref
219
ref
450
ref
appTerm
452
def
nil
cons
453
def
cons
nil
cons
cons
nil
cons
cons
454
def
135
ref
subst
73
ref
440
remove
appTerm
455
def
refl
185
remove
219
ref
63
ref
14
ref
65
ref
29
ref
287
remove
78
ref
appTerm
absTerm
appTerm
appTerm
78
remove
appTerm
absTerm
appTerm
absTerm
456
def
183
remove
appTerm
betaConv
appThm
nil
191
remove
28
ref
appTerm
456
remove
appTerm
axiom
192
remove
appThm
eqMp
457
def
nil
60
ref
455
remove
452
ref
appTerm
nil
cons
cons
63
ref
441
remove
452
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
454
remove
nil
60
ref
325
remove
nil
cons
458
def
cons
63
ref
331
ref
cons
nil
cons
cons
nil
cons
cons
459
def
90
ref
subst
459
remove
169
ref
subst
330
remove
eqMp
nil
112
ref
458
remove
cons
114
ref
331
remove
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
460
def
subst
eqMp
eqMp
nil
60
ref
453
remove
cons
63
ref
451
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
213
ref
211
ref
450
remove
nil
cons
cons
221
ref
446
ref
cons
nil
cons
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
112
ref
444
remove
cons
114
ref
446
ref
cons
nil
cons
461
def
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
nil
112
ref
438
remove
cons
462
def
114
ref
442
remove
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
463
def
subst
eqMp
eqMp
eqMp
nil
112
ref
424
remove
cons
433
ref
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
60
ref
65
ref
423
remove
appTerm
nil
cons
cons
63
ref
230
remove
419
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
388
ref
182
ref
305
remove
cons
464
def
433
remove
cons
nil
cons
cons
463
remove
subst
eqMp
eqMp
eqMp
eqMp
nil
112
ref
306
ref
cons
465
def
350
ref
cons
nil
cons
cons
128
ref
subst
466
def
deductAntisym
eqMp
eqMp
nil
432
remove
114
ref
411
ref
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
nil
60
ref
418
remove
410
ref
appTerm
nil
cons
cons
63
ref
14
ref
410
ref
appTerm
363
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
169
ref
subst
proveHyp
nil
60
ref
411
ref
cons
63
ref
369
ref
cons
nil
cons
cons
nil
cons
cons
467
def
90
ref
subst
467
remove
169
ref
subst
371
remove
29
ref
373
remove
375
remove
31
ref
376
remove
380
remove
381
remove
302
remove
sym
280
remove
sym
157
remove
assume
eqMp
204
ref
434
remove
393
remove
cons
nil
cons
cons
457
remove
sym
nil
211
ref
114
ref
14
ref
437
remove
appTerm
119
ref
appTerm
468
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
214
ref
subst
114
ref
nil
103
ref
468
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
449
ref
90
ref
subst
449
remove
169
ref
subst
nil
60
ref
225
remove
cons
447
remove
cons
nil
cons
cons
135
ref
subst
436
ref
35
remove
appTerm
469
def
betaConv
nil
439
remove
63
ref
469
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
388
ref
182
remove
436
remove
nil
cons
cons
390
ref
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
462
remove
461
remove
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
470
def
subst
proveHyp
eqMp
388
remove
464
remove
390
remove
cons
nil
cons
cons
470
remove
subst
proveHyp
414
remove
135
ref
subst
471
def
proveHyp
410
ref
assume
eqMp
eqMp
395
remove
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
112
ref
411
ref
cons
114
ref
369
remove
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
eqMp
absThm
appThm
trans
appThm
nil
60
ref
32
ref
322
remove
appTerm
15
ref
3
ref
410
remove
absTerm
472
def
appTerm
473
def
appTerm
474
def
nil
cons
475
def
cons
476
def
63
ref
15
ref
3
ref
171
ref
150
ref
appTerm
477
def
absTerm
478
def
appTerm
479
def
nil
cons
480
def
cons
nil
cons
cons
nil
cons
cons
481
def
338
ref
subst
481
ref
90
ref
subst
481
remove
169
ref
subst
nil
202
ref
478
ref
nil
cons
cons
482
def
nil
cons
nil
cons
cons
206
ref
subst
483
def
3
ref
nil
103
ref
477
remove
nil
cons
484
def
cons
nil
cons
nil
cons
cons
107
ref
subst
485
def
nil
60
ref
162
ref
nil
cons
486
def
cons
487
def
344
ref
cons
nil
cons
cons
488
def
90
ref
subst
489
def
488
ref
169
ref
subst
490
def
nil
476
remove
344
ref
cons
nil
cons
cons
491
def
135
ref
subst
nil
413
remove
63
ref
14
ref
474
ref
appTerm
492
def
150
ref
appTerm
nil
cons
493
def
cons
nil
cons
494
def
cons
nil
cons
cons
495
def
90
ref
subst
495
remove
169
ref
subst
491
ref
90
ref
subst
496
def
491
remove
169
ref
subst
497
def
471
remove
472
ref
20
ref
appTerm
498
def
betaConv
nil
356
remove
114
ref
473
remove
nil
cons
499
def
cons
nil
cons
cons
nil
cons
cons
500
def
337
ref
subst
nil
60
ref
499
ref
cons
63
ref
498
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
204
ref
202
ref
472
remove
nil
cons
cons
501
def
250
ref
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
112
ref
475
ref
cons
502
def
350
ref
cons
nil
cons
cons
128
ref
subst
503
def
deductAntisym
eqMp
eqMp
nil
465
remove
114
ref
493
ref
cons
nil
cons
504
def
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
nil
342
remove
494
remove
cons
nil
cons
cons
505
def
90
ref
subst
505
remove
169
ref
subst
496
remove
497
remove
345
remove
135
ref
subst
321
remove
20
ref
appTerm
506
def
betaConv
500
remove
128
ref
subst
nil
352
ref
63
ref
506
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
204
ref
339
remove
250
ref
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
eqMp
eqMp
503
remove
deductAntisym
eqMp
eqMp
nil
349
ref
504
remove
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
nil
349
ref
114
ref
306
remove
cons
507
def
"R"
6
ref
var
508
def
493
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
60
ref
14
ref
119
ref
appTerm
509
def
508
remove
varTerm
510
def
appTerm
511
def
nil
cons
cons
63
ref
510
ref
nil
cons
512
def
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
nil
60
ref
14
ref
117
ref
appTerm
513
def
510
ref
appTerm
nil
cons
cons
63
ref
14
ref
511
remove
appTerm
510
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
"r"
6
remove
var
514
def
14
ref
513
ref
514
ref
varTerm
515
def
appTerm
appTerm
516
def
14
ref
509
ref
515
ref
appTerm
appTerm
515
ref
appTerm
appTerm
absTerm
517
def
510
remove
appTerm
518
def
betaConv
73
ref
16
ref
117
ref
appTerm
519
def
119
ref
appTerm
520
def
appTerm
refl
63
ref
219
ref
514
ref
516
remove
14
ref
333
remove
515
ref
appTerm
521
def
appTerm
522
def
515
ref
appTerm
523
def
appTerm
absTerm
appTerm
absTerm
119
remove
appTerm
betaConv
appThm
99
remove
519
remove
appTerm
refl
60
ref
63
ref
219
ref
514
ref
14
ref
77
remove
515
ref
appTerm
524
def
appTerm
523
remove
appTerm
absTerm
appTerm
absTerm
absTerm
525
def
117
ref
appTerm
betaConv
appThm
nil
87
remove
16
remove
appTerm
525
remove
appTerm
axiom
126
remove
appThm
eqMp
122
remove
appThm
eqMp
526
def
520
remove
assume
eqMp
nil
60
ref
219
remove
517
ref
appTerm
nil
cons
cons
63
ref
518
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
213
remove
211
ref
517
remove
nil
cons
cons
221
remove
512
remove
cons
nil
cons
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
eqMp
eqMp
subst
proveHyp
proveHyp
eqMp
eqMp
nil
112
ref
486
ref
cons
350
ref
cons
nil
cons
cons
128
ref
subst
527
def
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
502
remove
114
ref
480
ref
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
nil
60
ref
492
remove
479
ref
appTerm
nil
cons
cons
63
ref
14
ref
479
remove
appTerm
474
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
169
ref
subst
proveHyp
nil
60
ref
480
ref
cons
528
def
63
ref
475
ref
cons
nil
cons
cons
nil
cons
cons
529
def
90
ref
subst
529
remove
169
ref
subst
340
remove
3
ref
341
remove
346
remove
347
remove
nil
528
ref
344
remove
cons
nil
cons
cons
530
def
135
ref
subst
531
def
nil
349
remove
507
remove
nil
cons
cons
nil
cons
cons
532
def
526
remove
sym
533
def
nil
211
remove
103
ref
14
ref
513
remove
105
ref
appTerm
534
def
appTerm
14
ref
509
remove
105
ref
appTerm
535
def
appTerm
105
ref
appTerm
536
def
appTerm
537
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
214
remove
subst
538
def
103
ref
nil
103
ref
537
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
539
def
nil
60
ref
534
ref
nil
cons
540
def
cons
63
ref
536
remove
nil
cons
541
def
cons
nil
cons
cons
nil
cons
cons
542
def
90
ref
subst
543
def
542
remove
169
ref
subst
544
def
nil
60
ref
535
ref
nil
cons
545
def
cons
63
ref
105
remove
nil
cons
546
def
cons
nil
cons
547
def
cons
nil
cons
cons
548
def
90
ref
subst
549
def
548
remove
169
ref
subst
550
def
nil
60
ref
117
remove
nil
cons
cons
547
ref
cons
nil
cons
cons
135
ref
subst
534
remove
assume
eqMp
eqMp
nil
112
ref
545
remove
cons
114
ref
546
remove
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
551
def
deductAntisym
eqMp
eqMp
nil
112
ref
540
remove
cons
114
ref
541
remove
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
552
def
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
subst
530
ref
90
ref
subst
530
remove
169
ref
subst
488
remove
135
ref
subst
478
remove
20
ref
appTerm
553
def
betaConv
nil
528
remove
63
ref
553
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
204
ref
482
remove
250
ref
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
112
ref
480
remove
cons
554
def
350
remove
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
555
def
proveHyp
eqMp
eqMp
351
remove
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
352
remove
63
ref
499
remove
cons
nil
cons
cons
nil
cons
cons
169
ref
subst
proveHyp
nil
501
remove
nil
cons
nil
cons
cons
206
ref
subst
3
ref
nil
103
ref
411
remove
cons
nil
cons
nil
cons
cons
107
ref
subst
415
remove
416
remove
531
remove
532
remove
533
remove
538
remove
103
ref
539
remove
543
remove
544
remove
549
remove
550
remove
nil
60
ref
446
remove
cons
547
remove
cons
nil
cons
cons
135
ref
subst
535
remove
assume
eqMp
eqMp
551
remove
deductAntisym
eqMp
eqMp
552
remove
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
subst
555
remove
proveHyp
eqMp
eqMp
466
remove
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
eqMp
nil
554
remove
114
ref
475
remove
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
eqMp
trans
sym
556
def
483
remove
3
ref
485
remove
489
remove
490
remove
156
ref
refl
57
remove
20
ref
appTerm
betaConv
appThm
138
remove
assume
20
ref
refl
appThm
eqMp
557
def
sym
nil
170
ref
55
ref
nil
cons
cons
558
def
nil
cons
nil
cons
cons
195
ref
subst
11
ref
nil
103
ref
54
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
nil
60
ref
52
remove
nil
cons
559
def
cons
560
def
63
ref
49
ref
nil
cons
561
def
cons
nil
cons
562
def
cons
nil
cons
cons
563
def
90
ref
subst
563
ref
169
ref
subst
nil
487
ref
562
ref
cons
nil
cons
cons
135
ref
subst
51
ref
20
ref
appTerm
564
def
betaConv
nil
560
ref
63
ref
564
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
204
ref
202
ref
51
remove
nil
cons
cons
250
ref
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
nil
60
ref
50
ref
nil
cons
cons
63
ref
171
remove
49
ref
appTerm
565
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
173
remove
20
ref
appTerm
566
def
betaConv
nil
248
remove
nil
cons
nil
cons
cons
206
ref
subst
3
ref
246
remove
nil
60
ref
343
ref
cons
567
def
562
remove
cons
nil
cons
cons
568
def
90
ref
subst
568
remove
169
ref
subst
563
remove
135
ref
subst
55
remove
41
ref
appTerm
569
def
betaConv
nil
567
ref
63
ref
56
ref
nil
cons
570
def
cons
nil
cons
cons
nil
cons
cons
571
def
135
ref
subst
557
remove
nil
60
ref
156
remove
56
ref
appTerm
nil
cons
cons
63
ref
151
ref
56
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
571
remove
460
remove
subst
eqMp
eqMp
nil
60
ref
570
remove
cons
63
ref
569
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
180
ref
558
remove
"x"
8
ref
var
572
def
41
ref
nil
cons
573
def
cons
nil
cons
574
def
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
112
ref
343
remove
cons
114
ref
561
ref
cons
nil
cons
575
def
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
576
def
201
remove
135
ref
subst
proveHyp
176
remove
41
remove
appTerm
577
def
betaConv
178
ref
137
ref
appTerm
578
def
betaConv
nil
60
ref
10
ref
178
ref
appTerm
nil
cons
cons
579
def
63
ref
578
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
180
ref
179
ref
572
ref
137
ref
nil
cons
cons
nil
cons
580
def
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
nil
60
ref
196
remove
cons
63
ref
577
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
180
ref
197
remove
574
remove
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
eqMp
nil
60
ref
200
remove
cons
63
ref
566
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
204
ref
203
remove
250
ref
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
nil
60
ref
207
remove
cons
63
ref
14
ref
50
remove
appTerm
565
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
nil
487
remove
63
ref
48
ref
nil
cons
cons
514
remove
561
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
332
remove
63
ref
522
remove
524
ref
appTerm
nil
cons
581
def
cons
nil
cons
cons
nil
cons
cons
582
def
90
ref
subst
582
remove
169
ref
subst
nil
60
ref
521
ref
nil
cons
583
def
cons
63
ref
524
remove
nil
cons
584
def
cons
nil
cons
cons
nil
cons
cons
585
def
90
ref
subst
585
remove
169
ref
subst
nil
215
remove
63
ref
515
remove
nil
cons
586
def
cons
nil
cons
587
def
cons
nil
cons
cons
588
def
90
ref
subst
588
remove
169
ref
subst
134
remove
nil
327
remove
587
remove
cons
nil
cons
cons
135
ref
subst
proveHyp
521
remove
assume
eqMp
eqMp
nil
113
remove
114
ref
586
remove
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
nil
112
ref
583
remove
cons
114
ref
584
remove
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
nil
335
remove
114
ref
581
remove
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
eqMp
eqMp
nil
112
ref
559
remove
cons
589
def
575
remove
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
eqMp
527
remove
deductAntisym
eqMp
590
def
eqMp
absThm
eqMp
591
def
eqMp
nil
60
ref
149
remove
nil
cons
cons
63
ref
166
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
169
ref
subst
proveHyp
10
ref
refl
11
ref
277
ref
nil
136
remove
573
remove
cons
nil
cons
nil
cons
cons
556
remove
subst
appThm
154
ref
refl
appThm
absThm
appThm
nil
170
ref
11
ref
53
remove
154
remove
appTerm
592
def
absTerm
593
def
nil
cons
cons
594
def
nil
cons
nil
cons
cons
195
remove
subst
11
ref
nil
103
ref
592
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
nil
560
remove
63
ref
198
ref
cons
nil
cons
cons
nil
cons
cons
595
def
90
remove
subst
595
remove
169
ref
subst
576
remove
eqMp
nil
589
remove
114
ref
198
remove
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
596
def
nil
60
ref
10
ref
593
ref
appTerm
nil
cons
597
def
cons
598
def
63
ref
165
remove
nil
cons
599
def
cons
nil
cons
600
def
cons
nil
cons
cons
169
ref
subst
proveHyp
nil
202
ref
164
remove
nil
cons
cons
nil
cons
nil
cons
cons
206
ref
subst
3
ref
nil
103
ref
163
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
nil
567
remove
63
ref
486
remove
cons
nil
cons
cons
nil
cons
cons
338
remove
subst
3
ref
151
ref
162
ref
appTerm
601
def
absTerm
602
def
20
ref
appTerm
603
def
betaConv
278
ref
3
ref
151
ref
refl
3
ref
162
ref
absTerm
604
def
20
ref
appTerm
605
def
betaConv
606
def
appThm
absThm
appThm
278
ref
3
ref
14
ref
24
remove
28
remove
29
ref
30
remove
31
ref
40
remove
604
ref
37
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
607
def
refl
606
ref
appThm
absThm
appThm
sym
278
remove
3
ref
277
remove
606
remove
appThm
150
ref
refl
appThm
absThm
appThm
sym
591
remove
eqMp
nil
60
ref
15
ref
3
ref
14
ref
605
ref
appTerm
608
def
150
remove
appTerm
absTerm
appTerm
nil
cons
cons
63
ref
15
ref
3
ref
607
ref
162
remove
appTerm
absTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
11
remove
14
ref
15
ref
3
ref
608
remove
49
remove
appTerm
absTerm
appTerm
appTerm
15
ref
3
ref
607
ref
48
remove
appTerm
absTerm
appTerm
appTerm
absTerm
609
def
137
remove
appTerm
610
def
betaConv
178
remove
604
ref
appTerm
611
def
betaConv
nil
579
remove
63
ref
611
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
180
ref
179
remove
572
remove
604
ref
nil
cons
cons
nil
cons
612
def
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
nil
60
ref
10
ref
609
ref
appTerm
nil
cons
cons
63
ref
610
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
180
ref
170
remove
609
remove
nil
cons
cons
580
remove
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
60
ref
15
ref
3
ref
607
remove
605
ref
appTerm
absTerm
appTerm
nil
cons
cons
63
ref
15
ref
3
ref
151
remove
605
remove
appTerm
absTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
593
remove
604
remove
appTerm
613
def
betaConv
596
remove
nil
598
remove
63
ref
613
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
proveHyp
180
remove
594
remove
612
remove
cons
nil
cons
cons
227
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
60
ref
15
ref
602
ref
appTerm
nil
cons
cons
63
ref
603
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
remove
subst
proveHyp
204
remove
202
ref
602
remove
nil
cons
cons
250
remove
cons
nil
cons
cons
227
remove
subst
eqMp
eqMp
nil
60
ref
601
remove
nil
cons
cons
63
remove
484
remove
cons
nil
cons
cons
nil
cons
cons
169
ref
subst
proveHyp
590
remove
eqMp
eqMp
eqMp
absThm
eqMp
614
def
eqMp
nil
112
ref
597
remove
cons
114
ref
599
remove
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
proveHyp
eqMp
nil
60
remove
155
remove
nil
cons
cons
600
remove
cons
nil
cons
cons
169
remove
subst
proveHyp
614
remove
eqMp
eqMp
proveHyp
eqMp
nil
112
ref
139
remove
cons
114
ref
167
remove
cons
nil
cons
cons
nil
cons
cons
128
ref
subst
deductAntisym
eqMp
subst
eqMp
615
def
nil
112
ref
68
remove
nil
cons
cons
114
ref
75
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
616
def
128
ref
subst
proveHyp
617
def
nil
112
ref
64
ref
nil
cons
cons
114
ref
67
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
618
def
128
ref
subst
proveHyp
nil
64
remove
thm
nil
202
remove
31
ref
73
ref
"Set.infinite"
"_9825"
2
remove
var
619
def
"Data.Bool.~"
const
12
remove
constTerm
620
def
62
remove
619
ref
varTerm
621
def
appTerm
appTerm
622
def
absTerm
623
def
defineConst
624
def
pop
8
remove
constTerm
625
def
37
ref
appTerm
appTerm
620
remove
66
remove
appTerm
appTerm
absTerm
626
def
nil
cons
cons
nil
cons
nil
cons
cons
206
remove
subst
619
remove
nil
103
remove
73
remove
625
remove
621
ref
appTerm
appTerm
622
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
107
remove
subst
624
remove
621
ref
refl
appThm
623
remove
621
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
15
ref
626
remove
appTerm
thm
617
remove
618
remove
337
ref
subst
proveHyp
nil
67
remove
thm
615
remove
616
remove
337
ref
subst
proveHyp
627
def
nil
112
remove
72
remove
nil
cons
cons
114
remove
74
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
628
def
337
remove
subst
proveHyp
nil
74
remove
thm
627
remove
628
remove
128
remove
subst
proveHyp
nil
10
remove
283
ref
14
ref
32
remove
283
remove
varTerm
629
def
22
remove
appTerm
appTerm
65
remove
29
remove
15
ref
31
remove
14
remove
629
ref
37
remove
appTerm
appTerm
629
ref
38
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
15
remove
3
remove
71
remove
629
remove
20
remove
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
thm