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