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