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