6
version
nil
"P"
"->"
typeOp
0
def
"A"
varType
1
def
"bool"
typeOp
nil
opType
2
def
nil
cons
3
def
cons
opType
4
def
var
5
def
"a"
1
ref
var
6
def
"Data.Bool.!"
const
7
def
0
ref
0
ref
"B"
varType
8
def
3
ref
cons
opType
9
def
3
ref
cons
opType
10
def
constTerm
11
def
"b"
8
ref
var
12
def
7
ref
0
ref
4
ref
3
ref
cons
opType
13
def
constTerm
14
def
"a'"
1
ref
var
15
def
11
ref
"b'"
8
ref
var
16
def
"="
const
17
def
0
ref
2
ref
0
ref
2
ref
3
ref
cons
opType
18
def
nil
cons
cons
opType
19
def
constTerm
20
def
17
ref
0
ref
"Data.Pair.*"
"HOLLight.ABS_prod"
"HOLLight.REP_prod"
"A"
"B"
nil
cons
cons
"A"
0
ref
1
ref
9
ref
nil
cons
21
def
cons
opType
22
def
nil
cons
23
def
cons
nil
cons
24
def
nil
nil
cons
25
def
cons
26
def
nil
17
ref
0
ref
13
ref
0
ref
13
ref
3
ref
cons
opType
27
def
nil
cons
cons
opType
constTerm
28
def
"Data.Bool.?"
const
29
def
13
ref
constTerm
30
def
appTerm
31
def
"p"
4
ref
var
32
def
32
ref
varTerm
33
def
"select"
const
34
def
0
ref
4
ref
1
ref
nil
cons
35
def
cons
opType
constTerm
36
def
33
ref
appTerm
37
def
appTerm
absTerm
appTerm
axiom
subst
"x"
22
ref
var
38
def
30
ref
6
ref
29
ref
10
remove
constTerm
39
def
12
ref
17
ref
0
ref
22
ref
0
ref
22
ref
3
ref
cons
opType
40
def
nil
cons
cons
opType
constTerm
41
def
38
ref
varTerm
42
def
appTerm
"HOLLight.mk_pair"
"x"
1
ref
var
43
def
"y"
8
ref
var
44
def
6
ref
12
ref
"Data.Bool./\\"
const
19
ref
constTerm
45
def
17
ref
0
ref
1
ref
4
ref
nil
cons
46
def
cons
opType
constTerm
47
def
6
ref
varTerm
48
def
appTerm
49
def
43
ref
varTerm
50
def
appTerm
appTerm
17
ref
0
ref
8
ref
21
ref
cons
opType
constTerm
51
def
12
ref
varTerm
52
def
appTerm
53
def
44
ref
varTerm
54
def
appTerm
55
def
appTerm
absTerm
absTerm
absTerm
56
def
absTerm
57
def
defineConst
58
def
pop
0
ref
1
ref
0
ref
8
ref
23
ref
cons
opType
nil
cons
cons
opType
constTerm
59
def
48
ref
appTerm
60
def
52
ref
appTerm
61
def
appTerm
62
def
absTerm
63
def
appTerm
absTerm
64
def
appTerm
absTerm
65
def
refl
appThm
"p"
40
ref
var
66
def
66
ref
varTerm
67
def
34
ref
0
ref
40
ref
23
ref
cons
opType
constTerm
67
remove
appTerm
appTerm
absTerm
65
ref
appTerm
betaConv
trans
nil
"p"
2
ref
var
68
def
29
ref
0
ref
40
ref
3
ref
cons
opType
69
def
constTerm
65
ref
appTerm
70
def
nil
cons
cons
nil
cons
nil
cons
cons
20
ref
68
ref
varTerm
71
def
appTerm
72
def
refl
73
def
nil
"t"
2
ref
var
74
def
"Data.Bool.~"
const
18
ref
constTerm
75
def
71
ref
appTerm
76
def
nil
cons
77
def
cons
nil
cons
nil
cons
cons
74
ref
20
ref
"Data.Bool.==>"
const
19
ref
constTerm
78
def
74
ref
varTerm
79
def
appTerm
80
def
"Data.Bool.F"
const
2
ref
constTerm
81
def
appTerm
appTerm
75
ref
79
ref
appTerm
82
def
appTerm
absTerm
83
def
79
ref
appTerm
84
def
betaConv
nil
7
ref
0
ref
18
ref
3
ref
cons
opType
85
def
constTerm
86
def
83
ref
appTerm
87
def
axiom
nil
68
ref
87
remove
nil
cons
cons
"q"
2
ref
var
88
def
84
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
20
ref
78
ref
71
ref
appTerm
89
def
88
ref
varTerm
90
def
appTerm
91
def
appTerm
refl
68
ref
88
ref
20
ref
45
ref
71
ref
appTerm
92
def
90
ref
appTerm
93
def
appTerm
94
def
71
ref
appTerm
absTerm
95
def
absTerm
96
def
71
ref
appTerm
betaConv
90
ref
refl
97
def
appThm
95
remove
90
ref
appTerm
betaConv
trans
appThm
nil
17
ref
0
ref
19
ref
0
ref
19
ref
3
ref
cons
opType
98
def
nil
cons
cons
opType
constTerm
99
def
78
ref
appTerm
96
remove
appTerm
axiom
71
ref
refl
100
def
appThm
97
ref
appThm
eqMp
101
def
sym
102
def
94
remove
refl
88
ref
17
ref
0
ref
98
ref
0
ref
98
remove
3
ref
cons
opType
nil
cons
cons
opType
constTerm
103
def
"f"
19
ref
var
104
def
104
ref
varTerm
105
def
71
ref
appTerm
90
ref
appTerm
absTerm
106
def
appTerm
104
ref
105
ref
"Data.Bool.T"
const
2
ref
constTerm
107
def
appTerm
107
ref
appTerm
absTerm
108
def
appTerm
absTerm
109
def
90
ref
appTerm
betaConv
appThm
17
ref
0
ref
18
ref
85
remove
nil
cons
cons
opType
constTerm
110
def
92
ref
appTerm
refl
68
ref
109
remove
absTerm
111
def
71
ref
appTerm
betaConv
appThm
nil
99
ref
45
ref
appTerm
111
ref
appTerm
axiom
112
def
100
remove
appThm
eqMp
97
ref
appThm
eqMp
113
def
sym
104
ref
105
ref
refl
nil
74
ref
71
ref
nil
cons
114
def
cons
nil
cons
nil
cons
cons
115
def
20
ref
79
ref
appTerm
116
def
107
ref
appTerm
117
def
assume
sym
nil
107
ref
axiom
118
def
eqMp
79
ref
assume
118
ref
deductAntisym
deductAntisym
119
def
subst
71
ref
assume
120
def
eqMp
appThm
nil
74
ref
90
ref
nil
cons
121
def
cons
nil
cons
nil
cons
cons
122
def
119
ref
subst
90
ref
assume
123
def
eqMp
appThm
absThm
eqMp
124
def
nil
"P"
2
ref
var
125
def
114
ref
cons
"Q"
2
ref
var
126
def
121
ref
cons
nil
cons
127
def
cons
nil
cons
cons
20
ref
refl
128
def
104
ref
105
remove
125
ref
varTerm
129
def
appTerm
130
def
126
ref
varTerm
131
def
appTerm
absTerm
132
def
68
ref
88
ref
71
ref
absTerm
absTerm
133
def
appTerm
betaConv
133
ref
129
ref
appTerm
betaConv
131
ref
refl
134
def
appThm
88
ref
129
ref
absTerm
131
ref
appTerm
betaConv
trans
trans
appThm
108
ref
133
ref
appTerm
betaConv
133
ref
107
ref
appTerm
betaConv
107
ref
refl
135
def
appThm
88
ref
107
ref
absTerm
107
ref
appTerm
betaConv
trans
trans
appThm
20
ref
45
ref
129
ref
appTerm
136
def
131
ref
appTerm
137
def
appTerm
refl
88
ref
103
remove
104
remove
130
remove
90
ref
appTerm
absTerm
appTerm
108
ref
appTerm
absTerm
131
ref
appTerm
betaConv
appThm
110
ref
136
remove
appTerm
refl
111
remove
129
ref
appTerm
betaConv
appThm
112
remove
129
ref
refl
138
def
appThm
eqMp
134
ref
appThm
eqMp
137
remove
assume
eqMp
139
def
133
remove
refl
appThm
eqMp
sym
118
ref
eqMp
140
def
subst
deductAntisym
eqMp
101
remove
91
ref
assume
eqMp
sym
120
remove
eqMp
128
ref
106
remove
68
ref
88
ref
90
ref
absTerm
141
def
absTerm
142
def
appTerm
betaConv
142
ref
71
ref
appTerm
betaConv
97
ref
appThm
141
ref
90
ref
appTerm
betaConv
trans
trans
appThm
108
remove
142
ref
appTerm
betaConv
142
ref
107
ref
appTerm
betaConv
135
remove
appThm
141
ref
107
ref
appTerm
betaConv
trans
trans
143
def
appThm
113
remove
93
ref
assume
eqMp
142
ref
refl
144
def
appThm
eqMp
sym
118
ref
eqMp
145
def
proveHyp
deductAntisym
146
def
subst
proveHyp
"A"
3
ref
cons
nil
cons
147
def
"P"
18
remove
var
148
def
83
remove
nil
cons
cons
"x"
2
ref
var
149
def
79
ref
nil
cons
cons
nil
cons
150
def
cons
nil
cons
cons
nil
68
ref
14
ref
5
ref
varTerm
151
def
appTerm
152
def
nil
cons
153
def
cons
88
ref
151
ref
50
ref
appTerm
154
def
nil
cons
155
def
cons
nil
cons
cons
nil
cons
cons
156
def
102
ref
subst
156
remove
145
remove
124
remove
deductAntisym
157
def
subst
20
ref
154
ref
appTerm
refl
43
ref
107
ref
absTerm
158
def
50
ref
appTerm
betaConv
appThm
32
ref
17
ref
0
ref
4
ref
13
ref
nil
cons
cons
opType
constTerm
33
ref
appTerm
158
remove
appTerm
absTerm
159
def
151
ref
appTerm
betaConv
160
def
nil
28
remove
14
ref
appTerm
159
remove
appTerm
axiom
151
ref
refl
161
def
appThm
162
def
152
ref
assume
eqMp
eqMp
50
ref
refl
163
def
appThm
eqMp
sym
118
ref
eqMp
eqMp
nil
125
ref
153
remove
cons
126
ref
155
ref
cons
nil
cons
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
164
def
subst
eqMp
eqMp
165
def
subst
appThm
sym
73
remove
115
ref
74
ref
20
ref
75
ref
82
ref
appTerm
appTerm
79
ref
appTerm
absTerm
166
def
79
ref
appTerm
167
def
betaConv
nil
86
ref
166
ref
appTerm
168
def
axiom
nil
68
ref
168
remove
nil
cons
cons
88
ref
167
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
166
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
169
def
subst
appThm
nil
149
ref
114
ref
cons
nil
cons
170
def
nil
cons
cons
147
ref
25
ref
cons
171
def
nil
74
ref
47
ref
50
ref
appTerm
172
def
50
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
163
ref
eqMp
173
def
subst
174
def
subst
trans
sym
118
ref
eqMp
eqMp
175
def
subst
sym
nil
68
ref
75
ref
70
remove
appTerm
176
def
nil
cons
177
def
cons
88
ref
81
ref
nil
cons
178
def
cons
nil
cons
179
def
cons
nil
cons
cons
180
def
102
ref
subst
180
remove
157
ref
subst
nil
38
ref
59
ref
"_1188"
1
ref
var
varTerm
181
def
appTerm
"_1189"
8
ref
var
varTerm
182
def
appTerm
183
def
nil
cons
184
def
cons
nil
cons
nil
cons
cons
26
ref
163
ref
subst
185
def
subst
nil
68
ref
41
ref
183
ref
appTerm
183
remove
appTerm
nil
cons
cons
179
ref
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
"_1183"
8
ref
var
186
def
182
remove
nil
cons
cons
"_1182"
1
ref
var
187
def
181
remove
nil
cons
cons
"_1181"
22
ref
var
188
def
184
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
68
ref
41
ref
188
remove
varTerm
189
def
appTerm
190
def
59
ref
187
remove
varTerm
191
def
appTerm
192
def
186
remove
varTerm
193
def
appTerm
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
20
ref
76
ref
appTerm
refl
115
remove
165
ref
subst
appThm
nil
149
ref
77
remove
cons
nil
cons
nil
cons
cons
174
ref
subst
trans
sym
118
ref
eqMp
194
def
subst
12
ref
75
ref
190
ref
192
remove
52
ref
appTerm
appTerm
appTerm
absTerm
195
def
193
ref
appTerm
196
def
betaConv
6
ref
11
ref
12
ref
75
ref
190
remove
61
ref
appTerm
appTerm
absTerm
appTerm
absTerm
197
def
191
ref
appTerm
198
def
betaConv
38
ref
14
ref
6
ref
11
ref
12
ref
75
ref
62
remove
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
199
def
189
ref
appTerm
200
def
betaConv
nil
"P"
40
ref
var
201
def
65
ref
nil
cons
cons
nil
cons
nil
cons
cons
26
ref
128
ref
75
ref
refl
202
def
30
ref
refl
203
def
nil
"t"
4
ref
var
151
ref
nil
cons
204
def
cons
nil
cons
nil
cons
cons
"A"
35
ref
cons
205
def
"B"
3
ref
cons
nil
cons
206
def
cons
25
ref
cons
"t"
0
ref
1
ref
8
ref
nil
cons
207
def
cons
208
def
opType
209
def
var
210
def
17
remove
0
ref
209
ref
0
ref
209
ref
3
ref
cons
opType
211
def
nil
cons
cons
opType
constTerm
212
def
210
ref
varTerm
213
def
appTerm
43
ref
213
ref
50
ref
appTerm
absTerm
214
def
appTerm
215
def
absTerm
216
def
213
ref
appTerm
217
def
betaConv
7
ref
0
ref
211
ref
3
ref
cons
opType
218
def
constTerm
219
def
refl
220
def
210
ref
215
remove
assume
sym
212
ref
214
remove
appTerm
213
ref
appTerm
221
def
assume
sym
deductAntisym
absThm
appThm
nil
219
ref
210
remove
221
remove
absTerm
appTerm
axiom
eqMp
nil
68
ref
219
ref
216
ref
appTerm
nil
cons
cons
88
ref
217
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
"A"
209
ref
nil
cons
cons
nil
cons
222
def
"P"
211
remove
var
223
def
216
remove
nil
cons
cons
"x"
209
ref
var
224
def
213
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
subst
subst
225
def
appThm
appThm
appThm
14
ref
43
ref
75
ref
154
ref
appTerm
absTerm
226
def
appTerm
refl
appThm
sym
nil
32
ref
204
remove
cons
nil
cons
nil
cons
cons
227
def
32
ref
20
ref
75
ref
30
ref
43
ref
33
ref
50
ref
appTerm
228
def
absTerm
229
def
appTerm
230
def
appTerm
appTerm
14
ref
43
ref
75
ref
228
ref
appTerm
absTerm
231
def
appTerm
appTerm
absTerm
232
def
33
ref
appTerm
233
def
betaConv
nil
7
ref
27
remove
constTerm
234
def
232
ref
appTerm
235
def
axiom
nil
68
ref
235
remove
nil
cons
cons
88
ref
233
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
"A"
46
ref
cons
nil
cons
236
def
"P"
13
remove
var
237
def
232
remove
nil
cons
cons
"x"
4
ref
var
238
def
33
ref
nil
cons
cons
nil
cons
239
def
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
subst
eqMp
240
def
subst
subst
7
ref
69
remove
constTerm
241
def
refl
242
def
38
ref
202
ref
65
ref
42
remove
appTerm
betaConv
appThm
nil
5
ref
64
ref
nil
cons
cons
nil
cons
nil
cons
cons
240
ref
subst
14
ref
refl
243
def
6
ref
202
ref
64
remove
48
ref
appTerm
betaConv
appThm
nil
"P"
9
ref
var
244
def
63
ref
nil
cons
cons
nil
cons
nil
cons
cons
"A"
207
ref
cons
245
def
nil
cons
246
def
25
ref
cons
247
def
240
ref
subst
248
def
subst
11
ref
refl
249
def
12
ref
202
ref
63
remove
52
ref
appTerm
betaConv
appThm
absThm
appThm
trans
trans
absThm
appThm
trans
trans
absThm
appThm
trans
176
remove
assume
eqMp
nil
68
ref
241
ref
199
ref
appTerm
nil
cons
cons
88
ref
200
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
24
ref
201
ref
199
remove
nil
cons
cons
38
ref
189
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
14
ref
197
ref
appTerm
nil
cons
cons
88
ref
198
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
205
ref
nil
cons
250
def
5
ref
197
remove
nil
cons
cons
43
ref
191
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
11
ref
195
ref
appTerm
nil
cons
cons
88
ref
196
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
246
ref
244
ref
195
remove
nil
cons
cons
"x"
8
ref
var
251
def
193
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
eqMp
subst
eqMp
eqMp
nil
125
ref
177
remove
cons
126
ref
178
ref
cons
nil
cons
252
def
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
eqMp
defineTypeOp
253
def
pop
254
def
pop
255
def
pop
256
def
pop
208
remove
opType
257
def
0
ref
257
ref
3
ref
cons
opType
258
def
nil
cons
cons
opType
constTerm
259
def
"Data.Pair.,"
43
ref
44
ref
256
remove
0
ref
22
ref
257
ref
nil
cons
260
def
cons
opType
constTerm
261
def
59
ref
50
ref
appTerm
54
ref
appTerm
262
def
appTerm
263
def
absTerm
264
def
absTerm
265
def
defineConst
266
def
pop
0
ref
1
ref
0
ref
8
ref
260
ref
cons
opType
nil
cons
cons
opType
constTerm
267
def
48
ref
appTerm
268
def
52
ref
appTerm
269
def
appTerm
267
ref
15
ref
varTerm
270
def
appTerm
16
ref
varTerm
271
def
appTerm
272
def
appTerm
273
def
appTerm
45
ref
49
ref
270
ref
appTerm
274
def
appTerm
275
def
53
ref
271
ref
appTerm
276
def
appTerm
277
def
appTerm
278
def
absTerm
279
def
appTerm
280
def
absTerm
281
def
appTerm
282
def
absTerm
283
def
appTerm
284
def
absTerm
285
def
nil
cons
cons
nil
cons
nil
cons
cons
20
ref
152
remove
appTerm
refl
160
remove
appThm
162
remove
eqMp
sym
286
def
subst
6
ref
nil
74
ref
284
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
nil
244
ref
283
remove
nil
cons
cons
nil
cons
nil
cons
cons
247
ref
286
ref
subst
287
def
subst
12
ref
nil
74
ref
282
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
nil
5
ref
281
remove
nil
cons
cons
nil
cons
nil
cons
cons
286
ref
subst
15
ref
nil
74
ref
280
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
nil
244
ref
279
remove
nil
cons
cons
nil
cons
nil
cons
cons
287
ref
subst
16
ref
nil
74
ref
278
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
nil
68
ref
273
ref
nil
cons
288
def
cons
289
def
88
ref
277
ref
nil
cons
290
def
cons
nil
cons
291
def
cons
nil
cons
cons
78
ref
refl
292
def
72
ref
90
ref
appTerm
293
def
assume
294
def
appThm
97
ref
appThm
sym
nil
68
ref
121
ref
cons
295
def
88
ref
121
ref
cons
nil
cons
cons
nil
cons
cons
296
def
102
ref
subst
296
remove
157
ref
subst
123
remove
eqMp
nil
125
ref
121
ref
cons
127
remove
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
297
def
eqMp
298
def
nil
68
ref
91
remove
nil
cons
299
def
cons
88
ref
78
ref
90
ref
appTerm
300
def
71
ref
appTerm
nil
cons
301
def
cons
nil
cons
cons
nil
cons
cons
157
ref
subst
proveHyp
300
ref
refl
294
remove
appThm
sym
297
remove
eqMp
eqMp
nil
295
remove
88
ref
114
ref
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
nil
125
ref
299
ref
cons
126
ref
301
remove
cons
nil
cons
cons
nil
cons
cons
302
def
128
ref
132
remove
142
ref
appTerm
betaConv
142
remove
129
ref
appTerm
betaConv
134
ref
appThm
141
remove
131
ref
appTerm
betaConv
trans
trans
appThm
143
remove
appThm
139
remove
144
remove
appThm
eqMp
sym
118
ref
eqMp
303
def
subst
eqMp
146
ref
302
remove
140
ref
subst
eqMp
deductAntisym
deductAntisym
304
def
subst
292
ref
259
ref
refl
305
def
nil
44
ref
52
ref
nil
cons
306
def
cons
43
ref
48
ref
nil
cons
307
def
cons
308
def
nil
cons
309
def
cons
nil
cons
cons
310
def
266
remove
163
ref
appThm
265
remove
50
ref
appTerm
betaConv
trans
54
ref
refl
311
def
appThm
264
remove
54
ref
appTerm
betaConv
trans
312
def
subst
313
def
appThm
nil
44
ref
271
ref
nil
cons
cons
43
ref
270
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
314
def
312
remove
subst
appThm
appThm
277
ref
refl
315
def
appThm
sym
nil
68
ref
259
ref
261
ref
61
ref
appTerm
316
def
appTerm
317
def
261
ref
59
ref
270
ref
appTerm
271
ref
appTerm
318
def
appTerm
319
def
appTerm
320
def
nil
cons
321
def
cons
291
ref
cons
nil
cons
cons
322
def
102
ref
subst
322
remove
157
ref
subst
255
remove
0
ref
257
ref
23
remove
cons
opType
constTerm
323
def
refl
324
def
320
ref
assume
appThm
nil
68
ref
41
ref
323
ref
316
ref
appTerm
appTerm
323
ref
319
remove
appTerm
appTerm
nil
cons
cons
291
ref
cons
nil
cons
cons
146
ref
subst
proveHyp
292
ref
41
ref
refl
325
def
310
ref
44
ref
41
ref
323
ref
263
remove
appTerm
appTerm
262
ref
appTerm
326
def
absTerm
327
def
54
ref
appTerm
328
def
betaConv
329
def
43
ref
11
ref
327
ref
appTerm
330
def
absTerm
331
def
50
ref
appTerm
332
def
betaConv
333
def
nil
68
ref
14
ref
331
ref
appTerm
334
def
nil
cons
cons
335
def
nil
cons
nil
cons
cons
175
ref
subst
sym
nil
68
ref
75
ref
334
remove
appTerm
336
def
nil
cons
337
def
cons
179
ref
cons
nil
cons
cons
338
def
102
ref
subst
338
remove
157
ref
subst
nil
"P"
258
ref
var
339
def
"a"
257
ref
var
340
def
259
ref
261
ref
323
ref
340
ref
varTerm
341
def
appTerm
appTerm
342
def
appTerm
341
ref
appTerm
343
def
absTerm
344
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
260
remove
cons
nil
cons
25
ref
cons
345
def
286
ref
subst
346
def
subst
340
ref
nil
74
ref
343
ref
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
305
ref
340
ref
342
remove
absTerm
341
ref
appTerm
betaConv
appThm
340
ref
341
ref
absTerm
341
ref
appTerm
betaConv
appThm
254
remove
341
remove
refl
appThm
eqMp
347
def
eqMp
absThm
eqMp
nil
68
ref
7
ref
0
ref
258
remove
3
ref
cons
opType
constTerm
348
def
344
remove
appTerm
349
def
nil
cons
350
def
cons
351
def
88
ref
241
ref
"r"
22
ref
var
352
def
20
ref
30
ref
6
ref
39
ref
12
ref
41
ref
352
ref
varTerm
353
def
appTerm
354
def
61
ref
appTerm
355
def
absTerm
356
def
appTerm
absTerm
357
def
appTerm
358
def
appTerm
41
ref
323
ref
261
ref
353
ref
appTerm
appTerm
appTerm
353
ref
appTerm
359
def
appTerm
360
def
absTerm
361
def
appTerm
362
def
nil
cons
363
def
cons
nil
cons
cons
nil
cons
cons
157
ref
subst
proveHyp
nil
201
ref
361
ref
nil
cons
cons
364
def
nil
cons
nil
cons
cons
26
ref
286
ref
subst
subst
352
ref
nil
74
ref
360
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
128
ref
65
remove
353
ref
appTerm
365
def
betaConv
appThm
359
ref
refl
366
def
appThm
128
ref
352
ref
359
ref
absTerm
353
ref
appTerm
betaConv
appThm
352
ref
365
remove
absTerm
353
ref
appTerm
betaConv
appThm
253
remove
353
ref
refl
appThm
eqMp
sym
eqMp
eqMp
absThm
eqMp
367
def
eqMp
nil
68
ref
45
ref
349
remove
appTerm
368
def
362
remove
appTerm
369
def
nil
cons
370
def
cons
179
ref
cons
nil
cons
cons
371
def
146
ref
subst
proveHyp
371
ref
102
ref
subst
371
remove
157
ref
subst
45
ref
refl
372
def
348
ref
refl
340
ref
343
remove
refl
absThm
appThm
appThm
373
def
242
ref
352
ref
nil
68
ref
358
ref
nil
cons
cons
88
ref
359
ref
nil
cons
cons
nil
cons
374
def
cons
nil
cons
cons
nil
68
ref
72
ref
81
ref
appTerm
375
def
nil
cons
376
def
cons
377
def
88
ref
20
ref
293
ref
appTerm
45
ref
"Data.Bool.\\/"
const
19
remove
constTerm
378
def
71
ref
appTerm
75
ref
90
ref
appTerm
379
def
appTerm
appTerm
378
ref
76
remove
appTerm
380
def
90
ref
appTerm
appTerm
appTerm
nil
cons
381
def
cons
nil
cons
382
def
cons
nil
cons
cons
383
def
102
ref
subst
383
remove
157
ref
subst
20
ref
"_554"
2
ref
var
384
def
20
ref
20
ref
384
remove
varTerm
385
def
appTerm
90
ref
appTerm
appTerm
45
ref
378
ref
385
ref
appTerm
379
ref
appTerm
appTerm
378
ref
75
ref
385
remove
appTerm
appTerm
90
ref
appTerm
appTerm
appTerm
absTerm
386
def
71
ref
appTerm
387
def
appTerm
refl
388
def
386
ref
81
ref
appTerm
betaConv
appThm
128
ref
387
remove
betaConv
appThm
389
def
20
ref
20
ref
81
ref
appTerm
390
def
90
ref
appTerm
appTerm
45
ref
378
ref
81
ref
appTerm
391
def
379
ref
appTerm
appTerm
378
ref
75
ref
81
ref
appTerm
392
def
appTerm
393
def
90
ref
appTerm
appTerm
appTerm
refl
appThm
trans
386
remove
refl
394
def
375
remove
assume
395
def
appThm
eqMp
sym
128
ref
122
ref
74
ref
20
ref
390
remove
79
ref
appTerm
appTerm
82
remove
appTerm
absTerm
396
def
79
ref
appTerm
397
def
betaConv
nil
86
ref
396
ref
appTerm
398
def
axiom
nil
68
ref
398
remove
nil
cons
cons
88
ref
397
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
396
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
399
def
subst
appThm
372
ref
nil
74
ref
379
ref
nil
cons
400
def
cons
nil
cons
nil
cons
cons
401
def
74
ref
20
ref
391
ref
79
ref
appTerm
appTerm
79
ref
appTerm
absTerm
402
def
79
ref
appTerm
403
def
betaConv
nil
86
ref
402
ref
appTerm
404
def
axiom
nil
68
ref
404
remove
nil
cons
cons
88
ref
403
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
402
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
405
def
subst
406
def
appThm
378
ref
refl
407
def
nil
20
ref
392
ref
appTerm
107
ref
appTerm
axiom
408
def
appThm
409
def
97
ref
appThm
122
ref
74
ref
20
ref
378
ref
107
ref
appTerm
410
def
79
ref
appTerm
appTerm
107
ref
appTerm
absTerm
411
def
79
ref
appTerm
412
def
betaConv
nil
86
ref
411
ref
appTerm
413
def
axiom
nil
68
ref
413
remove
nil
cons
cons
88
ref
412
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
411
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
414
def
subst
trans
appThm
401
ref
74
ref
20
ref
45
ref
79
ref
appTerm
107
ref
appTerm
appTerm
79
ref
appTerm
absTerm
415
def
79
ref
appTerm
416
def
betaConv
nil
86
ref
415
ref
appTerm
417
def
axiom
nil
68
ref
417
remove
nil
cons
cons
88
ref
416
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
415
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
418
def
subst
trans
appThm
nil
149
ref
400
remove
cons
nil
cons
nil
cons
cons
174
ref
subst
419
def
trans
sym
118
ref
eqMp
eqMp
eqMp
nil
125
ref
376
ref
cons
420
def
126
ref
381
ref
cons
nil
cons
421
def
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
nil
68
ref
72
remove
107
ref
appTerm
422
def
nil
cons
423
def
cons
424
def
382
remove
cons
nil
cons
cons
425
def
102
ref
subst
425
remove
157
ref
subst
388
remove
"_552"
2
ref
var
426
def
20
ref
20
ref
426
remove
varTerm
427
def
appTerm
90
ref
appTerm
appTerm
45
ref
378
ref
427
ref
appTerm
379
ref
appTerm
appTerm
378
ref
75
ref
427
remove
appTerm
appTerm
90
ref
appTerm
appTerm
appTerm
absTerm
107
ref
appTerm
betaConv
appThm
389
remove
20
ref
20
ref
107
ref
appTerm
428
def
90
ref
appTerm
appTerm
45
ref
410
ref
379
ref
appTerm
appTerm
378
ref
75
ref
107
ref
appTerm
429
def
appTerm
430
def
90
ref
appTerm
appTerm
appTerm
refl
appThm
trans
394
remove
422
remove
assume
431
def
appThm
eqMp
sym
128
ref
122
ref
74
ref
20
ref
428
remove
79
ref
appTerm
appTerm
79
ref
appTerm
absTerm
432
def
79
ref
appTerm
433
def
betaConv
nil
86
ref
432
ref
appTerm
434
def
axiom
nil
68
ref
434
remove
nil
cons
cons
88
ref
433
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
432
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
435
def
subst
appThm
372
ref
401
remove
414
ref
subst
436
def
appThm
407
ref
nil
20
ref
429
ref
appTerm
81
ref
appTerm
axiom
437
def
appThm
438
def
97
remove
appThm
122
ref
405
ref
subst
trans
appThm
122
ref
74
ref
20
ref
45
ref
107
ref
appTerm
439
def
79
ref
appTerm
appTerm
79
ref
appTerm
absTerm
440
def
79
ref
appTerm
441
def
betaConv
nil
86
ref
440
ref
appTerm
442
def
axiom
nil
68
ref
442
remove
nil
cons
cons
88
ref
441
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
440
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
443
def
subst
444
def
trans
appThm
nil
149
ref
121
ref
cons
nil
cons
445
def
nil
cons
cons
174
ref
subst
trans
sym
118
ref
eqMp
eqMp
eqMp
nil
125
ref
423
remove
cons
446
def
421
remove
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
74
ref
378
ref
117
ref
appTerm
116
remove
81
ref
appTerm
appTerm
absTerm
447
def
71
ref
appTerm
448
def
betaConv
nil
86
ref
447
ref
appTerm
449
def
axiom
450
def
nil
68
ref
449
remove
nil
cons
cons
451
def
88
ref
448
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
447
ref
nil
cons
cons
452
def
170
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
453
def
nil
446
ref
126
ref
376
remove
cons
454
def
"R"
2
ref
var
455
def
381
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
68
ref
78
ref
131
ref
appTerm
456
def
455
ref
varTerm
457
def
appTerm
458
def
nil
cons
cons
88
ref
457
ref
nil
cons
459
def
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
nil
68
ref
78
ref
129
ref
appTerm
460
def
457
ref
appTerm
nil
cons
cons
88
ref
78
ref
458
remove
appTerm
457
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
"r"
2
ref
var
461
def
78
ref
460
remove
461
ref
varTerm
462
def
appTerm
appTerm
463
def
78
ref
456
remove
462
ref
appTerm
appTerm
462
ref
appTerm
appTerm
absTerm
464
def
457
remove
appTerm
465
def
betaConv
20
ref
378
ref
129
ref
appTerm
466
def
131
ref
appTerm
467
def
appTerm
refl
88
ref
86
ref
461
ref
463
remove
78
ref
300
remove
462
ref
appTerm
appTerm
462
ref
appTerm
468
def
appTerm
absTerm
appTerm
absTerm
131
ref
appTerm
betaConv
appThm
110
remove
466
remove
appTerm
refl
68
ref
88
ref
86
ref
461
ref
78
ref
89
remove
462
ref
appTerm
appTerm
468
remove
appTerm
absTerm
appTerm
absTerm
absTerm
469
def
129
remove
appTerm
betaConv
appThm
nil
99
remove
378
ref
appTerm
469
remove
appTerm
axiom
138
remove
appThm
eqMp
134
remove
appThm
eqMp
467
remove
assume
eqMp
nil
68
ref
86
ref
464
ref
appTerm
nil
cons
cons
88
ref
465
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
464
remove
nil
cons
cons
149
ref
459
remove
cons
nil
cons
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
eqMp
eqMp
470
def
subst
proveHyp
proveHyp
proveHyp
471
def
subst
372
ref
407
ref
203
ref
6
ref
39
ref
refl
472
def
12
ref
355
ref
refl
absThm
appThm
absThm
appThm
appThm
75
ref
359
ref
appTerm
473
def
refl
474
def
appThm
appThm
407
ref
nil
5
ref
357
ref
nil
cons
475
def
cons
nil
cons
nil
cons
cons
240
remove
subst
243
ref
6
ref
202
ref
357
remove
48
ref
appTerm
betaConv
476
def
appThm
nil
244
ref
356
ref
nil
cons
477
def
cons
nil
cons
nil
cons
cons
248
remove
subst
249
ref
12
ref
202
ref
356
remove
52
ref
appTerm
betaConv
478
def
appThm
absThm
appThm
trans
trans
absThm
appThm
trans
appThm
366
ref
appThm
appThm
trans
absThm
appThm
appThm
373
ref
128
ref
242
ref
352
ref
372
ref
352
ref
378
ref
358
remove
appTerm
473
ref
appTerm
absTerm
479
def
353
ref
appTerm
betaConv
480
def
appThm
352
ref
378
ref
14
ref
6
ref
11
ref
12
ref
75
ref
355
ref
appTerm
481
def
absTerm
482
def
appTerm
absTerm
483
def
appTerm
appTerm
359
ref
appTerm
absTerm
484
def
353
ref
appTerm
betaConv
485
def
appThm
absThm
appThm
appThm
372
ref
242
ref
352
ref
480
remove
absThm
appThm
appThm
242
ref
352
ref
485
remove
absThm
appThm
appThm
appThm
nil
66
remove
479
remove
nil
cons
cons
"q"
40
remove
var
484
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
26
ref
"q"
4
remove
var
486
def
20
ref
14
ref
43
ref
45
ref
228
ref
appTerm
487
def
486
ref
varTerm
488
def
50
ref
appTerm
489
def
appTerm
absTerm
appTerm
appTerm
45
ref
14
ref
229
remove
appTerm
490
def
appTerm
14
ref
43
ref
489
ref
absTerm
491
def
appTerm
appTerm
appTerm
absTerm
492
def
488
ref
appTerm
493
def
betaConv
32
ref
234
ref
492
ref
appTerm
494
def
absTerm
495
def
33
ref
appTerm
496
def
betaConv
nil
234
ref
495
ref
appTerm
497
def
axiom
nil
68
ref
497
remove
nil
cons
cons
88
ref
496
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
236
ref
237
ref
495
remove
nil
cons
cons
239
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
494
remove
nil
cons
cons
88
ref
493
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
236
ref
237
ref
492
remove
nil
cons
cons
238
remove
488
ref
nil
cons
cons
nil
cons
498
def
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
499
def
subst
subst
eqMp
appThm
373
ref
372
ref
242
ref
352
ref
128
ref
407
ref
203
ref
6
ref
476
ref
absThm
appThm
appThm
474
ref
appThm
appThm
203
ref
6
ref
407
ref
476
remove
appThm
474
ref
appThm
absThm
appThm
appThm
nil
32
ref
475
remove
cons
88
ref
473
ref
nil
cons
cons
nil
cons
500
def
cons
nil
cons
cons
88
ref
20
ref
378
ref
230
ref
appTerm
90
ref
appTerm
appTerm
30
ref
43
ref
378
ref
228
ref
appTerm
90
ref
appTerm
absTerm
501
def
appTerm
appTerm
absTerm
502
def
90
ref
appTerm
503
def
betaConv
32
ref
86
ref
502
ref
appTerm
504
def
absTerm
505
def
33
ref
appTerm
506
def
betaConv
nil
234
ref
505
ref
appTerm
507
def
axiom
nil
68
ref
507
remove
nil
cons
cons
88
ref
506
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
236
ref
237
ref
505
remove
nil
cons
cons
239
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
504
remove
nil
cons
cons
88
ref
503
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
502
remove
nil
cons
cons
445
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
508
def
subst
eqMp
203
ref
6
ref
128
ref
407
ref
472
ref
12
ref
478
ref
absThm
appThm
appThm
474
ref
appThm
appThm
472
ref
12
ref
407
ref
478
remove
appThm
474
remove
appThm
absThm
appThm
appThm
nil
"p"
9
ref
var
509
def
477
remove
cons
500
remove
cons
nil
cons
cons
247
ref
508
remove
subst
subst
eqMp
absThm
appThm
trans
absThm
appThm
128
ref
242
ref
352
ref
203
ref
6
ref
352
ref
6
ref
39
ref
12
ref
378
ref
355
remove
appTerm
473
ref
appTerm
absTerm
appTerm
absTerm
510
def
absTerm
511
def
353
ref
appTerm
betaConv
512
def
48
ref
refl
513
def
appThm
510
ref
48
ref
appTerm
betaConv
trans
absThm
appThm
absThm
appThm
appThm
29
ref
0
ref
0
ref
0
ref
22
ref
35
ref
cons
opType
514
def
3
ref
cons
opType
515
def
3
ref
cons
opType
516
def
constTerm
517
def
refl
518
def
"f"
514
ref
var
519
def
242
ref
352
ref
512
remove
519
ref
varTerm
520
def
353
ref
appTerm
521
def
refl
appThm
510
remove
521
ref
appTerm
betaConv
trans
absThm
appThm
absThm
appThm
appThm
nil
"r"
0
ref
22
ref
46
remove
cons
opType
var
511
remove
nil
cons
cons
nil
cons
nil
cons
cons
"B"
35
ref
cons
24
ref
cons
25
ref
cons
352
ref
20
ref
14
ref
43
ref
39
ref
44
ref
353
ref
50
ref
appTerm
522
def
54
ref
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
29
ref
218
remove
constTerm
"f"
209
ref
var
523
def
14
ref
43
ref
522
remove
523
ref
varTerm
524
def
50
ref
appTerm
525
def
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
526
def
353
ref
appTerm
527
def
betaConv
nil
241
ref
526
ref
appTerm
528
def
axiom
nil
68
ref
528
remove
nil
cons
cons
88
ref
527
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
24
ref
201
ref
526
remove
nil
cons
cons
38
ref
353
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
529
def
subst
subst
eqMp
518
ref
519
ref
128
ref
242
ref
352
ref
472
ref
12
ref
352
ref
12
ref
378
ref
354
ref
59
ref
521
remove
appTerm
530
def
52
ref
appTerm
appTerm
appTerm
473
ref
appTerm
absTerm
531
def
absTerm
532
def
353
ref
appTerm
betaConv
533
def
52
ref
refl
534
def
appThm
531
ref
52
ref
appTerm
betaConv
trans
absThm
appThm
absThm
appThm
appThm
29
remove
0
ref
0
ref
0
ref
22
ref
207
ref
cons
opType
535
def
3
ref
cons
opType
536
def
3
remove
cons
opType
537
def
constTerm
538
def
refl
539
def
"f"
535
ref
var
540
def
242
ref
352
ref
533
remove
540
ref
varTerm
541
def
353
ref
appTerm
542
def
refl
appThm
531
remove
542
ref
appTerm
betaConv
trans
absThm
appThm
absThm
appThm
appThm
nil
"r"
0
ref
22
ref
21
ref
cons
opType
var
532
remove
nil
cons
cons
nil
cons
nil
cons
cons
"B"
207
ref
cons
24
ref
cons
25
ref
cons
529
remove
subst
subst
eqMp
absThm
appThm
trans
trans
appThm
241
ref
484
remove
appTerm
543
def
refl
544
def
appThm
128
ref
372
ref
518
ref
519
ref
519
ref
538
ref
540
ref
241
ref
352
ref
378
ref
354
ref
530
ref
542
remove
appTerm
appTerm
appTerm
473
ref
appTerm
absTerm
appTerm
545
def
absTerm
546
def
appTerm
absTerm
547
def
520
ref
appTerm
betaConv
548
def
absThm
appThm
appThm
544
ref
appThm
appThm
518
ref
519
ref
372
ref
548
remove
appThm
544
ref
appThm
absThm
appThm
appThm
nil
"p"
515
ref
var
547
remove
nil
cons
cons
88
ref
543
ref
nil
cons
549
def
cons
nil
cons
550
def
cons
nil
cons
cons
"A"
514
ref
nil
cons
cons
nil
cons
551
def
25
ref
cons
552
def
88
ref
20
ref
45
ref
230
remove
appTerm
90
ref
appTerm
appTerm
30
ref
43
ref
487
remove
90
ref
appTerm
absTerm
appTerm
appTerm
absTerm
553
def
90
ref
appTerm
554
def
betaConv
32
ref
86
ref
553
ref
appTerm
555
def
absTerm
556
def
33
ref
appTerm
557
def
betaConv
nil
234
ref
556
ref
appTerm
558
def
axiom
nil
68
ref
558
remove
nil
cons
cons
88
ref
557
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
236
ref
237
ref
556
remove
nil
cons
cons
239
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
555
remove
nil
cons
cons
88
ref
554
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
553
remove
nil
cons
cons
445
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
559
def
subst
subst
eqMp
518
ref
519
ref
128
ref
372
ref
539
ref
540
ref
546
ref
541
ref
appTerm
betaConv
560
def
absThm
appThm
appThm
544
ref
appThm
appThm
539
ref
540
ref
372
ref
560
remove
appThm
544
remove
appThm
absThm
appThm
appThm
nil
"p"
536
ref
var
546
remove
nil
cons
cons
550
remove
cons
nil
cons
cons
"A"
535
ref
nil
cons
cons
nil
cons
561
def
25
ref
cons
562
def
559
remove
subst
subst
eqMp
absThm
appThm
trans
trans
appThm
128
ref
373
ref
518
ref
519
ref
519
ref
538
ref
540
ref
45
ref
545
remove
appTerm
543
ref
appTerm
563
def
absTerm
564
def
appTerm
absTerm
565
def
520
ref
appTerm
betaConv
566
def
absThm
appThm
appThm
appThm
518
ref
519
ref
373
ref
566
remove
appThm
absThm
appThm
appThm
nil
"q"
515
ref
var
565
remove
nil
cons
cons
351
remove
nil
cons
567
def
cons
nil
cons
cons
552
ref
486
ref
20
ref
92
ref
30
ref
491
remove
appTerm
appTerm
appTerm
30
ref
43
ref
92
remove
489
remove
appTerm
absTerm
appTerm
appTerm
absTerm
568
def
488
remove
appTerm
569
def
betaConv
68
ref
234
ref
568
ref
appTerm
570
def
absTerm
571
def
71
ref
appTerm
572
def
betaConv
nil
86
ref
571
ref
appTerm
573
def
axiom
nil
68
ref
573
remove
nil
cons
cons
88
ref
572
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
571
remove
nil
cons
cons
170
remove
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
570
remove
nil
cons
cons
88
ref
569
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
236
ref
237
ref
568
remove
nil
cons
cons
498
remove
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
574
def
subst
subst
eqMp
518
remove
519
ref
128
ref
373
ref
539
ref
540
ref
564
ref
541
remove
appTerm
betaConv
575
def
absThm
appThm
appThm
appThm
539
remove
540
ref
373
remove
575
remove
appThm
absThm
appThm
appThm
nil
"q"
536
ref
var
564
remove
nil
cons
cons
567
remove
cons
nil
cons
cons
562
ref
574
remove
subst
subst
eqMp
absThm
appThm
trans
trans
trans
trans
369
remove
assume
eqMp
nil
68
ref
517
remove
519
ref
538
remove
540
remove
368
ref
563
remove
appTerm
absTerm
576
def
appTerm
577
def
absTerm
578
def
appTerm
579
def
nil
cons
cons
179
ref
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
"P"
515
remove
var
580
def
519
ref
78
ref
578
ref
520
remove
appTerm
581
def
appTerm
81
ref
appTerm
582
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
552
remove
286
ref
subst
subst
519
remove
nil
74
ref
582
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
nil
68
ref
581
ref
nil
cons
583
def
cons
179
ref
cons
nil
cons
cons
584
def
102
ref
subst
584
remove
157
ref
subst
581
ref
betaConv
581
remove
assume
eqMp
nil
68
ref
577
ref
nil
cons
cons
179
ref
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
"P"
536
remove
var
585
def
"f'"
535
ref
var
586
def
78
ref
576
ref
586
ref
varTerm
587
def
appTerm
588
def
appTerm
81
ref
appTerm
589
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
562
remove
286
ref
subst
subst
586
remove
nil
74
ref
589
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
nil
68
ref
588
ref
nil
cons
590
def
cons
179
ref
cons
nil
cons
cons
591
def
102
ref
subst
591
remove
157
ref
subst
588
ref
betaConv
588
remove
assume
eqMp
nil
68
ref
368
remove
45
ref
241
ref
352
ref
378
ref
354
remove
530
remove
587
remove
353
remove
appTerm
appTerm
appTerm
appTerm
473
remove
appTerm
absTerm
appTerm
592
def
appTerm
543
remove
appTerm
593
def
appTerm
nil
cons
594
def
cons
179
ref
cons
nil
cons
cons
595
def
146
ref
subst
proveHyp
595
ref
102
ref
subst
595
remove
157
ref
subst
nil
5
ref
331
remove
nil
cons
cons
596
def
nil
cons
nil
cons
cons
128
ref
202
ref
243
ref
225
remove
appThm
appThm
appThm
30
ref
226
remove
appTerm
refl
appThm
sym
227
remove
32
ref
20
ref
75
ref
490
ref
appTerm
appTerm
30
ref
231
remove
appTerm
appTerm
absTerm
597
def
33
ref
appTerm
598
def
betaConv
nil
234
ref
597
ref
appTerm
599
def
axiom
nil
68
ref
599
remove
nil
cons
cons
88
ref
598
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
236
ref
237
ref
597
remove
nil
cons
cons
239
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
subst
eqMp
600
def
subst
203
ref
43
ref
202
ref
333
remove
appThm
nil
244
ref
327
remove
nil
cons
cons
601
def
nil
cons
nil
cons
cons
247
ref
600
remove
subst
subst
472
ref
44
ref
202
ref
329
remove
appThm
absThm
appThm
trans
trans
absThm
appThm
trans
336
remove
assume
eqMp
nil
68
ref
30
ref
43
ref
39
ref
44
ref
75
ref
326
ref
appTerm
602
def
absTerm
603
def
appTerm
604
def
absTerm
605
def
appTerm
606
def
nil
cons
cons
179
ref
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
5
ref
43
ref
78
ref
605
ref
50
ref
appTerm
607
def
appTerm
81
ref
appTerm
608
def
absTerm
609
def
nil
cons
cons
nil
cons
nil
cons
cons
286
ref
subst
43
ref
nil
74
ref
608
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
nil
68
ref
607
ref
nil
cons
610
def
cons
179
ref
cons
nil
cons
cons
611
def
102
ref
subst
611
remove
157
ref
subst
607
ref
betaConv
607
remove
assume
eqMp
nil
68
ref
604
ref
nil
cons
cons
179
ref
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
244
ref
44
ref
78
ref
603
ref
54
ref
appTerm
612
def
appTerm
81
ref
appTerm
613
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
287
ref
subst
44
ref
nil
74
ref
613
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
nil
68
ref
612
ref
nil
cons
614
def
cons
179
ref
cons
nil
cons
cons
615
def
102
ref
subst
615
remove
157
ref
subst
612
ref
betaConv
612
remove
assume
eqMp
nil
68
ref
602
ref
nil
cons
616
def
cons
179
ref
cons
nil
cons
cons
617
def
146
ref
subst
proveHyp
617
ref
102
ref
subst
617
remove
157
ref
subst
nil
38
ref
262
ref
nil
cons
618
def
cons
nil
cons
nil
cons
cons
185
remove
subst
nil
68
ref
41
ref
262
ref
appTerm
262
remove
appTerm
nil
cons
cons
88
ref
326
remove
nil
cons
619
def
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
"_1194"
8
ref
var
620
def
54
ref
nil
cons
621
def
cons
"_1193"
1
ref
var
622
def
50
ref
nil
cons
623
def
cons
"_1192"
22
ref
var
624
def
618
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
"b"
2
ref
var
625
def
75
ref
41
ref
624
remove
varTerm
626
def
appTerm
627
def
59
remove
622
remove
varTerm
628
def
appTerm
629
def
620
remove
varTerm
630
def
appTerm
appTerm
631
def
appTerm
nil
cons
632
def
cons
"a"
2
ref
var
633
def
41
ref
323
ref
261
ref
626
ref
appTerm
appTerm
appTerm
626
ref
appTerm
634
def
nil
cons
635
def
cons
nil
cons
cons
nil
cons
cons
nil
68
ref
20
ref
633
ref
varTerm
636
def
appTerm
637
def
81
ref
appTerm
638
def
nil
cons
639
def
cons
640
def
88
ref
20
ref
378
ref
636
ref
appTerm
641
def
625
ref
varTerm
642
def
appTerm
643
def
appTerm
78
ref
75
ref
642
ref
appTerm
644
def
appTerm
645
def
636
ref
appTerm
appTerm
nil
cons
646
def
cons
nil
cons
647
def
cons
nil
cons
cons
648
def
102
ref
subst
648
remove
157
ref
subst
20
ref
"_606"
2
ref
var
649
def
20
ref
378
ref
649
remove
varTerm
650
def
appTerm
642
ref
appTerm
appTerm
645
ref
650
remove
appTerm
appTerm
absTerm
651
def
636
ref
appTerm
652
def
appTerm
refl
653
def
651
ref
81
ref
appTerm
betaConv
appThm
128
ref
652
remove
betaConv
appThm
654
def
20
ref
391
ref
642
ref
appTerm
655
def
appTerm
645
ref
81
ref
appTerm
appTerm
refl
appThm
trans
651
remove
refl
656
def
638
remove
assume
657
def
appThm
eqMp
sym
128
ref
nil
74
ref
642
ref
nil
cons
658
def
cons
nil
cons
nil
cons
cons
659
def
405
ref
subst
660
def
appThm
nil
74
ref
644
ref
nil
cons
661
def
cons
nil
cons
nil
cons
cons
662
def
165
remove
subst
659
ref
169
ref
subst
trans
appThm
nil
149
ref
658
remove
cons
nil
cons
nil
cons
cons
174
ref
subst
trans
sym
118
ref
eqMp
eqMp
eqMp
nil
125
ref
639
ref
cons
663
def
126
ref
646
ref
cons
nil
cons
664
def
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
nil
68
ref
637
remove
107
ref
appTerm
665
def
nil
cons
666
def
cons
667
def
647
remove
cons
nil
cons
cons
668
def
102
ref
subst
668
remove
157
ref
subst
653
remove
"_604"
2
ref
var
669
def
20
ref
378
ref
669
remove
varTerm
670
def
appTerm
642
ref
appTerm
appTerm
645
ref
670
remove
appTerm
appTerm
absTerm
107
ref
appTerm
betaConv
appThm
654
remove
20
ref
410
ref
642
ref
appTerm
671
def
appTerm
645
remove
107
ref
appTerm
appTerm
refl
appThm
trans
656
remove
665
remove
assume
672
def
appThm
eqMp
sym
128
ref
659
remove
414
ref
subst
673
def
appThm
662
ref
74
ref
20
ref
80
remove
107
ref
appTerm
appTerm
107
ref
appTerm
absTerm
674
def
79
ref
appTerm
675
def
betaConv
nil
86
ref
674
ref
appTerm
676
def
axiom
nil
68
ref
676
remove
nil
cons
cons
88
ref
675
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
674
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
subst
appThm
nil
74
ref
107
ref
nil
cons
cons
nil
cons
nil
cons
cons
677
def
435
remove
subst
678
def
trans
sym
118
ref
eqMp
eqMp
eqMp
nil
125
ref
666
remove
cons
679
def
664
remove
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
447
remove
636
ref
appTerm
680
def
betaConv
450
remove
nil
451
remove
88
ref
680
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
452
remove
149
ref
636
ref
nil
cons
681
def
cons
nil
cons
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
682
def
nil
679
ref
126
ref
639
remove
cons
683
def
455
ref
646
remove
cons
nil
cons
cons
cons
nil
cons
cons
470
ref
subst
proveHyp
proveHyp
proveHyp
684
def
subst
292
ref
nil
633
ref
631
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
74
ref
681
remove
cons
nil
cons
nil
cons
cons
169
remove
subst
685
def
subst
appThm
634
ref
refl
appThm
trans
nil
88
ref
635
remove
cons
68
ref
632
remove
cons
nil
cons
cons
nil
cons
cons
nil
"t2"
2
ref
var
686
def
121
ref
cons
"t1"
2
ref
var
687
def
114
ref
cons
nil
cons
cons
688
def
nil
cons
cons
686
ref
20
ref
378
ref
687
ref
varTerm
689
def
appTerm
690
def
686
ref
varTerm
691
def
appTerm
692
def
appTerm
378
ref
691
ref
appTerm
693
def
689
ref
appTerm
appTerm
absTerm
694
def
691
ref
appTerm
695
def
betaConv
687
ref
86
ref
694
ref
appTerm
696
def
absTerm
697
def
689
ref
appTerm
698
def
betaConv
nil
86
ref
697
ref
appTerm
699
def
axiom
nil
68
ref
699
remove
nil
cons
cons
88
ref
698
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
697
remove
nil
cons
cons
149
ref
689
ref
nil
cons
cons
nil
cons
700
def
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
696
remove
nil
cons
cons
88
ref
695
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
694
remove
nil
cons
cons
149
ref
691
ref
nil
cons
cons
nil
cons
701
def
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
subst
702
def
subst
12
ref
378
ref
75
ref
627
ref
629
remove
52
ref
appTerm
appTerm
appTerm
appTerm
634
ref
appTerm
absTerm
703
def
630
ref
appTerm
704
def
betaConv
6
ref
11
ref
12
ref
378
ref
75
ref
627
remove
61
ref
appTerm
appTerm
appTerm
634
remove
appTerm
absTerm
appTerm
absTerm
705
def
628
ref
appTerm
706
def
betaConv
352
ref
14
ref
6
ref
11
ref
12
ref
378
ref
481
remove
appTerm
359
remove
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
707
def
626
ref
appTerm
708
def
betaConv
242
remove
352
remove
128
ref
407
ref
243
ref
6
ref
483
ref
48
ref
appTerm
betaConv
709
def
absThm
appThm
appThm
366
ref
appThm
appThm
243
ref
6
ref
407
ref
709
remove
appThm
366
ref
appThm
absThm
appThm
appThm
nil
32
ref
483
remove
nil
cons
cons
374
ref
cons
nil
cons
cons
88
ref
20
ref
378
ref
490
remove
appTerm
90
ref
appTerm
appTerm
14
ref
501
remove
appTerm
appTerm
absTerm
710
def
90
ref
appTerm
711
def
betaConv
32
ref
86
ref
710
ref
appTerm
712
def
absTerm
713
def
33
ref
appTerm
714
def
betaConv
nil
234
ref
713
ref
appTerm
715
def
axiom
nil
68
ref
715
remove
nil
cons
cons
88
ref
714
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
236
ref
237
ref
713
remove
nil
cons
cons
239
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
712
remove
nil
cons
cons
88
ref
711
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
710
remove
nil
cons
cons
445
remove
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
716
def
subst
eqMp
243
ref
6
ref
128
ref
407
ref
249
ref
12
ref
482
ref
52
ref
appTerm
betaConv
717
def
absThm
appThm
appThm
366
ref
appThm
appThm
249
ref
12
ref
407
ref
717
remove
appThm
366
remove
appThm
absThm
appThm
appThm
nil
509
ref
482
remove
nil
cons
cons
374
remove
cons
nil
cons
cons
247
ref
716
remove
subst
subst
eqMp
absThm
appThm
trans
absThm
appThm
nil
125
ref
350
remove
cons
126
ref
593
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
303
ref
subst
nil
125
ref
592
remove
nil
cons
cons
126
ref
549
remove
cons
nil
cons
cons
nil
cons
cons
303
ref
subst
proveHyp
eqMp
nil
68
ref
241
remove
707
ref
appTerm
nil
cons
cons
88
ref
708
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
24
ref
201
remove
707
remove
nil
cons
cons
38
ref
626
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
14
ref
705
ref
appTerm
nil
cons
cons
88
ref
706
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
250
ref
5
ref
705
remove
nil
cons
cons
43
ref
628
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
11
ref
703
ref
appTerm
nil
cons
cons
88
ref
704
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
246
ref
244
ref
703
remove
nil
cons
cons
251
ref
630
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
eqMp
eqMp
subst
eqMp
nil
68
ref
619
remove
cons
718
def
179
ref
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
718
remove
nil
cons
nil
cons
cons
194
ref
subst
602
remove
assume
eqMp
eqMp
eqMp
nil
125
ref
616
remove
cons
252
ref
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
125
ref
614
remove
cons
252
ref
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
68
ref
11
ref
251
ref
78
ref
603
ref
251
ref
varTerm
719
def
appTerm
appTerm
81
ref
appTerm
absTerm
appTerm
nil
cons
cons
88
ref
78
ref
604
remove
appTerm
81
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
246
ref
244
ref
603
remove
nil
cons
cons
252
ref
cons
nil
cons
cons
nil
68
ref
14
ref
43
ref
78
ref
154
remove
appTerm
720
def
131
ref
appTerm
absTerm
721
def
appTerm
722
def
nil
cons
723
def
cons
724
def
88
ref
78
ref
30
ref
151
ref
appTerm
725
def
appTerm
726
def
131
ref
appTerm
nil
cons
727
def
cons
nil
cons
cons
nil
cons
cons
728
def
102
ref
subst
728
remove
157
ref
subst
nil
68
ref
725
ref
nil
cons
729
def
cons
730
def
88
ref
131
ref
nil
cons
731
def
cons
nil
cons
732
def
cons
nil
cons
cons
733
def
102
ref
subst
733
remove
157
ref
subst
nil
724
ref
732
ref
cons
nil
cons
cons
734
def
146
ref
subst
88
ref
78
ref
14
ref
43
ref
720
remove
90
ref
appTerm
absTerm
appTerm
appTerm
90
ref
appTerm
absTerm
735
def
131
ref
appTerm
736
def
betaConv
nil
730
remove
88
ref
86
ref
735
ref
appTerm
737
def
nil
cons
738
def
cons
nil
cons
cons
nil
cons
cons
739
def
146
ref
subst
20
ref
725
remove
appTerm
740
def
refl
32
ref
86
ref
88
ref
78
ref
14
ref
43
ref
78
ref
228
remove
appTerm
90
ref
appTerm
absTerm
appTerm
appTerm
90
ref
appTerm
absTerm
appTerm
absTerm
741
def
151
remove
appTerm
betaConv
appThm
nil
31
remove
741
remove
appTerm
axiom
161
remove
appThm
eqMp
742
def
nil
68
ref
740
remove
737
ref
appTerm
nil
cons
cons
88
ref
726
remove
737
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
739
remove
nil
68
ref
293
remove
nil
cons
743
def
cons
88
ref
299
ref
cons
nil
cons
cons
nil
cons
cons
744
def
102
ref
subst
744
remove
157
ref
subst
298
remove
eqMp
nil
125
ref
743
remove
cons
126
ref
299
remove
cons
nil
cons
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
68
ref
738
remove
cons
88
ref
736
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
735
remove
nil
cons
cons
149
ref
731
ref
cons
nil
cons
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
125
ref
729
remove
cons
126
ref
731
remove
cons
nil
cons
745
def
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
nil
125
ref
723
remove
cons
746
def
126
ref
727
remove
cons
nil
cons
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
747
def
subst
eqMp
eqMp
eqMp
nil
125
ref
610
remove
cons
252
ref
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
68
ref
14
ref
609
remove
appTerm
nil
cons
cons
88
ref
78
ref
606
remove
appTerm
81
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
250
ref
5
ref
605
remove
nil
cons
cons
252
ref
cons
nil
cons
cons
747
ref
subst
eqMp
eqMp
eqMp
nil
125
ref
594
remove
cons
252
ref
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
125
ref
590
remove
cons
252
ref
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
68
ref
7
ref
537
remove
constTerm
"x"
535
remove
var
748
def
78
ref
576
ref
748
remove
varTerm
appTerm
appTerm
81
ref
appTerm
absTerm
appTerm
nil
cons
cons
88
ref
78
ref
577
remove
appTerm
81
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
561
remove
585
remove
576
remove
nil
cons
cons
252
ref
cons
nil
cons
cons
747
ref
subst
eqMp
eqMp
eqMp
nil
125
ref
583
remove
cons
252
ref
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
68
ref
7
remove
516
remove
constTerm
"x"
514
remove
var
749
def
78
ref
578
ref
749
remove
varTerm
appTerm
appTerm
81
ref
appTerm
absTerm
appTerm
nil
cons
cons
88
ref
78
ref
579
remove
appTerm
81
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
551
remove
580
remove
578
remove
nil
cons
cons
252
ref
cons
nil
cons
cons
747
ref
subst
eqMp
eqMp
eqMp
nil
125
ref
370
remove
cons
252
ref
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
125
ref
337
remove
cons
252
ref
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
nil
335
remove
88
ref
332
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
250
ref
596
remove
43
ref
623
remove
cons
nil
cons
750
def
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
330
remove
nil
cons
cons
88
ref
328
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
246
ref
601
remove
251
ref
621
ref
cons
nil
cons
751
def
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
752
def
subst
appThm
314
ref
752
remove
subst
appThm
appThm
315
ref
appThm
sym
292
ref
nil
"g"
22
ref
var
318
ref
nil
cons
cons
"f"
22
remove
var
61
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
205
remove
"B"
21
remove
cons
nil
cons
cons
25
ref
cons
"g"
209
remove
var
753
def
20
ref
212
remove
524
ref
appTerm
753
ref
varTerm
754
def
appTerm
755
def
appTerm
14
ref
43
ref
51
ref
525
remove
appTerm
754
ref
50
ref
appTerm
appTerm
absTerm
appTerm
756
def
appTerm
absTerm
757
def
754
ref
appTerm
758
def
betaConv
523
ref
219
ref
757
ref
appTerm
759
def
absTerm
760
def
524
ref
appTerm
761
def
betaConv
220
ref
523
ref
220
remove
753
ref
nil
"y"
2
ref
var
756
ref
nil
cons
cons
149
ref
755
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
171
ref
"y"
1
ref
var
762
def
20
ref
172
ref
762
ref
varTerm
763
def
appTerm
appTerm
47
ref
763
ref
appTerm
764
def
50
ref
appTerm
765
def
appTerm
absTerm
766
def
763
ref
appTerm
767
def
betaConv
43
ref
14
ref
766
ref
appTerm
768
def
absTerm
769
def
50
ref
appTerm
770
def
betaConv
nil
14
ref
769
ref
appTerm
771
def
axiom
nil
68
ref
771
remove
nil
cons
cons
88
ref
770
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
250
ref
5
ref
769
remove
nil
cons
cons
750
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
768
remove
nil
cons
cons
88
ref
767
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
250
ref
5
ref
766
remove
nil
cons
cons
43
ref
763
ref
nil
cons
772
def
cons
nil
cons
773
def
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
subst
subst
absThm
appThm
absThm
appThm
sym
nil
219
ref
523
remove
219
ref
753
remove
20
ref
756
remove
appTerm
755
remove
appTerm
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
68
ref
219
remove
760
ref
appTerm
nil
cons
cons
88
ref
761
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
222
ref
223
ref
760
remove
nil
cons
cons
224
ref
524
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
759
remove
nil
cons
cons
88
ref
758
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
222
remove
223
remove
757
remove
nil
cons
cons
224
remove
754
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
774
def
subst
subst
243
ref
43
ref
nil
"g"
9
ref
var
318
remove
50
ref
appTerm
nil
cons
cons
"f"
9
ref
var
61
ref
50
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
245
remove
206
remove
cons
25
remove
cons
774
remove
subst
subst
249
ref
251
ref
128
ref
310
remove
58
remove
163
ref
appThm
57
remove
50
ref
appTerm
betaConv
trans
311
remove
appThm
56
remove
54
ref
appTerm
betaConv
trans
775
def
subst
163
ref
appThm
15
ref
16
ref
45
ref
47
ref
270
ref
appTerm
48
ref
appTerm
appTerm
51
ref
271
ref
appTerm
52
ref
appTerm
776
def
appTerm
absTerm
absTerm
50
ref
appTerm
betaConv
trans
719
ref
refl
777
def
appThm
16
ref
45
ref
172
ref
48
ref
appTerm
778
def
appTerm
779
def
776
remove
appTerm
absTerm
719
ref
appTerm
betaConv
trans
appThm
314
remove
775
remove
subst
163
ref
appThm
6
ref
12
ref
277
ref
absTerm
absTerm
50
ref
appTerm
betaConv
trans
777
ref
appThm
12
ref
45
ref
172
remove
270
ref
appTerm
780
def
appTerm
781
def
276
ref
appTerm
absTerm
719
ref
appTerm
betaConv
trans
appThm
absThm
appThm
trans
absThm
appThm
trans
appThm
315
remove
appThm
sym
nil
68
ref
14
ref
43
ref
11
ref
251
ref
20
ref
779
remove
51
ref
719
ref
appTerm
782
def
52
ref
appTerm
783
def
appTerm
784
def
appTerm
781
remove
782
remove
271
ref
appTerm
785
def
appTerm
786
def
appTerm
absTerm
appTerm
absTerm
appTerm
787
def
nil
cons
788
def
cons
291
remove
cons
nil
cons
cons
789
def
102
ref
subst
789
remove
157
ref
subst
nil
68
ref
290
ref
cons
790
def
nil
cons
nil
cons
cons
175
ref
subst
sym
nil
68
ref
75
ref
277
ref
appTerm
791
def
nil
cons
792
def
cons
179
ref
cons
nil
cons
cons
793
def
102
ref
subst
793
remove
157
ref
subst
nil
68
ref
75
ref
276
ref
appTerm
794
def
nil
cons
795
def
cons
179
ref
cons
nil
cons
cons
796
def
102
ref
subst
796
remove
157
ref
subst
513
ref
nil
68
ref
49
ref
48
ref
appTerm
797
def
nil
cons
cons
88
ref
53
ref
52
ref
appTerm
798
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
157
ref
subst
proveHyp
534
ref
eqMp
799
def
nil
68
ref
45
ref
797
remove
appTerm
798
remove
appTerm
nil
cons
cons
800
def
88
ref
276
ref
nil
cons
801
def
cons
nil
cons
802
def
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
"_1214"
8
ref
var
803
def
306
ref
cons
"_1213"
1
ref
var
804
def
307
ref
cons
nil
cons
cons
nil
cons
cons
nil
625
ref
378
ref
75
ref
47
ref
804
remove
varTerm
805
def
appTerm
806
def
48
ref
appTerm
807
def
appTerm
808
def
appTerm
809
def
75
ref
51
ref
803
remove
varTerm
810
def
appTerm
811
def
52
ref
appTerm
812
def
appTerm
813
def
appTerm
814
def
nil
cons
cons
633
ref
811
remove
271
ref
appTerm
815
def
nil
cons
816
def
cons
nil
cons
cons
nil
cons
cons
684
ref
subst
292
ref
nil
625
ref
813
remove
nil
cons
817
def
cons
633
ref
808
remove
nil
cons
818
def
cons
nil
cons
cons
nil
cons
cons
nil
640
ref
88
ref
20
ref
75
ref
643
ref
appTerm
appTerm
45
ref
75
ref
636
ref
appTerm
appTerm
644
ref
appTerm
appTerm
nil
cons
819
def
cons
nil
cons
820
def
cons
nil
cons
cons
821
def
102
ref
subst
821
remove
157
ref
subst
20
ref
"_610"
2
ref
var
822
def
20
ref
75
ref
378
ref
822
remove
varTerm
823
def
appTerm
642
ref
appTerm
appTerm
appTerm
45
ref
75
ref
823
remove
appTerm
appTerm
644
ref
appTerm
appTerm
absTerm
824
def
636
ref
appTerm
825
def
appTerm
refl
826
def
824
ref
81
ref
appTerm
betaConv
appThm
128
ref
825
remove
betaConv
appThm
827
def
20
ref
75
ref
655
ref
appTerm
appTerm
45
ref
392
remove
appTerm
644
ref
appTerm
appTerm
refl
appThm
trans
824
remove
refl
828
def
657
ref
appThm
eqMp
sym
128
ref
202
ref
660
ref
appThm
appThm
372
ref
408
ref
appThm
644
ref
refl
829
def
appThm
662
ref
443
ref
subst
trans
appThm
nil
149
ref
661
remove
cons
nil
cons
nil
cons
cons
174
ref
subst
trans
sym
118
ref
eqMp
eqMp
eqMp
nil
663
ref
126
ref
819
ref
cons
nil
cons
830
def
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
nil
667
ref
820
remove
cons
nil
cons
cons
831
def
102
ref
subst
831
remove
157
ref
subst
826
remove
"_608"
2
ref
var
832
def
20
ref
75
ref
378
ref
832
remove
varTerm
833
def
appTerm
642
ref
appTerm
appTerm
appTerm
45
ref
75
ref
833
remove
appTerm
appTerm
644
ref
appTerm
appTerm
absTerm
107
ref
appTerm
betaConv
appThm
827
remove
20
ref
75
ref
671
ref
appTerm
appTerm
45
ref
429
remove
appTerm
644
remove
appTerm
appTerm
refl
appThm
trans
828
remove
672
ref
appThm
eqMp
sym
128
ref
202
ref
673
ref
appThm
437
ref
trans
appThm
372
ref
437
remove
appThm
829
remove
appThm
662
remove
74
ref
20
ref
45
ref
81
ref
appTerm
834
def
79
ref
appTerm
appTerm
81
ref
appTerm
absTerm
835
def
79
ref
appTerm
836
def
betaConv
nil
86
ref
835
ref
appTerm
837
def
axiom
nil
68
ref
837
remove
nil
cons
cons
88
ref
836
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
835
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
838
def
subst
trans
appThm
nil
74
ref
178
ref
cons
nil
cons
nil
cons
cons
399
remove
subst
408
ref
trans
trans
sym
118
ref
eqMp
eqMp
eqMp
nil
679
ref
830
remove
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
682
ref
nil
679
ref
683
ref
455
ref
819
remove
cons
nil
cons
cons
cons
nil
cons
cons
470
ref
subst
proveHyp
proveHyp
proveHyp
839
def
subst
372
ref
nil
633
ref
807
remove
nil
cons
cons
nil
cons
nil
cons
cons
685
ref
subst
appThm
nil
633
ref
812
remove
nil
cons
cons
nil
cons
nil
cons
cons
685
ref
subst
appThm
trans
appThm
815
ref
refl
appThm
trans
809
ref
refl
nil
88
ref
816
ref
cons
840
def
68
ref
817
ref
cons
nil
cons
cons
nil
cons
cons
702
ref
subst
appThm
nil
461
ref
817
ref
cons
840
remove
68
ref
818
ref
cons
nil
cons
cons
cons
nil
cons
cons
128
ref
nil
"t3"
2
ref
var
841
def
462
ref
nil
cons
cons
842
def
688
remove
cons
nil
cons
cons
841
ref
20
ref
690
remove
693
remove
841
ref
varTerm
843
def
appTerm
appTerm
844
def
appTerm
378
ref
692
remove
appTerm
843
ref
appTerm
845
def
appTerm
846
def
absTerm
847
def
843
ref
appTerm
848
def
betaConv
686
ref
86
ref
847
ref
appTerm
849
def
absTerm
850
def
691
ref
appTerm
851
def
betaConv
687
ref
86
ref
850
ref
appTerm
852
def
absTerm
853
def
689
ref
appTerm
854
def
betaConv
86
ref
refl
855
def
687
ref
855
ref
686
ref
855
remove
841
ref
846
remove
assume
sym
20
ref
845
remove
appTerm
844
remove
appTerm
856
def
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
absThm
appThm
nil
86
ref
687
ref
86
ref
686
ref
86
ref
841
ref
856
remove
absTerm
857
def
appTerm
858
def
absTerm
859
def
appTerm
860
def
absTerm
861
def
appTerm
862
def
axiom
863
def
eqMp
nil
68
ref
86
ref
853
ref
appTerm
nil
cons
cons
88
ref
854
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
853
remove
nil
cons
cons
700
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
852
remove
nil
cons
cons
88
ref
851
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
850
remove
nil
cons
cons
701
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
849
remove
nil
cons
cons
88
ref
848
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
847
remove
nil
cons
cons
149
ref
843
ref
nil
cons
cons
nil
cons
864
def
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
865
def
subst
appThm
nil
842
remove
686
ref
114
remove
cons
687
ref
121
remove
cons
nil
cons
cons
cons
nil
cons
cons
865
remove
subst
appThm
sym
407
ref
702
ref
appThm
462
remove
refl
appThm
eqMp
866
def
subst
trans
nil
687
ref
818
remove
cons
686
ref
817
remove
cons
841
ref
816
remove
cons
nil
cons
cons
cons
nil
cons
cons
857
ref
843
remove
appTerm
867
def
betaConv
859
ref
691
remove
appTerm
868
def
betaConv
861
ref
689
remove
appTerm
869
def
betaConv
863
remove
nil
68
ref
862
remove
nil
cons
cons
88
ref
869
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
861
remove
nil
cons
cons
700
remove
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
860
remove
nil
cons
cons
88
ref
868
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
859
remove
nil
cons
cons
701
remove
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
858
remove
nil
cons
cons
88
ref
867
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
ref
148
ref
857
remove
nil
cons
cons
864
remove
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
870
def
subst
251
ref
45
ref
378
ref
809
remove
75
ref
783
ref
appTerm
871
def
appTerm
appTerm
872
def
806
remove
270
ref
appTerm
873
def
appTerm
appTerm
872
remove
785
ref
appTerm
appTerm
absTerm
874
def
810
ref
appTerm
875
def
betaConv
43
ref
11
ref
251
ref
45
ref
378
ref
378
ref
75
ref
778
ref
appTerm
appTerm
871
ref
appTerm
876
def
appTerm
877
def
780
ref
appTerm
appTerm
877
ref
785
ref
appTerm
appTerm
absTerm
appTerm
absTerm
878
def
805
ref
appTerm
879
def
betaConv
243
ref
43
ref
249
ref
251
ref
nil
633
ref
876
remove
nil
cons
cons
625
ref
780
ref
nil
cons
880
def
cons
"c"
2
ref
var
881
def
785
ref
nil
cons
882
def
cons
nil
cons
cons
cons
nil
cons
cons
nil
640
remove
88
ref
20
ref
641
ref
45
ref
642
ref
appTerm
881
remove
varTerm
883
def
appTerm
884
def
appTerm
appTerm
45
ref
643
remove
appTerm
641
remove
883
ref
appTerm
appTerm
appTerm
nil
cons
885
def
cons
nil
cons
886
def
cons
nil
cons
cons
887
def
102
ref
subst
887
remove
157
ref
subst
20
ref
"_582"
2
ref
var
888
def
20
ref
378
ref
888
remove
varTerm
appTerm
889
def
884
ref
appTerm
appTerm
45
ref
889
ref
642
ref
appTerm
appTerm
889
remove
883
ref
appTerm
appTerm
appTerm
absTerm
890
def
636
remove
appTerm
891
def
appTerm
refl
892
def
890
ref
81
ref
appTerm
betaConv
appThm
128
ref
891
remove
betaConv
appThm
893
def
20
ref
391
ref
884
ref
appTerm
appTerm
45
ref
655
remove
appTerm
391
remove
883
ref
appTerm
appTerm
appTerm
refl
appThm
trans
890
remove
refl
894
def
657
remove
appThm
eqMp
sym
128
ref
nil
74
ref
884
ref
nil
cons
895
def
cons
nil
cons
nil
cons
cons
896
def
405
ref
subst
appThm
372
ref
660
remove
appThm
nil
74
ref
883
ref
nil
cons
cons
nil
cons
nil
cons
cons
897
def
405
remove
subst
appThm
appThm
nil
149
remove
895
remove
cons
nil
cons
nil
cons
cons
174
remove
subst
trans
sym
118
ref
eqMp
eqMp
eqMp
nil
663
remove
126
ref
885
ref
cons
nil
cons
898
def
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
nil
667
remove
886
remove
cons
nil
cons
cons
899
def
102
ref
subst
899
remove
157
ref
subst
892
remove
"_580"
2
ref
var
900
def
20
ref
378
ref
900
remove
varTerm
appTerm
901
def
884
ref
appTerm
appTerm
45
ref
901
ref
642
remove
appTerm
appTerm
901
remove
883
ref
appTerm
appTerm
appTerm
absTerm
107
ref
appTerm
betaConv
appThm
893
remove
20
ref
410
ref
884
remove
appTerm
appTerm
45
ref
671
remove
appTerm
410
remove
883
remove
appTerm
appTerm
appTerm
refl
appThm
trans
894
remove
672
remove
appThm
eqMp
sym
128
ref
896
remove
414
ref
subst
appThm
372
ref
673
remove
appThm
897
remove
414
remove
subst
appThm
677
remove
443
ref
subst
trans
appThm
678
ref
trans
sym
118
ref
eqMp
eqMp
eqMp
nil
679
ref
898
remove
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
682
remove
nil
679
remove
683
remove
455
ref
885
remove
cons
nil
cons
cons
cons
nil
cons
cons
470
ref
subst
proveHyp
proveHyp
proveHyp
subst
absThm
appThm
absThm
appThm
243
ref
43
ref
249
ref
251
ref
nil
68
ref
784
ref
nil
cons
cons
88
ref
786
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
471
remove
subst
372
ref
407
ref
372
ref
47
ref
refl
902
def
163
ref
appThm
513
ref
appThm
appThm
51
ref
refl
903
def
777
remove
appThm
534
ref
appThm
appThm
appThm
nil
68
ref
880
remove
cons
88
ref
882
remove
cons
nil
cons
cons
nil
cons
cons
nil
377
remove
88
ref
20
ref
75
ref
93
remove
appTerm
appTerm
380
remove
379
ref
appTerm
appTerm
nil
cons
904
def
cons
nil
cons
905
def
cons
nil
cons
cons
906
def
102
ref
subst
906
remove
157
ref
subst
20
ref
"_530"
2
ref
var
907
def
20
ref
75
ref
45
ref
907
remove
varTerm
908
def
appTerm
90
ref
appTerm
appTerm
appTerm
378
ref
75
ref
908
remove
appTerm
appTerm
379
ref
appTerm
appTerm
absTerm
909
def
71
remove
appTerm
910
def
appTerm
refl
911
def
909
ref
81
remove
appTerm
betaConv
appThm
128
ref
910
remove
betaConv
appThm
912
def
20
ref
75
ref
834
remove
90
ref
appTerm
appTerm
appTerm
393
remove
379
ref
appTerm
appTerm
refl
appThm
trans
909
remove
refl
913
def
395
remove
appThm
eqMp
sym
128
ref
202
ref
122
remove
838
remove
subst
appThm
408
remove
trans
appThm
409
remove
379
ref
refl
914
def
appThm
436
remove
trans
appThm
678
remove
trans
sym
118
ref
eqMp
eqMp
eqMp
nil
420
remove
126
ref
904
ref
cons
nil
cons
915
def
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
nil
424
remove
905
remove
cons
nil
cons
cons
916
def
102
ref
subst
916
remove
157
ref
subst
911
remove
"_528"
2
remove
var
917
def
20
ref
75
ref
45
ref
917
remove
varTerm
918
def
appTerm
90
ref
appTerm
appTerm
appTerm
378
ref
75
ref
918
remove
appTerm
appTerm
379
ref
appTerm
appTerm
absTerm
107
remove
appTerm
betaConv
appThm
912
remove
20
ref
75
ref
439
remove
90
remove
appTerm
appTerm
appTerm
430
remove
379
remove
appTerm
appTerm
refl
appThm
trans
913
remove
431
remove
appThm
eqMp
sym
128
ref
202
remove
444
remove
appThm
appThm
438
remove
914
remove
appThm
406
remove
trans
appThm
419
remove
trans
sym
118
ref
eqMp
eqMp
eqMp
nil
446
ref
915
remove
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
453
remove
nil
446
remove
454
remove
455
ref
904
remove
cons
nil
cons
cons
cons
nil
cons
cons
470
ref
subst
proveHyp
proveHyp
proveHyp
919
def
subst
appThm
appThm
407
remove
nil
68
ref
778
remove
nil
cons
cons
88
ref
783
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
919
ref
subst
appThm
372
ref
780
ref
refl
appThm
785
ref
refl
appThm
appThm
appThm
trans
absThm
appThm
absThm
appThm
243
ref
43
ref
128
ref
249
ref
251
ref
372
ref
251
ref
378
ref
784
remove
appTerm
378
ref
75
ref
780
remove
appTerm
appTerm
75
ref
785
ref
appTerm
appTerm
appTerm
absTerm
920
def
719
ref
appTerm
betaConv
921
def
appThm
251
ref
877
remove
786
remove
appTerm
absTerm
922
def
719
ref
appTerm
betaConv
923
def
appThm
absThm
appThm
appThm
372
ref
249
ref
251
ref
921
remove
absThm
appThm
appThm
249
remove
251
ref
923
remove
absThm
appThm
appThm
appThm
nil
509
ref
920
ref
nil
cons
cons
"q"
9
ref
var
922
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
247
ref
499
ref
subst
subst
eqMp
absThm
appThm
128
ref
243
ref
43
ref
372
ref
43
ref
11
ref
920
remove
appTerm
absTerm
924
def
50
ref
appTerm
betaConv
925
def
appThm
43
ref
11
ref
922
remove
appTerm
absTerm
926
def
50
ref
appTerm
betaConv
927
def
appThm
absThm
appThm
appThm
372
ref
243
ref
43
ref
925
remove
absThm
appThm
appThm
243
remove
43
ref
927
remove
absThm
appThm
appThm
appThm
nil
32
ref
924
ref
nil
cons
cons
486
remove
926
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
499
remove
subst
eqMp
trans
trans
787
remove
assume
eqMp
nil
125
ref
14
ref
924
remove
appTerm
nil
cons
cons
126
ref
14
ref
926
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
303
ref
subst
proveHyp
eqMp
928
def
nil
68
ref
14
ref
878
ref
appTerm
nil
cons
cons
929
def
88
ref
879
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
250
ref
5
ref
878
ref
nil
cons
cons
930
def
43
ref
805
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
11
ref
874
ref
appTerm
nil
cons
cons
88
ref
875
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
246
ref
244
ref
874
remove
nil
cons
cons
251
ref
810
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
125
ref
378
ref
814
remove
appTerm
931
def
873
remove
appTerm
nil
cons
cons
126
ref
931
remove
815
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
303
ref
subst
proveHyp
eqMp
eqMp
eqMp
subst
eqMp
nil
68
ref
801
ref
cons
932
def
179
ref
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
932
remove
nil
cons
nil
cons
cons
194
ref
subst
794
remove
assume
eqMp
eqMp
eqMp
nil
125
ref
795
ref
cons
252
ref
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
nil
68
ref
75
ref
274
ref
appTerm
933
def
nil
cons
934
def
cons
179
ref
cons
nil
cons
cons
935
def
102
ref
subst
935
remove
157
ref
subst
799
remove
nil
800
remove
88
ref
274
ref
nil
cons
936
def
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
"_1210"
8
ref
var
937
def
306
ref
cons
"_1209"
1
ref
var
938
def
307
remove
cons
nil
cons
cons
nil
cons
cons
nil
625
ref
378
ref
75
ref
47
ref
938
remove
varTerm
939
def
appTerm
940
def
48
ref
appTerm
941
def
appTerm
942
def
appTerm
943
def
75
ref
51
ref
937
remove
varTerm
944
def
appTerm
945
def
52
ref
appTerm
946
def
appTerm
947
def
appTerm
948
def
nil
cons
cons
633
ref
940
remove
270
ref
appTerm
949
def
nil
cons
950
def
cons
nil
cons
cons
nil
cons
cons
684
remove
subst
292
ref
nil
625
remove
947
remove
nil
cons
951
def
cons
633
ref
942
remove
nil
cons
952
def
cons
nil
cons
cons
nil
cons
cons
839
remove
subst
372
ref
nil
633
ref
941
remove
nil
cons
cons
nil
cons
nil
cons
cons
685
ref
subst
appThm
nil
633
remove
946
remove
nil
cons
cons
nil
cons
nil
cons
cons
685
remove
subst
appThm
trans
appThm
949
ref
refl
appThm
trans
943
ref
refl
nil
88
ref
950
ref
cons
953
def
68
ref
951
ref
cons
nil
cons
cons
nil
cons
cons
702
remove
subst
appThm
nil
461
remove
951
ref
cons
953
remove
68
ref
952
ref
cons
nil
cons
cons
cons
nil
cons
cons
866
remove
subst
trans
nil
687
remove
952
remove
cons
686
remove
951
remove
cons
841
remove
950
remove
cons
nil
cons
cons
cons
nil
cons
cons
870
remove
subst
251
ref
45
ref
378
ref
943
remove
871
remove
appTerm
appTerm
954
def
949
ref
appTerm
appTerm
954
remove
785
remove
appTerm
appTerm
absTerm
955
def
944
ref
appTerm
956
def
betaConv
878
remove
939
ref
appTerm
957
def
betaConv
928
remove
nil
929
remove
88
ref
957
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
250
ref
930
remove
43
ref
939
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
11
ref
955
ref
appTerm
nil
cons
cons
88
ref
956
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
246
ref
244
ref
955
remove
nil
cons
cons
251
ref
944
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
125
ref
378
remove
948
remove
appTerm
958
def
949
remove
appTerm
nil
cons
cons
126
ref
958
remove
945
remove
271
ref
appTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
140
ref
subst
proveHyp
eqMp
eqMp
eqMp
subst
eqMp
nil
68
ref
936
ref
cons
959
def
179
ref
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
959
ref
nil
cons
nil
cons
cons
194
ref
subst
933
remove
assume
eqMp
eqMp
eqMp
nil
125
ref
934
remove
cons
960
def
252
ref
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
nil
959
remove
802
remove
cons
nil
cons
cons
919
remove
subst
791
remove
assume
eqMp
nil
960
remove
126
ref
795
remove
cons
455
remove
178
remove
cons
nil
cons
cons
cons
nil
cons
cons
470
remove
subst
proveHyp
proveHyp
proveHyp
eqMp
nil
125
ref
792
remove
cons
252
ref
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
125
ref
788
remove
cons
126
ref
290
ref
cons
nil
cons
961
def
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
nil
125
ref
321
remove
cons
961
remove
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
nil
68
ref
78
ref
273
ref
appTerm
277
ref
appTerm
nil
cons
cons
88
ref
78
ref
277
remove
appTerm
273
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
157
ref
subst
proveHyp
nil
790
remove
88
ref
288
ref
cons
nil
cons
cons
nil
cons
cons
962
def
102
ref
subst
962
remove
157
ref
subst
nil
289
remove
nil
cons
nil
cons
cons
175
remove
subst
sym
nil
68
ref
75
ref
273
ref
appTerm
963
def
nil
cons
964
def
cons
179
ref
cons
nil
cons
cons
965
def
102
ref
subst
965
remove
157
ref
subst
nil
"x"
257
ref
var
966
def
272
ref
nil
cons
cons
nil
cons
nil
cons
cons
345
remove
163
remove
subst
967
def
subst
nil
68
ref
259
ref
272
ref
appTerm
272
ref
appTerm
968
def
nil
cons
cons
969
def
179
remove
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
969
remove
nil
cons
nil
cons
cons
194
remove
subst
20
ref
"_1223"
1
remove
var
970
def
75
ref
259
ref
267
remove
970
remove
varTerm
appTerm
271
ref
appTerm
appTerm
272
ref
appTerm
appTerm
absTerm
971
def
48
ref
appTerm
972
def
appTerm
refl
971
ref
270
ref
appTerm
betaConv
appThm
128
ref
972
remove
betaConv
appThm
75
ref
968
remove
appTerm
refl
appThm
trans
971
remove
refl
nil
125
ref
936
ref
cons
973
def
126
ref
801
ref
cons
nil
cons
974
def
cons
nil
cons
cons
975
def
140
ref
subst
appThm
eqMp
20
ref
"_1217"
8
remove
var
976
def
75
ref
259
ref
268
ref
976
remove
varTerm
appTerm
appTerm
272
ref
appTerm
appTerm
absTerm
977
def
52
ref
appTerm
978
def
appTerm
refl
977
ref
271
ref
appTerm
betaConv
appThm
128
ref
978
remove
betaConv
appThm
75
remove
259
ref
268
remove
271
ref
appTerm
appTerm
272
remove
appTerm
appTerm
refl
appThm
trans
977
remove
refl
975
remove
303
ref
subst
appThm
eqMp
963
remove
assume
eqMp
eqMp
eqMp
eqMp
eqMp
nil
125
ref
964
remove
cons
252
remove
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
125
ref
290
remove
cons
126
ref
288
remove
cons
nil
cons
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
eqMp
979
def
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
14
ref
285
remove
appTerm
thm
nil
339
remove
966
ref
30
ref
6
ref
39
ref
12
ref
259
ref
966
ref
varTerm
980
def
appTerm
981
def
269
ref
appTerm
982
def
absTerm
appTerm
absTerm
983
def
appTerm
984
def
absTerm
985
def
nil
cons
cons
nil
cons
nil
cons
cons
346
remove
subst
966
ref
nil
74
ref
984
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
203
ref
6
ref
472
ref
12
ref
981
ref
refl
313
remove
appThm
absThm
appThm
absThm
appThm
sym
361
remove
323
ref
980
ref
appTerm
986
def
appTerm
987
def
betaConv
367
remove
nil
68
ref
363
remove
cons
88
ref
987
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
24
remove
364
remove
38
remove
986
ref
nil
cons
cons
nil
cons
988
def
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
20
ref
30
ref
6
ref
39
ref
12
ref
41
ref
986
ref
appTerm
61
remove
appTerm
989
def
absTerm
990
def
appTerm
991
def
absTerm
992
def
appTerm
993
def
appTerm
994
def
41
remove
323
remove
261
ref
986
ref
appTerm
995
def
appTerm
appTerm
986
ref
appTerm
appTerm
nil
cons
cons
88
ref
30
ref
6
ref
39
ref
12
ref
981
remove
316
ref
appTerm
996
def
absTerm
appTerm
absTerm
appTerm
997
def
nil
cons
998
def
cons
nil
cons
999
def
cons
nil
cons
cons
146
ref
subst
proveHyp
292
ref
994
remove
refl
325
remove
324
remove
nil
340
remove
980
ref
nil
cons
cons
nil
cons
nil
cons
cons
347
remove
subst
1000
def
appThm
appThm
986
remove
refl
appThm
nil
988
remove
nil
cons
cons
26
remove
173
ref
subst
subst
trans
appThm
nil
74
ref
993
ref
nil
cons
cons
nil
cons
nil
cons
cons
74
ref
20
ref
117
remove
appTerm
79
ref
appTerm
absTerm
1001
def
79
remove
appTerm
1002
def
betaConv
nil
86
remove
1001
ref
appTerm
1003
def
axiom
nil
68
ref
1003
remove
nil
cons
cons
88
ref
1002
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
147
remove
148
ref
1001
remove
nil
cons
cons
150
remove
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
subst
trans
appThm
997
ref
refl
1004
def
appThm
sym
nil
5
ref
6
ref
78
ref
992
ref
48
ref
appTerm
1005
def
appTerm
997
ref
appTerm
1006
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
286
ref
subst
6
ref
nil
74
ref
1006
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
nil
68
ref
1005
ref
nil
cons
1007
def
cons
999
ref
cons
nil
cons
cons
1008
def
102
ref
subst
1008
remove
157
ref
subst
1005
ref
betaConv
1005
remove
assume
eqMp
nil
68
ref
991
ref
nil
cons
cons
999
ref
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
244
ref
12
ref
78
ref
990
ref
52
ref
appTerm
1009
def
appTerm
997
ref
appTerm
1010
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
287
ref
subst
12
ref
nil
74
ref
1010
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
nil
68
ref
1009
ref
nil
cons
1011
def
cons
999
ref
cons
nil
cons
cons
1012
def
102
ref
subst
1012
remove
157
ref
subst
1009
ref
betaConv
1009
remove
assume
eqMp
nil
68
ref
989
ref
nil
cons
1013
def
cons
999
ref
cons
nil
cons
cons
1014
def
146
ref
subst
proveHyp
1014
ref
102
ref
subst
1014
remove
157
ref
subst
261
ref
refl
989
remove
assume
appThm
nil
68
ref
259
ref
995
remove
appTerm
316
ref
appTerm
nil
cons
cons
999
ref
cons
nil
cons
cons
146
ref
subst
proveHyp
292
remove
305
remove
1000
remove
appThm
316
ref
refl
1015
def
appThm
appThm
1004
remove
appThm
sym
nil
68
ref
996
ref
nil
cons
1016
def
cons
999
remove
cons
nil
cons
cons
1017
def
102
ref
subst
1017
remove
157
ref
subst
20
ref
"_1229"
257
ref
var
1018
def
30
ref
6
ref
39
ref
12
ref
259
remove
1018
remove
varTerm
appTerm
316
ref
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
1019
def
980
ref
appTerm
1020
def
appTerm
refl
1019
ref
316
remove
appTerm
betaConv
appThm
128
ref
1020
remove
betaConv
appThm
30
ref
15
ref
39
ref
16
ref
320
remove
absTerm
appTerm
absTerm
1021
def
appTerm
refl
appThm
trans
1019
remove
refl
996
remove
assume
appThm
eqMp
sym
1021
ref
48
ref
appTerm
betaConv
sym
16
ref
317
remove
261
remove
60
remove
271
ref
appTerm
appTerm
appTerm
absTerm
1022
def
52
ref
appTerm
betaConv
sym
1015
remove
eqMp
246
ref
244
ref
1022
remove
nil
cons
cons
251
ref
306
remove
cons
1023
def
nil
cons
1024
def
cons
nil
cons
cons
742
remove
sym
nil
148
remove
126
ref
78
ref
722
remove
appTerm
131
remove
appTerm
1025
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
171
remove
286
ref
subst
subst
126
ref
nil
74
ref
1025
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
734
ref
102
ref
subst
734
remove
157
ref
subst
nil
68
ref
155
remove
cons
732
remove
cons
nil
cons
cons
146
ref
subst
721
ref
50
ref
appTerm
1026
def
betaConv
nil
724
remove
88
ref
1026
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
250
ref
5
ref
721
remove
nil
cons
cons
750
ref
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
746
remove
745
remove
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
1027
def
subst
proveHyp
eqMp
250
ref
5
ref
1021
remove
nil
cons
cons
309
ref
cons
nil
cons
cons
1027
ref
subst
proveHyp
eqMp
eqMp
nil
125
ref
1016
remove
cons
126
ref
998
remove
cons
nil
cons
1028
def
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
125
ref
1013
remove
cons
1028
ref
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
125
ref
1011
remove
cons
1028
ref
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
68
ref
11
ref
251
ref
78
ref
990
ref
719
ref
appTerm
appTerm
997
ref
appTerm
absTerm
appTerm
nil
cons
cons
88
ref
78
ref
991
remove
appTerm
997
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
246
ref
244
ref
990
remove
nil
cons
cons
1028
ref
cons
nil
cons
cons
747
ref
subst
eqMp
eqMp
eqMp
nil
125
ref
1007
remove
cons
1028
ref
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
68
ref
14
ref
43
ref
78
ref
992
ref
50
ref
appTerm
appTerm
997
ref
appTerm
absTerm
appTerm
nil
cons
cons
88
ref
78
ref
993
remove
appTerm
997
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
250
ref
5
ref
992
remove
nil
cons
cons
1028
remove
cons
nil
cons
cons
747
ref
subst
eqMp
eqMp
eqMp
eqMp
eqMp
absThm
eqMp
nil
348
remove
985
remove
appTerm
thm
nil
5
ref
6
ref
11
ref
12
ref
47
ref
"Data.Pair.fst"
966
ref
36
ref
983
remove
appTerm
absTerm
1029
def
defineConst
1030
def
pop
0
ref
257
ref
35
remove
cons
opType
constTerm
269
ref
appTerm
appTerm
48
ref
appTerm
1031
def
absTerm
1032
def
appTerm
1033
def
absTerm
1034
def
nil
cons
cons
nil
cons
nil
cons
cons
286
ref
subst
6
ref
nil
74
ref
1033
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
nil
244
ref
1032
remove
nil
cons
cons
nil
cons
nil
cons
cons
287
ref
subst
12
ref
nil
74
ref
1031
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
902
remove
nil
966
ref
269
ref
nil
cons
cons
nil
cons
nil
cons
cons
1035
def
1030
remove
967
ref
appThm
1029
remove
980
ref
appTerm
betaConv
trans
subst
appThm
513
ref
appThm
sym
nil
5
ref
762
ref
20
ref
15
ref
39
ref
16
ref
273
ref
absTerm
appTerm
absTerm
1036
def
763
ref
appTerm
1037
def
appTerm
764
ref
48
ref
appTerm
1038
def
appTerm
1039
def
absTerm
1040
def
nil
cons
cons
nil
cons
nil
cons
cons
286
ref
subst
762
ref
nil
74
ref
1039
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
128
ref
1037
remove
betaConv
appThm
1038
ref
refl
1041
def
appThm
sym
128
ref
472
ref
16
ref
nil
15
ref
772
remove
cons
nil
cons
nil
cons
cons
979
ref
subst
absThm
appThm
appThm
1041
remove
appThm
sym
nil
68
ref
39
remove
16
ref
45
remove
49
ref
763
ref
appTerm
1042
def
appTerm
276
ref
appTerm
1043
def
absTerm
1044
def
appTerm
1045
def
nil
cons
1046
def
cons
88
ref
1038
ref
nil
cons
1047
def
cons
nil
cons
1048
def
cons
nil
cons
cons
304
ref
subst
nil
244
ref
16
ref
78
ref
1044
ref
271
remove
appTerm
1049
def
appTerm
1038
ref
appTerm
1050
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
287
ref
subst
16
ref
nil
74
ref
1050
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
nil
68
ref
1049
ref
nil
cons
1051
def
cons
1048
ref
cons
nil
cons
cons
1052
def
102
ref
subst
1052
remove
157
ref
subst
1049
ref
betaConv
1049
remove
assume
eqMp
nil
68
ref
1043
remove
nil
cons
1053
def
cons
1048
remove
cons
nil
cons
cons
1054
def
146
ref
subst
proveHyp
1054
ref
102
ref
subst
1054
remove
157
ref
subst
nil
125
ref
1042
ref
nil
cons
cons
974
remove
cons
nil
cons
cons
140
ref
subst
764
remove
refl
1042
remove
assume
appThm
nil
773
remove
nil
cons
cons
173
ref
subst
trans
sym
118
ref
eqMp
proveHyp
eqMp
nil
125
ref
1053
remove
cons
126
ref
1047
ref
cons
nil
cons
1055
def
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
125
ref
1051
remove
cons
1055
ref
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
68
ref
11
ref
251
remove
78
ref
1044
ref
719
remove
appTerm
appTerm
1038
ref
appTerm
absTerm
appTerm
nil
cons
cons
88
ref
78
ref
1045
ref
appTerm
1038
ref
appTerm
nil
cons
1056
def
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
246
ref
244
ref
1044
remove
nil
cons
cons
1055
remove
cons
nil
cons
cons
747
ref
subst
eqMp
nil
68
ref
1056
remove
cons
88
ref
78
ref
1038
ref
appTerm
1045
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
157
ref
subst
proveHyp
nil
68
ref
1047
ref
cons
88
ref
1046
ref
cons
nil
cons
cons
nil
cons
cons
1057
def
102
ref
subst
1057
remove
157
ref
subst
472
remove
16
ref
372
remove
49
remove
refl
1038
remove
assume
appThm
nil
309
ref
nil
cons
cons
173
ref
subst
trans
appThm
276
ref
refl
appThm
nil
74
ref
801
remove
cons
nil
cons
nil
cons
cons
443
remove
subst
trans
absThm
appThm
sym
16
ref
276
remove
absTerm
1058
def
52
ref
appTerm
betaConv
sym
534
ref
eqMp
246
remove
244
ref
1058
remove
nil
cons
cons
1024
ref
cons
nil
cons
cons
1027
ref
subst
proveHyp
eqMp
eqMp
nil
125
ref
1047
remove
cons
126
ref
1046
remove
cons
nil
cons
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
absThm
eqMp
nil
68
ref
14
ref
1040
remove
appTerm
nil
cons
cons
88
ref
47
ref
36
remove
1036
ref
appTerm
appTerm
48
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
308
remove
32
ref
1036
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
43
ref
78
ref
14
ref
762
remove
20
ref
33
ref
763
remove
appTerm
appTerm
765
remove
appTerm
absTerm
appTerm
appTerm
47
remove
37
remove
appTerm
50
ref
appTerm
appTerm
absTerm
1059
def
50
ref
appTerm
1060
def
betaConv
32
remove
14
ref
1059
ref
appTerm
1061
def
absTerm
1062
def
33
remove
appTerm
1063
def
betaConv
nil
234
remove
1062
ref
appTerm
1064
def
axiom
nil
68
ref
1064
remove
nil
cons
cons
88
ref
1063
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
236
remove
237
remove
1062
remove
nil
cons
cons
239
remove
cons
nil
cons
cons
164
ref
subst
eqMp
eqMp
nil
68
ref
1061
remove
nil
cons
cons
88
ref
1060
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
250
ref
5
ref
1059
remove
nil
cons
cons
750
remove
cons
nil
cons
cons
164
remove
subst
eqMp
eqMp
1065
def
subst
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
14
ref
1034
remove
appTerm
thm
nil
5
ref
6
ref
11
ref
12
ref
51
ref
"Data.Pair.snd"
966
remove
34
remove
0
ref
9
remove
207
ref
cons
opType
constTerm
1066
def
12
ref
30
ref
6
ref
982
remove
absTerm
appTerm
absTerm
appTerm
absTerm
1067
def
defineConst
1068
def
pop
0
remove
257
remove
207
remove
cons
opType
constTerm
269
remove
appTerm
appTerm
52
ref
appTerm
1069
def
absTerm
1070
def
appTerm
1071
def
absTerm
1072
def
nil
cons
cons
nil
cons
nil
cons
cons
286
ref
subst
6
remove
nil
74
ref
1071
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
nil
244
ref
1070
remove
nil
cons
cons
nil
cons
nil
cons
cons
287
ref
subst
12
remove
nil
74
ref
1069
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
903
remove
1035
remove
1068
remove
967
remove
appThm
1067
remove
980
remove
appTerm
betaConv
trans
subst
appThm
534
remove
appThm
sym
nil
244
remove
44
ref
20
remove
16
ref
30
ref
15
ref
273
remove
absTerm
appTerm
absTerm
1073
def
54
ref
appTerm
1074
def
appTerm
51
ref
54
remove
appTerm
1075
def
52
ref
appTerm
1076
def
appTerm
1077
def
absTerm
1078
def
nil
cons
cons
nil
cons
nil
cons
cons
287
remove
subst
44
remove
nil
74
ref
1077
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
ref
subst
128
ref
1074
remove
betaConv
appThm
1076
ref
refl
1079
def
appThm
sym
128
remove
203
ref
15
ref
nil
16
remove
621
remove
cons
nil
cons
nil
cons
cons
979
remove
subst
absThm
appThm
appThm
1079
remove
appThm
sym
nil
68
ref
30
remove
15
ref
275
ref
55
ref
appTerm
1080
def
absTerm
1081
def
appTerm
1082
def
nil
cons
1083
def
cons
88
ref
1076
ref
nil
cons
1084
def
cons
nil
cons
1085
def
cons
nil
cons
cons
304
remove
subst
nil
5
ref
15
ref
78
ref
1081
ref
270
remove
appTerm
1086
def
appTerm
1076
ref
appTerm
1087
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
286
remove
subst
15
ref
nil
74
ref
1087
remove
nil
cons
cons
nil
cons
nil
cons
cons
119
remove
subst
nil
68
ref
1086
ref
nil
cons
1088
def
cons
1085
ref
cons
nil
cons
cons
1089
def
102
ref
subst
1089
remove
157
ref
subst
1086
ref
betaConv
1086
remove
assume
eqMp
nil
68
ref
1080
remove
nil
cons
1090
def
cons
1085
remove
cons
nil
cons
cons
1091
def
146
ref
subst
proveHyp
1091
ref
102
ref
subst
1091
remove
157
ref
subst
nil
973
remove
126
ref
55
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
303
remove
subst
1075
remove
refl
55
remove
assume
appThm
nil
751
remove
nil
cons
cons
247
ref
173
remove
subst
1092
def
subst
trans
sym
118
remove
eqMp
proveHyp
eqMp
nil
125
ref
1090
remove
cons
126
ref
1084
ref
cons
nil
cons
1093
def
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
125
ref
1088
remove
cons
1093
ref
cons
nil
cons
cons
140
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
68
ref
14
ref
43
remove
78
ref
1081
ref
50
remove
appTerm
appTerm
1076
ref
appTerm
absTerm
appTerm
nil
cons
cons
88
ref
78
ref
1082
ref
appTerm
1076
ref
appTerm
nil
cons
1094
def
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
250
ref
5
ref
1081
remove
nil
cons
cons
1093
remove
cons
nil
cons
cons
747
remove
subst
eqMp
nil
68
ref
1094
remove
cons
88
ref
78
remove
1076
ref
appTerm
1082
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
157
ref
subst
proveHyp
nil
68
ref
1084
ref
cons
88
ref
1083
ref
cons
nil
cons
cons
nil
cons
cons
1095
def
102
remove
subst
1095
remove
157
remove
subst
203
remove
15
ref
275
remove
refl
53
remove
refl
1076
remove
assume
appThm
nil
1024
remove
nil
cons
cons
1092
remove
subst
trans
appThm
nil
74
remove
936
remove
cons
nil
cons
nil
cons
cons
418
remove
subst
trans
absThm
appThm
sym
15
remove
274
remove
absTerm
1096
def
48
remove
appTerm
betaConv
sym
513
remove
eqMp
250
remove
5
remove
1096
remove
nil
cons
cons
309
remove
cons
nil
cons
cons
1027
remove
subst
proveHyp
eqMp
eqMp
nil
125
remove
1084
remove
cons
126
remove
1083
remove
cons
nil
cons
cons
nil
cons
cons
140
remove
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
absThm
eqMp
nil
68
remove
11
remove
1078
remove
appTerm
nil
cons
cons
88
remove
51
remove
1066
remove
1073
ref
appTerm
appTerm
52
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
remove
subst
proveHyp
nil
1023
remove
509
remove
1073
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
247
remove
1065
remove
subst
subst
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
14
remove
1072
remove
appTerm
thm