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