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