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