6
version
nil
"P"
"->"
typeOp
0
def
"Number.Natural.natural"
typeOp
nil
opType
1
def
"bool"
typeOp
nil
opType
2
def
nil
cons
3
def
cons
opType
4
def
var
5
def
"n"
1
ref
var
6
def
"Data.Bool.!"
const
7
def
0
ref
4
ref
3
ref
cons
opType
8
def
constTerm
9
def
"r"
1
ref
var
10
def
9
ref
"k"
1
ref
var
11
def
9
ref
"a"
1
ref
var
12
def
"Data.Bool.==>"
const
0
ref
2
ref
0
ref
2
ref
3
ref
cons
opType
13
def
nil
cons
cons
opType
14
def
constTerm
15
def
"Data.Bool./\\"
const
14
ref
constTerm
16
def
"Data.Bool.~"
const
13
ref
constTerm
17
def
"="
const
18
def
0
ref
1
ref
4
ref
nil
cons
cons
opType
19
def
constTerm
20
def
6
ref
varTerm
21
def
appTerm
22
def
"Number.Natural.zero"
const
1
ref
constTerm
23
def
appTerm
24
def
appTerm
25
def
appTerm
26
def
16
ref
17
ref
20
ref
10
ref
varTerm
27
def
appTerm
23
ref
appTerm
28
def
appTerm
29
def
appTerm
30
def
"Number.Natural.<="
const
19
ref
constTerm
31
def
12
ref
varTerm
32
def
appTerm
33
def
27
ref
appTerm
34
def
appTerm
35
def
appTerm
36
def
appTerm
31
ref
"Number.Natural.Montgomery.reduce"
const
0
ref
1
ref
0
ref
1
ref
0
ref
1
ref
0
ref
1
ref
1
ref
nil
cons
37
def
cons
opType
38
def
nil
cons
cons
opType
39
def
nil
cons
40
def
cons
opType
nil
cons
cons
opType
constTerm
21
ref
appTerm
41
def
27
ref
appTerm
11
ref
varTerm
42
def
appTerm
32
ref
appTerm
43
def
appTerm
21
ref
appTerm
44
def
appTerm
45
def
absTerm
46
def
appTerm
47
def
absTerm
48
def
appTerm
49
def
absTerm
50
def
appTerm
51
def
absTerm
52
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
37
ref
cons
nil
cons
53
def
nil
nil
cons
54
def
cons
55
def
18
ref
14
ref
constTerm
56
def
7
ref
0
ref
0
ref
"A"
varType
57
def
3
ref
cons
opType
58
def
3
ref
cons
opType
59
def
constTerm
60
def
"P"
58
ref
var
61
def
varTerm
62
def
appTerm
63
def
appTerm
refl
"p"
58
ref
var
64
def
18
ref
0
ref
58
ref
59
ref
nil
cons
cons
opType
constTerm
64
ref
varTerm
65
def
appTerm
"x"
57
ref
var
66
def
"Data.Bool.T"
const
2
ref
constTerm
67
def
absTerm
68
def
appTerm
absTerm
69
def
62
ref
appTerm
betaConv
70
def
appThm
nil
18
ref
0
ref
59
ref
0
ref
59
ref
3
ref
cons
opType
71
def
nil
cons
cons
opType
constTerm
72
def
60
ref
appTerm
69
remove
appTerm
axiom
62
ref
refl
73
def
appThm
74
def
eqMp
sym
75
def
subst
76
def
subst
6
ref
nil
"t"
2
ref
var
77
def
51
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
77
ref
varTerm
78
def
appTerm
79
def
67
ref
appTerm
80
def
assume
sym
nil
67
ref
axiom
81
def
eqMp
78
ref
assume
81
ref
deductAntisym
deductAntisym
82
def
subst
nil
5
ref
50
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
10
ref
nil
77
ref
49
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
48
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
11
ref
nil
77
ref
47
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
46
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
12
ref
nil
77
ref
45
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
"p"
2
ref
var
83
def
36
remove
nil
cons
84
def
cons
"q"
2
ref
var
85
def
44
remove
nil
cons
86
def
cons
nil
cons
cons
nil
cons
cons
87
def
56
ref
15
ref
83
ref
varTerm
88
def
appTerm
89
def
85
ref
varTerm
90
def
appTerm
91
def
appTerm
refl
83
ref
85
ref
56
ref
16
ref
88
ref
appTerm
92
def
90
ref
appTerm
93
def
appTerm
94
def
88
ref
appTerm
absTerm
95
def
absTerm
96
def
88
ref
appTerm
betaConv
90
ref
refl
97
def
appThm
95
remove
90
ref
appTerm
betaConv
trans
appThm
nil
18
ref
0
ref
14
ref
0
ref
14
ref
3
ref
cons
opType
98
def
nil
cons
cons
opType
constTerm
99
def
15
ref
appTerm
96
remove
appTerm
axiom
88
ref
refl
100
def
appThm
97
ref
appThm
eqMp
101
def
sym
102
def
subst
87
remove
56
ref
refl
103
def
"f"
14
ref
var
104
def
104
ref
varTerm
105
def
88
ref
appTerm
90
ref
appTerm
absTerm
106
def
83
ref
85
ref
90
ref
absTerm
107
def
absTerm
108
def
appTerm
betaConv
108
ref
88
ref
appTerm
betaConv
97
ref
appThm
107
ref
90
ref
appTerm
betaConv
trans
trans
appThm
104
ref
105
ref
67
ref
appTerm
67
ref
appTerm
absTerm
109
def
108
ref
appTerm
betaConv
108
ref
67
ref
appTerm
betaConv
67
ref
refl
110
def
appThm
107
ref
67
ref
appTerm
betaConv
trans
trans
111
def
appThm
94
remove
refl
85
ref
18
ref
0
ref
98
ref
0
ref
98
remove
3
ref
cons
opType
nil
cons
cons
opType
constTerm
112
def
106
remove
appTerm
109
ref
appTerm
absTerm
113
def
90
ref
appTerm
betaConv
appThm
18
ref
0
ref
13
ref
0
ref
13
ref
3
ref
cons
opType
114
def
nil
cons
cons
opType
constTerm
115
def
92
remove
appTerm
refl
83
ref
113
remove
absTerm
116
def
88
ref
appTerm
betaConv
appThm
nil
99
ref
16
ref
appTerm
116
ref
appTerm
axiom
117
def
100
remove
appThm
eqMp
97
ref
appThm
eqMp
118
def
93
remove
assume
eqMp
108
ref
refl
119
def
appThm
eqMp
sym
81
ref
eqMp
120
def
118
remove
sym
104
ref
105
ref
refl
nil
77
ref
88
ref
nil
cons
121
def
cons
nil
cons
nil
cons
cons
82
ref
subst
88
ref
assume
122
def
eqMp
appThm
nil
77
ref
90
ref
nil
cons
123
def
cons
nil
cons
nil
cons
cons
82
ref
subst
90
ref
assume
124
def
eqMp
appThm
absThm
eqMp
125
def
deductAntisym
126
def
subst
nil
"P"
2
ref
var
127
def
25
ref
nil
cons
128
def
cons
129
def
"Q"
2
ref
var
130
def
35
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
131
def
103
ref
104
ref
105
remove
127
ref
varTerm
132
def
appTerm
133
def
130
ref
varTerm
134
def
appTerm
absTerm
135
def
83
ref
85
ref
88
ref
absTerm
absTerm
136
def
appTerm
betaConv
136
ref
132
ref
appTerm
betaConv
134
ref
refl
137
def
appThm
85
ref
132
ref
absTerm
134
ref
appTerm
betaConv
trans
trans
appThm
109
ref
136
ref
appTerm
betaConv
136
ref
67
ref
appTerm
betaConv
110
remove
appThm
85
ref
67
ref
absTerm
67
ref
appTerm
betaConv
trans
trans
appThm
56
ref
16
ref
132
ref
appTerm
138
def
134
ref
appTerm
139
def
appTerm
refl
85
ref
112
remove
104
remove
133
remove
90
ref
appTerm
absTerm
appTerm
109
remove
appTerm
absTerm
134
ref
appTerm
betaConv
appThm
115
ref
138
remove
appTerm
refl
116
remove
132
ref
appTerm
betaConv
appThm
117
remove
132
ref
refl
140
def
appThm
eqMp
137
ref
appThm
eqMp
139
remove
assume
eqMp
141
def
136
remove
refl
appThm
eqMp
sym
81
ref
eqMp
142
def
subst
131
remove
103
ref
135
remove
108
ref
appTerm
betaConv
108
remove
132
ref
appTerm
betaConv
137
ref
appThm
107
remove
134
ref
appTerm
betaConv
trans
trans
appThm
111
remove
appThm
141
remove
119
remove
appThm
eqMp
sym
81
ref
eqMp
143
def
subst
nil
127
ref
29
ref
nil
cons
144
def
cons
145
def
130
ref
34
ref
nil
cons
146
def
cons
nil
cons
cons
nil
cons
cons
147
def
142
ref
subst
147
remove
143
ref
subst
nil
"m"
1
ref
var
148
def
43
ref
nil
cons
149
def
cons
nil
cons
150
def
nil
cons
cons
6
ref
56
ref
31
ref
148
ref
varTerm
151
def
appTerm
21
ref
appTerm
152
def
appTerm
"Number.Natural.<"
const
19
ref
constTerm
153
def
151
ref
appTerm
154
def
"Number.Natural.suc"
const
38
ref
constTerm
155
def
21
ref
appTerm
156
def
appTerm
157
def
appTerm
158
def
absTerm
159
def
21
ref
appTerm
160
def
betaConv
148
ref
9
ref
159
ref
appTerm
161
def
absTerm
162
def
151
ref
appTerm
163
def
betaConv
9
ref
refl
164
def
148
ref
164
ref
6
ref
158
remove
assume
sym
56
ref
157
remove
appTerm
152
ref
appTerm
165
def
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
nil
9
ref
148
ref
9
ref
6
ref
165
remove
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
83
ref
9
ref
162
ref
appTerm
nil
cons
cons
85
ref
163
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
102
ref
125
remove
nil
127
ref
121
ref
cons
130
ref
123
ref
cons
nil
cons
166
def
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
101
remove
91
ref
assume
eqMp
sym
122
remove
eqMp
120
remove
proveHyp
deductAntisym
167
def
subst
proveHyp
53
ref
5
ref
162
remove
nil
cons
cons
"x"
1
ref
var
168
def
151
ref
nil
cons
169
def
cons
nil
cons
170
def
cons
nil
cons
cons
nil
83
ref
63
ref
nil
cons
171
def
cons
85
ref
62
ref
66
ref
varTerm
172
def
appTerm
173
def
nil
cons
174
def
cons
nil
cons
cons
nil
cons
cons
175
def
102
ref
subst
175
remove
126
ref
subst
56
ref
173
ref
appTerm
refl
68
remove
172
ref
appTerm
betaConv
appThm
70
remove
74
remove
63
remove
assume
eqMp
eqMp
172
ref
refl
176
def
appThm
eqMp
sym
81
ref
eqMp
eqMp
nil
127
ref
171
remove
cons
130
ref
174
ref
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
177
def
subst
eqMp
eqMp
nil
83
ref
161
remove
nil
cons
cons
85
ref
160
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
159
remove
nil
cons
cons
168
ref
21
ref
nil
cons
178
def
cons
nil
cons
179
def
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
153
ref
43
ref
appTerm
180
def
refl
181
def
nil
148
ref
178
ref
cons
nil
cons
182
def
nil
cons
cons
183
def
148
ref
20
ref
155
ref
151
ref
appTerm
184
def
appTerm
185
def
"Number.Natural.+"
const
39
ref
constTerm
186
def
"Number.Natural.bit1"
const
38
ref
constTerm
187
def
23
ref
appTerm
188
def
appTerm
189
def
151
ref
appTerm
appTerm
absTerm
190
def
151
ref
appTerm
191
def
betaConv
164
ref
148
ref
185
ref
refl
nil
6
ref
188
ref
nil
cons
192
def
cons
193
def
nil
cons
nil
cons
cons
194
def
6
ref
20
ref
186
ref
151
ref
appTerm
195
def
21
ref
appTerm
196
def
appTerm
197
def
186
ref
21
ref
appTerm
198
def
151
ref
appTerm
199
def
appTerm
absTerm
200
def
21
ref
appTerm
201
def
betaConv
148
ref
9
ref
200
ref
appTerm
202
def
absTerm
203
def
151
ref
appTerm
204
def
betaConv
nil
9
ref
203
ref
appTerm
205
def
axiom
nil
83
ref
205
remove
nil
cons
cons
85
ref
204
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
203
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
202
remove
nil
cons
cons
85
ref
201
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
200
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
206
def
subst
appThm
absThm
appThm
nil
9
ref
148
ref
185
remove
195
ref
188
ref
appTerm
207
def
appTerm
208
def
absTerm
appTerm
axiom
209
def
eqMp
nil
83
ref
9
ref
190
ref
appTerm
nil
cons
cons
85
ref
191
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
190
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
appThm
trans
sym
16
ref
refl
210
def
17
ref
refl
211
def
nil
83
ref
128
remove
cons
212
def
85
ref
56
ref
24
ref
appTerm
"Data.Bool.F"
const
2
ref
constTerm
213
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
nil
127
ref
24
ref
nil
cons
cons
nil
cons
nil
cons
cons
nil
83
ref
17
ref
132
ref
appTerm
214
def
nil
cons
215
def
cons
85
ref
56
ref
132
ref
appTerm
213
ref
appTerm
nil
cons
216
def
cons
nil
cons
cons
nil
cons
cons
217
def
102
ref
subst
217
remove
126
ref
subst
nil
83
ref
132
ref
nil
cons
218
def
cons
85
ref
213
ref
nil
cons
219
def
cons
nil
cons
220
def
cons
nil
cons
cons
15
ref
refl
221
def
56
ref
88
ref
appTerm
90
ref
appTerm
222
def
assume
223
def
appThm
97
remove
appThm
sym
nil
83
ref
123
ref
cons
224
def
85
ref
123
ref
cons
nil
cons
cons
nil
cons
cons
225
def
102
ref
subst
225
remove
126
ref
subst
124
remove
eqMp
nil
127
ref
123
remove
cons
166
remove
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
226
def
eqMp
227
def
nil
83
ref
91
remove
nil
cons
228
def
cons
85
ref
15
ref
90
ref
appTerm
229
def
88
ref
appTerm
nil
cons
230
def
cons
nil
cons
cons
nil
cons
cons
126
ref
subst
proveHyp
229
ref
refl
223
remove
appThm
sym
226
remove
eqMp
eqMp
nil
224
remove
85
ref
121
remove
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
nil
127
ref
228
ref
cons
130
ref
230
remove
cons
nil
cons
cons
nil
cons
cons
231
def
143
ref
subst
eqMp
167
ref
231
remove
142
ref
subst
eqMp
deductAntisym
deductAntisym
subst
56
ref
214
ref
appTerm
refl
83
ref
89
ref
213
ref
appTerm
absTerm
232
def
132
ref
appTerm
betaConv
appThm
nil
115
ref
17
ref
appTerm
232
remove
appTerm
axiom
140
ref
appThm
eqMp
233
def
214
remove
assume
eqMp
nil
83
ref
15
ref
132
ref
appTerm
234
def
213
ref
appTerm
nil
cons
cons
85
ref
15
ref
213
ref
appTerm
132
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
126
ref
subst
proveHyp
nil
83
ref
219
ref
cons
85
ref
218
ref
cons
nil
cons
cons
nil
cons
cons
235
def
102
ref
subst
235
remove
126
ref
subst
83
ref
88
remove
absTerm
236
def
132
ref
appTerm
237
def
betaConv
nil
56
ref
213
ref
appTerm
7
ref
114
remove
constTerm
238
def
236
ref
appTerm
239
def
appTerm
axiom
213
ref
assume
eqMp
nil
83
ref
239
remove
nil
cons
cons
85
ref
237
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
"A"
3
remove
cons
nil
cons
240
def
"P"
13
remove
var
241
def
236
remove
nil
cons
cons
"x"
2
ref
var
242
def
218
ref
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
243
def
eqMp
nil
127
ref
219
ref
cons
130
ref
218
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
127
ref
215
remove
cons
130
ref
216
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
244
def
subst
eqMp
appThm
nil
56
ref
17
ref
213
ref
appTerm
appTerm
67
ref
appTerm
axiom
245
def
trans
246
def
appThm
247
def
210
ref
211
ref
nil
83
ref
144
remove
cons
248
def
85
ref
56
ref
28
ref
appTerm
213
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
nil
127
ref
28
ref
nil
cons
249
def
cons
250
def
nil
cons
nil
cons
cons
251
def
244
ref
subst
eqMp
252
def
appThm
245
ref
trans
253
def
appThm
254
def
33
ref
refl
nil
148
ref
27
ref
nil
cons
255
def
cons
nil
cons
256
def
nil
cons
cons
257
def
148
ref
20
ref
"Number.Natural.*"
const
39
ref
constTerm
258
def
151
ref
appTerm
259
def
188
ref
appTerm
appTerm
151
ref
appTerm
absTerm
260
def
151
ref
appTerm
261
def
betaConv
nil
9
ref
260
ref
appTerm
262
def
axiom
nil
83
ref
262
remove
nil
cons
cons
85
ref
261
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
260
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
263
def
subst
appThm
nil
77
ref
146
remove
cons
nil
cons
nil
cons
cons
82
ref
subst
34
remove
assume
eqMp
trans
appThm
nil
77
ref
67
ref
nil
cons
cons
nil
cons
nil
cons
cons
264
def
77
ref
56
ref
16
ref
67
ref
appTerm
78
ref
appTerm
appTerm
78
ref
appTerm
absTerm
265
def
78
ref
appTerm
266
def
betaConv
nil
238
ref
265
ref
appTerm
267
def
axiom
nil
83
ref
267
remove
nil
cons
cons
85
ref
266
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
240
ref
241
ref
265
remove
nil
cons
cons
242
ref
78
ref
nil
cons
cons
nil
cons
268
def
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
269
def
trans
appThm
269
ref
trans
sym
81
ref
eqMp
nil
83
ref
26
ref
30
ref
33
ref
258
ref
27
ref
appTerm
270
def
188
ref
appTerm
appTerm
appTerm
appTerm
nil
cons
cons
85
ref
180
ref
189
ref
21
ref
appTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
nil
148
ref
192
ref
cons
nil
cons
271
def
nil
cons
cons
nil
83
ref
26
ref
30
ref
33
ref
270
ref
151
ref
appTerm
272
def
appTerm
273
def
appTerm
274
def
appTerm
275
def
nil
cons
276
def
cons
85
ref
180
ref
196
ref
appTerm
277
def
nil
cons
278
def
cons
nil
cons
cons
nil
cons
cons
279
def
102
ref
subst
279
remove
126
ref
subst
nil
129
ref
130
ref
274
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
280
def
142
ref
subst
280
remove
143
ref
subst
nil
145
ref
130
ref
273
ref
nil
cons
281
def
cons
nil
cons
cons
nil
cons
cons
282
def
142
ref
subst
282
remove
143
ref
subst
153
ref
refl
283
def
12
ref
20
ref
43
ref
appTerm
284
def
"Number.Natural.div"
const
39
ref
constTerm
285
def
186
ref
32
ref
appTerm
286
def
258
ref
"Number.Natural.mod"
const
39
ref
constTerm
287
def
258
ref
32
ref
appTerm
288
def
42
ref
appTerm
289
def
appTerm
290
def
27
ref
appTerm
291
def
appTerm
292
def
21
ref
appTerm
293
def
appTerm
294
def
appTerm
295
def
27
ref
appTerm
296
def
appTerm
absTerm
297
def
32
ref
appTerm
298
def
betaConv
11
ref
9
ref
297
ref
appTerm
299
def
absTerm
300
def
42
ref
appTerm
301
def
betaConv
10
ref
9
ref
300
ref
appTerm
302
def
absTerm
303
def
27
ref
appTerm
304
def
betaConv
6
ref
9
ref
303
ref
appTerm
305
def
absTerm
306
def
21
ref
appTerm
307
def
betaConv
nil
9
ref
306
ref
appTerm
308
def
axiom
nil
83
ref
308
remove
nil
cons
cons
85
ref
307
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
306
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
305
remove
nil
cons
cons
85
ref
304
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
303
remove
nil
cons
cons
168
ref
255
ref
cons
nil
cons
309
def
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
302
remove
nil
cons
cons
85
ref
301
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
300
remove
nil
cons
cons
168
ref
42
ref
nil
cons
310
def
cons
nil
cons
311
def
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
299
remove
nil
cons
cons
85
ref
298
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
297
remove
nil
cons
cons
168
ref
32
ref
nil
cons
312
def
cons
nil
cons
313
def
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
314
def
appThm
196
ref
refl
appThm
sym
153
ref
294
ref
appTerm
315
def
refl
nil
"p"
1
ref
var
316
def
178
remove
cons
317
def
6
ref
169
ref
cons
256
ref
cons
cons
nil
cons
cons
316
ref
20
ref
259
ref
198
ref
316
ref
varTerm
318
def
appTerm
319
def
appTerm
appTerm
186
ref
259
ref
21
ref
appTerm
320
def
appTerm
259
ref
318
ref
appTerm
321
def
appTerm
appTerm
absTerm
322
def
318
ref
appTerm
323
def
betaConv
6
ref
9
ref
322
ref
appTerm
324
def
absTerm
325
def
21
ref
appTerm
326
def
betaConv
148
ref
9
ref
325
ref
appTerm
327
def
absTerm
328
def
151
ref
appTerm
329
def
betaConv
nil
9
ref
328
ref
appTerm
330
def
axiom
nil
83
ref
330
remove
nil
cons
cons
85
ref
329
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
328
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
327
remove
nil
cons
cons
85
ref
326
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
325
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
324
remove
nil
cons
cons
85
ref
323
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
322
remove
nil
cons
cons
168
ref
318
ref
nil
cons
cons
nil
cons
331
def
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
332
def
subst
appThm
sym
"n'"
1
ref
var
333
def
16
ref
315
ref
333
ref
varTerm
334
def
appTerm
appTerm
31
ref
334
ref
appTerm
335
def
186
ref
272
ref
appTerm
270
ref
21
ref
appTerm
336
def
appTerm
337
def
appTerm
appTerm
absTerm
338
def
286
ref
336
ref
appTerm
339
def
appTerm
betaConv
sym
210
ref
nil
316
ref
336
ref
nil
cons
340
def
cons
6
ref
293
ref
nil
cons
341
def
cons
148
ref
312
ref
cons
nil
cons
342
def
cons
cons
nil
cons
cons
316
ref
56
ref
153
ref
196
ref
appTerm
195
ref
318
ref
appTerm
343
def
appTerm
appTerm
153
ref
21
ref
appTerm
344
def
318
ref
appTerm
345
def
appTerm
absTerm
346
def
318
ref
appTerm
347
def
betaConv
6
ref
9
ref
346
ref
appTerm
348
def
absTerm
349
def
21
ref
appTerm
350
def
betaConv
148
ref
9
ref
349
ref
appTerm
351
def
absTerm
352
def
151
ref
appTerm
353
def
betaConv
nil
9
ref
352
ref
appTerm
354
def
axiom
nil
83
ref
354
remove
nil
cons
cons
85
ref
353
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
352
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
351
remove
nil
cons
cons
85
ref
350
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
349
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
348
remove
nil
cons
cons
85
ref
347
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
346
remove
nil
cons
cons
331
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
355
def
subst
nil
6
ref
255
ref
cons
356
def
317
ref
148
ref
291
ref
nil
cons
357
def
cons
nil
cons
358
def
cons
359
def
cons
nil
cons
cons
316
ref
56
ref
153
ref
321
ref
appTerm
258
ref
21
ref
appTerm
360
def
318
ref
appTerm
361
def
appTerm
appTerm
16
ref
154
ref
21
ref
appTerm
362
def
appTerm
363
def
17
ref
20
ref
318
ref
appTerm
23
ref
appTerm
364
def
appTerm
appTerm
appTerm
absTerm
365
def
318
ref
appTerm
366
def
betaConv
6
ref
9
ref
365
ref
appTerm
367
def
absTerm
368
def
21
ref
appTerm
369
def
betaConv
148
ref
9
ref
368
ref
appTerm
370
def
absTerm
371
def
151
ref
appTerm
372
def
betaConv
nil
9
ref
371
ref
appTerm
373
def
axiom
nil
83
ref
373
remove
nil
cons
cons
85
ref
372
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
371
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
370
remove
nil
cons
cons
85
ref
369
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
368
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
367
remove
nil
cons
cons
85
ref
366
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
365
remove
nil
cons
cons
331
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
trans
16
ref
153
ref
291
ref
appTerm
27
ref
appTerm
374
def
appTerm
refl
246
ref
appThm
nil
77
ref
374
remove
nil
cons
375
def
cons
nil
cons
nil
cons
cons
77
ref
56
ref
16
ref
78
ref
appTerm
67
ref
appTerm
appTerm
78
ref
appTerm
absTerm
376
def
78
ref
appTerm
377
def
betaConv
nil
238
ref
376
ref
appTerm
378
def
axiom
nil
83
ref
378
remove
nil
cons
cons
85
ref
377
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
240
ref
241
ref
376
remove
nil
cons
cons
268
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
379
def
trans
trans
appThm
nil
316
ref
272
remove
nil
cons
cons
148
ref
340
remove
cons
6
ref
312
ref
cons
nil
cons
380
def
cons
cons
nil
cons
cons
316
ref
56
ref
31
ref
199
ref
appTerm
186
ref
318
ref
appTerm
151
ref
appTerm
381
def
appTerm
appTerm
31
ref
21
ref
appTerm
382
def
318
ref
appTerm
383
def
appTerm
absTerm
384
def
318
ref
appTerm
385
def
betaConv
6
ref
9
ref
384
ref
appTerm
386
def
absTerm
387
def
21
ref
appTerm
388
def
betaConv
148
ref
9
ref
387
ref
appTerm
389
def
absTerm
390
def
151
ref
appTerm
391
def
betaConv
nil
9
ref
390
ref
appTerm
392
def
axiom
nil
83
ref
392
remove
nil
cons
cons
85
ref
391
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
390
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
389
remove
nil
cons
cons
85
ref
388
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
387
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
386
remove
nil
cons
cons
85
ref
385
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
384
remove
nil
cons
cons
331
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
nil
77
ref
281
remove
cons
nil
cons
nil
cons
cons
82
ref
subst
273
remove
assume
eqMp
trans
appThm
379
remove
trans
sym
nil
248
ref
85
ref
375
remove
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
nil
356
ref
148
ref
289
ref
nil
cons
393
def
cons
nil
cons
394
def
cons
nil
cons
cons
6
ref
15
ref
25
remove
appTerm
395
def
153
ref
287
ref
151
ref
appTerm
396
def
21
ref
appTerm
397
def
appTerm
21
ref
appTerm
appTerm
absTerm
398
def
21
ref
appTerm
399
def
betaConv
148
ref
9
ref
398
ref
appTerm
400
def
absTerm
401
def
151
ref
appTerm
402
def
betaConv
nil
9
ref
401
ref
appTerm
403
def
axiom
nil
83
ref
403
remove
nil
cons
cons
85
ref
402
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
401
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
400
remove
nil
cons
cons
85
ref
399
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
398
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
404
def
subst
eqMp
eqMp
eqMp
53
ref
5
ref
338
ref
nil
cons
cons
168
ref
339
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
56
ref
"Data.Bool.?"
const
405
def
59
ref
constTerm
406
def
62
ref
appTerm
407
def
appTerm
408
def
refl
64
ref
238
ref
85
ref
15
ref
60
ref
66
ref
15
ref
65
ref
172
ref
appTerm
409
def
appTerm
90
ref
appTerm
absTerm
appTerm
appTerm
90
ref
appTerm
absTerm
appTerm
absTerm
410
def
62
remove
appTerm
betaConv
appThm
nil
72
remove
406
ref
appTerm
410
remove
appTerm
axiom
73
remove
appThm
eqMp
411
def
sym
nil
241
ref
130
ref
15
ref
60
ref
66
ref
15
ref
173
remove
appTerm
412
def
134
ref
appTerm
absTerm
413
def
appTerm
414
def
appTerm
134
ref
appTerm
415
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
240
ref
54
remove
cons
75
ref
subst
subst
130
ref
nil
77
ref
415
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
83
ref
414
remove
nil
cons
416
def
cons
417
def
85
ref
134
ref
nil
cons
418
def
cons
nil
cons
419
def
cons
nil
cons
cons
420
def
102
ref
subst
420
ref
126
ref
subst
nil
83
ref
174
remove
cons
419
ref
cons
nil
cons
cons
167
ref
subst
413
ref
172
ref
appTerm
421
def
betaConv
nil
417
ref
85
ref
421
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
"A"
57
ref
nil
cons
422
def
cons
nil
cons
423
def
61
ref
413
remove
nil
cons
cons
66
ref
172
ref
nil
cons
cons
nil
cons
424
def
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
127
ref
416
remove
cons
425
def
130
ref
418
ref
cons
nil
cons
426
def
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
427
def
subst
proveHyp
nil
83
ref
405
remove
8
remove
constTerm
428
def
338
remove
appTerm
nil
cons
cons
85
ref
315
ref
337
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
nil
316
ref
337
remove
nil
cons
cons
148
ref
294
ref
nil
cons
429
def
cons
nil
cons
430
def
cons
nil
cons
cons
316
ref
15
ref
428
ref
6
ref
363
ref
383
remove
appTerm
431
def
absTerm
432
def
appTerm
433
def
appTerm
434
def
154
remove
318
ref
appTerm
435
def
appTerm
436
def
absTerm
437
def
318
ref
appTerm
438
def
betaConv
148
ref
9
ref
437
ref
appTerm
439
def
absTerm
440
def
151
ref
appTerm
441
def
betaConv
nil
9
ref
148
ref
9
ref
6
ref
9
ref
316
ref
15
ref
431
ref
appTerm
435
ref
appTerm
absTerm
442
def
appTerm
443
def
absTerm
444
def
appTerm
445
def
absTerm
446
def
appTerm
447
def
axiom
nil
83
ref
447
ref
nil
cons
448
def
cons
449
def
85
ref
9
ref
440
ref
appTerm
nil
cons
450
def
cons
nil
cons
cons
nil
cons
cons
451
def
167
ref
subst
proveHyp
451
ref
102
ref
subst
451
remove
126
ref
subst
nil
5
ref
440
remove
nil
cons
cons
452
def
nil
cons
nil
cons
cons
76
ref
subst
148
ref
nil
77
ref
439
remove
nil
cons
453
def
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
437
remove
nil
cons
cons
454
def
nil
cons
nil
cons
cons
76
ref
subst
316
ref
nil
77
ref
436
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
83
ref
433
remove
nil
cons
455
def
cons
456
def
85
ref
435
ref
nil
cons
457
def
cons
nil
cons
458
def
cons
nil
cons
cons
459
def
102
ref
subst
459
remove
126
ref
subst
nil
449
ref
458
ref
cons
nil
cons
cons
460
def
167
ref
subst
nil
456
remove
85
ref
15
ref
447
remove
appTerm
435
ref
appTerm
461
def
nil
cons
462
def
cons
nil
cons
463
def
cons
nil
cons
cons
167
ref
subst
nil
5
ref
6
ref
15
ref
432
ref
21
ref
appTerm
464
def
appTerm
461
ref
appTerm
465
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
6
ref
nil
77
ref
465
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
83
ref
464
ref
nil
cons
466
def
cons
463
ref
cons
nil
cons
cons
467
def
102
ref
subst
467
remove
126
ref
subst
464
ref
betaConv
464
remove
assume
eqMp
nil
83
ref
431
remove
nil
cons
468
def
cons
469
def
463
remove
cons
nil
cons
cons
470
def
167
ref
subst
proveHyp
470
ref
102
ref
subst
470
remove
126
ref
subst
460
ref
102
ref
subst
460
remove
126
ref
subst
nil
469
remove
458
ref
cons
nil
cons
cons
167
ref
subst
442
ref
318
ref
appTerm
471
def
betaConv
444
ref
21
ref
appTerm
472
def
betaConv
446
ref
151
ref
appTerm
473
def
betaConv
nil
449
remove
85
ref
473
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
53
ref
5
ref
446
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
445
remove
nil
cons
cons
85
ref
472
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
444
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
443
remove
nil
cons
cons
85
ref
471
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
442
remove
nil
cons
cons
331
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
127
ref
448
remove
cons
474
def
130
ref
457
remove
cons
nil
cons
475
def
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
nil
127
ref
468
remove
cons
130
ref
462
remove
cons
nil
cons
476
def
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
127
ref
466
remove
cons
476
ref
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
83
ref
9
ref
168
ref
15
ref
432
ref
168
ref
varTerm
477
def
appTerm
appTerm
461
ref
appTerm
absTerm
appTerm
nil
cons
cons
85
ref
434
remove
461
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
432
remove
nil
cons
cons
476
remove
cons
nil
cons
cons
nil
417
remove
85
ref
15
ref
407
ref
appTerm
478
def
134
ref
appTerm
nil
cons
479
def
cons
nil
cons
cons
nil
cons
cons
480
def
102
ref
subst
480
remove
126
ref
subst
nil
83
ref
407
remove
nil
cons
481
def
cons
482
def
419
remove
cons
nil
cons
cons
483
def
102
ref
subst
483
remove
126
ref
subst
420
remove
167
ref
subst
85
ref
15
ref
60
ref
66
ref
412
remove
90
ref
appTerm
absTerm
appTerm
appTerm
90
remove
appTerm
absTerm
484
def
134
ref
appTerm
485
def
betaConv
nil
482
remove
85
ref
238
ref
484
ref
appTerm
486
def
nil
cons
487
def
cons
nil
cons
cons
nil
cons
cons
488
def
167
ref
subst
411
remove
nil
83
ref
408
remove
486
ref
appTerm
nil
cons
cons
85
ref
478
remove
486
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
488
remove
nil
83
ref
222
remove
nil
cons
489
def
cons
85
ref
228
ref
cons
nil
cons
cons
nil
cons
cons
490
def
102
ref
subst
490
remove
126
ref
subst
227
remove
eqMp
nil
127
ref
489
remove
cons
130
ref
228
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
83
ref
487
remove
cons
85
ref
485
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
240
ref
241
ref
484
remove
nil
cons
cons
242
ref
418
remove
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
127
ref
481
remove
cons
426
remove
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
nil
425
remove
130
ref
479
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
491
def
subst
eqMp
eqMp
eqMp
eqMp
nil
127
ref
455
remove
cons
475
ref
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
474
remove
130
ref
450
ref
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
nil
83
ref
450
remove
cons
85
ref
441
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
452
remove
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
453
remove
cons
85
ref
438
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
454
remove
331
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
492
def
subst
eqMp
eqMp
nil
83
ref
315
remove
270
ref
196
ref
appTerm
appTerm
nil
cons
cons
85
ref
153
ref
296
ref
appTerm
196
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
nil
6
ref
196
ref
nil
cons
cons
12
ref
255
ref
cons
493
def
"b"
1
ref
var
494
def
429
ref
cons
nil
cons
cons
cons
nil
cons
cons
6
ref
15
ref
153
ref
494
ref
varTerm
495
def
appTerm
288
ref
21
ref
appTerm
appTerm
appTerm
153
ref
285
ref
495
ref
appTerm
32
ref
appTerm
appTerm
21
ref
appTerm
appTerm
absTerm
496
def
21
ref
appTerm
497
def
betaConv
12
ref
9
ref
496
ref
appTerm
498
def
absTerm
499
def
32
ref
appTerm
500
def
betaConv
494
ref
9
ref
499
ref
appTerm
501
def
absTerm
502
def
495
ref
appTerm
503
def
betaConv
nil
9
ref
12
ref
9
ref
494
ref
498
ref
absTerm
504
def
appTerm
505
def
absTerm
506
def
appTerm
507
def
axiom
nil
83
ref
507
remove
nil
cons
508
def
cons
509
def
85
ref
9
ref
502
ref
appTerm
nil
cons
510
def
cons
nil
cons
cons
nil
cons
cons
511
def
167
ref
subst
proveHyp
511
ref
102
ref
subst
511
remove
126
ref
subst
nil
5
ref
502
remove
nil
cons
cons
512
def
nil
cons
nil
cons
cons
76
ref
subst
494
ref
nil
77
ref
501
remove
nil
cons
513
def
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
499
remove
nil
cons
cons
514
def
nil
cons
nil
cons
cons
76
ref
subst
12
ref
nil
77
ref
498
remove
nil
cons
515
def
cons
nil
cons
nil
cons
cons
82
ref
subst
504
ref
495
ref
appTerm
516
def
betaConv
506
ref
32
ref
appTerm
517
def
betaConv
nil
509
remove
85
ref
517
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
53
ref
5
ref
506
remove
nil
cons
cons
313
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
505
remove
nil
cons
cons
85
ref
516
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
504
remove
nil
cons
cons
168
ref
495
ref
nil
cons
cons
nil
cons
518
def
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
127
ref
508
remove
cons
130
ref
510
ref
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
nil
83
ref
510
remove
cons
85
ref
503
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
512
remove
518
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
513
remove
cons
85
ref
500
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
514
remove
313
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
515
remove
cons
85
ref
497
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
496
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
proveHyp
proveHyp
proveHyp
proveHyp
eqMp
nil
127
ref
276
remove
cons
130
ref
278
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
519
def
subst
eqMp
eqMp
proveHyp
proveHyp
proveHyp
proveHyp
eqMp
nil
127
ref
84
remove
cons
130
ref
86
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
52
remove
appTerm
thm
nil
5
ref
6
ref
9
ref
10
ref
9
ref
11
ref
9
ref
12
ref
15
ref
26
ref
30
ref
33
ref
270
ref
27
ref
appTerm
appTerm
appTerm
appTerm
appTerm
180
ref
186
ref
27
ref
appTerm
520
def
21
ref
appTerm
appTerm
appTerm
521
def
absTerm
522
def
appTerm
523
def
absTerm
524
def
appTerm
525
def
absTerm
526
def
appTerm
527
def
absTerm
528
def
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
6
ref
nil
77
ref
527
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
526
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
10
ref
nil
77
ref
525
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
524
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
11
ref
nil
77
ref
523
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
522
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
12
ref
nil
77
ref
521
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
257
ref
519
ref
subst
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
528
remove
appTerm
thm
nil
5
ref
6
ref
9
ref
10
ref
9
ref
11
ref
9
ref
148
ref
9
ref
12
ref
15
ref
275
remove
appTerm
277
remove
appTerm
529
def
absTerm
530
def
appTerm
531
def
absTerm
532
def
appTerm
533
def
absTerm
534
def
appTerm
535
def
absTerm
536
def
appTerm
537
def
absTerm
538
def
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
6
ref
nil
77
ref
537
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
536
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
10
ref
nil
77
ref
535
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
534
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
11
ref
nil
77
ref
533
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
532
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
148
ref
nil
77
ref
531
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
530
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
12
ref
nil
77
ref
529
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
519
ref
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
538
remove
appTerm
thm
nil
5
ref
6
ref
9
ref
10
ref
9
ref
11
ref
9
ref
12
ref
15
ref
26
ref
30
remove
33
remove
336
remove
appTerm
539
def
appTerm
540
def
appTerm
541
def
appTerm
180
ref
258
ref
"Number.Natural.bit0"
const
38
remove
constTerm
542
def
188
ref
appTerm
543
def
appTerm
21
ref
appTerm
544
def
appTerm
545
def
appTerm
546
def
absTerm
547
def
appTerm
548
def
absTerm
549
def
appTerm
550
def
absTerm
551
def
appTerm
552
def
absTerm
553
def
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
6
ref
nil
77
ref
552
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
551
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
10
ref
nil
77
ref
550
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
549
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
11
ref
nil
77
ref
548
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
547
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
12
ref
nil
77
ref
546
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
83
ref
541
remove
nil
cons
554
def
cons
555
def
85
ref
545
remove
nil
cons
556
def
cons
nil
cons
cons
nil
cons
cons
557
def
102
ref
subst
557
remove
126
ref
subst
nil
129
ref
130
ref
540
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
558
def
142
ref
subst
558
remove
143
ref
subst
nil
145
remove
130
ref
539
ref
nil
cons
559
def
cons
nil
cons
cons
nil
cons
cons
560
def
142
ref
subst
560
remove
143
ref
subst
181
remove
6
ref
20
ref
544
ref
appTerm
198
remove
21
ref
appTerm
561
def
appTerm
562
def
absTerm
563
def
21
ref
appTerm
564
def
betaConv
nil
9
ref
563
ref
appTerm
565
def
axiom
566
def
nil
83
ref
565
remove
nil
cons
cons
85
ref
564
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
563
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
appThm
sym
247
remove
254
remove
nil
77
ref
559
remove
cons
nil
cons
nil
cons
cons
82
ref
subst
539
remove
assume
eqMp
appThm
269
ref
trans
appThm
269
remove
trans
sym
81
ref
eqMp
nil
555
remove
85
ref
180
remove
561
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
183
remove
519
remove
subst
eqMp
eqMp
proveHyp
proveHyp
proveHyp
proveHyp
eqMp
nil
127
ref
554
remove
cons
130
ref
556
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
553
remove
appTerm
thm
nil
5
ref
6
ref
9
ref
10
ref
9
ref
"s"
1
ref
var
567
def
9
ref
11
ref
9
ref
12
ref
15
ref
26
remove
20
ref
270
ref
567
ref
varTerm
568
def
appTerm
569
def
appTerm
186
ref
258
ref
42
ref
appTerm
21
ref
appTerm
570
def
appTerm
188
ref
appTerm
571
def
appTerm
572
def
appTerm
573
def
appTerm
20
ref
287
ref
43
ref
appTerm
21
ref
appTerm
574
def
appTerm
575
def
287
ref
288
ref
568
ref
appTerm
appTerm
21
ref
appTerm
576
def
appTerm
577
def
appTerm
578
def
absTerm
579
def
appTerm
580
def
absTerm
581
def
appTerm
582
def
absTerm
583
def
appTerm
584
def
absTerm
585
def
appTerm
586
def
absTerm
587
def
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
6
ref
nil
77
ref
586
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
585
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
10
ref
nil
77
ref
584
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
583
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
567
ref
nil
77
ref
582
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
581
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
11
ref
nil
77
ref
580
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
579
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
12
ref
nil
77
ref
578
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
83
ref
573
remove
nil
cons
588
def
cons
85
ref
577
remove
nil
cons
589
def
cons
nil
cons
590
def
cons
nil
cons
cons
591
def
102
ref
subst
591
remove
126
ref
subst
nil
129
remove
130
ref
572
ref
nil
cons
592
def
cons
nil
cons
cons
nil
cons
cons
593
def
142
ref
subst
593
remove
143
ref
subst
251
remove
233
remove
sym
subst
nil
83
ref
249
ref
cons
220
ref
cons
nil
cons
cons
594
def
102
ref
subst
594
remove
126
ref
subst
56
ref
"_44281"
1
ref
var
595
def
20
ref
258
ref
595
remove
varTerm
appTerm
568
ref
appTerm
appTerm
571
ref
appTerm
absTerm
596
def
27
ref
appTerm
597
def
appTerm
refl
596
ref
23
ref
appTerm
betaConv
appThm
103
ref
597
remove
betaConv
appThm
20
ref
258
ref
23
ref
appTerm
598
def
568
ref
appTerm
appTerm
571
ref
appTerm
599
def
refl
appThm
trans
596
remove
refl
28
ref
assume
appThm
eqMp
572
ref
assume
600
def
eqMp
nil
83
ref
599
remove
nil
cons
601
def
cons
220
ref
cons
nil
cons
cons
167
ref
subst
proveHyp
nil
77
ref
601
remove
cons
nil
cons
nil
cons
cons
77
ref
56
ref
15
ref
78
ref
appTerm
602
def
213
ref
appTerm
appTerm
17
ref
78
ref
appTerm
603
def
appTerm
absTerm
604
def
78
ref
appTerm
605
def
betaConv
nil
238
ref
604
ref
appTerm
606
def
axiom
nil
83
ref
606
remove
nil
cons
cons
85
ref
605
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
240
ref
241
ref
604
remove
nil
cons
cons
268
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
607
def
subst
211
ref
20
ref
refl
608
def
nil
6
ref
568
ref
nil
cons
609
def
cons
610
def
nil
cons
nil
cons
cons
6
ref
20
ref
598
ref
21
ref
appTerm
appTerm
23
ref
appTerm
absTerm
611
def
21
ref
appTerm
612
def
betaConv
nil
9
ref
611
ref
appTerm
613
def
axiom
nil
83
ref
613
remove
nil
cons
cons
85
ref
612
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
611
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
614
def
subst
appThm
nil
148
ref
570
ref
nil
cons
615
def
cons
nil
cons
nil
cons
cons
148
ref
20
ref
207
remove
appTerm
184
ref
appTerm
616
def
absTerm
617
def
151
ref
appTerm
618
def
betaConv
164
ref
148
ref
616
remove
assume
sym
208
remove
assume
sym
deductAntisym
absThm
appThm
209
remove
eqMp
nil
83
ref
9
ref
617
ref
appTerm
nil
cons
cons
85
ref
618
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
617
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
appThm
nil
6
ref
615
ref
cons
619
def
nil
cons
620
def
nil
cons
cons
211
ref
20
ref
23
ref
appTerm
621
def
156
ref
appTerm
622
def
assume
sym
20
ref
156
ref
appTerm
23
ref
appTerm
623
def
assume
sym
deductAntisym
appThm
6
ref
17
ref
623
ref
appTerm
624
def
absTerm
625
def
21
ref
appTerm
626
def
betaConv
nil
9
ref
625
ref
appTerm
627
def
axiom
nil
83
ref
627
remove
nil
cons
cons
85
ref
626
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
625
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
628
def
eqMp
nil
83
ref
17
ref
622
ref
appTerm
nil
cons
cons
85
ref
56
ref
622
ref
appTerm
213
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
nil
127
ref
622
remove
nil
cons
cons
nil
cons
nil
cons
cons
244
ref
subst
eqMp
subst
trans
appThm
245
remove
trans
trans
sym
81
ref
eqMp
eqMp
eqMp
nil
250
remove
130
ref
219
remove
cons
nil
cons
629
def
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
630
def
"y"
1
ref
var
631
def
16
ref
575
ref
631
ref
varTerm
632
def
appTerm
appTerm
20
ref
632
ref
appTerm
633
def
576
ref
appTerm
appTerm
absTerm
634
def
287
ref
258
ref
43
ref
appTerm
569
ref
appTerm
appTerm
21
ref
appTerm
635
def
appTerm
betaConv
sym
148
ref
20
ref
397
ref
appTerm
636
def
287
ref
259
ref
569
ref
appTerm
appTerm
21
ref
appTerm
appTerm
637
def
absTerm
638
def
43
remove
appTerm
639
def
betaConv
nil
5
ref
638
ref
nil
cons
cons
640
def
nil
cons
nil
cons
cons
76
ref
subst
148
ref
nil
77
ref
637
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
56
ref
"_44334"
1
ref
var
641
def
636
ref
287
ref
259
ref
641
remove
varTerm
appTerm
appTerm
21
ref
appTerm
appTerm
absTerm
642
def
569
ref
appTerm
643
def
appTerm
refl
642
ref
571
ref
appTerm
betaConv
appThm
103
ref
643
remove
betaConv
appThm
636
ref
287
ref
259
ref
571
ref
appTerm
appTerm
21
ref
appTerm
appTerm
refl
appThm
trans
642
remove
refl
600
ref
appThm
eqMp
sym
636
ref
refl
644
def
287
ref
refl
645
def
nil
316
ref
192
ref
cons
620
remove
cons
nil
cons
cons
332
ref
subst
186
ref
259
ref
570
ref
appTerm
646
def
appTerm
647
def
refl
263
ref
appThm
trans
appThm
21
ref
refl
648
def
appThm
appThm
sym
6
ref
9
ref
12
ref
9
ref
494
ref
395
ref
20
ref
287
ref
186
ref
287
ref
32
ref
appTerm
649
def
21
ref
appTerm
650
def
appTerm
651
def
287
ref
495
ref
appTerm
652
def
21
ref
appTerm
appTerm
appTerm
21
ref
appTerm
653
def
appTerm
287
ref
286
ref
495
ref
appTerm
appTerm
654
def
21
ref
appTerm
655
def
appTerm
656
def
appTerm
657
def
absTerm
658
def
appTerm
659
def
absTerm
660
def
appTerm
661
def
absTerm
662
def
21
ref
appTerm
663
def
betaConv
nil
9
ref
662
ref
appTerm
664
def
axiom
665
def
nil
83
ref
664
remove
nil
cons
cons
666
def
85
ref
663
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
662
ref
nil
cons
cons
667
def
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
668
def
nil
83
ref
661
remove
nil
cons
cons
669
def
85
ref
636
ref
287
ref
647
remove
151
ref
appTerm
appTerm
21
ref
appTerm
appTerm
670
def
nil
cons
671
def
cons
nil
cons
672
def
cons
nil
cons
cons
167
ref
subst
proveHyp
221
ref
164
ref
12
ref
164
ref
494
ref
221
ref
246
remove
appThm
673
def
656
ref
refl
appThm
nil
77
ref
656
ref
nil
cons
cons
nil
cons
nil
cons
cons
77
ref
56
ref
15
ref
67
ref
appTerm
78
ref
appTerm
appTerm
78
ref
appTerm
absTerm
674
def
78
ref
appTerm
675
def
betaConv
nil
238
ref
674
ref
appTerm
676
def
axiom
nil
83
ref
676
remove
nil
cons
cons
85
ref
675
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
240
ref
241
ref
674
remove
nil
cons
cons
268
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
677
def
subst
trans
absThm
appThm
absThm
appThm
appThm
678
def
670
remove
refl
appThm
sym
nil
83
ref
9
ref
12
ref
9
ref
494
ref
656
ref
absTerm
appTerm
absTerm
appTerm
679
def
nil
cons
680
def
cons
681
def
672
remove
cons
nil
cons
cons
682
def
102
ref
subst
682
remove
126
ref
subst
644
ref
nil
494
ref
169
remove
cons
12
ref
646
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
494
ref
20
ref
655
remove
appTerm
653
remove
appTerm
683
def
absTerm
684
def
495
ref
appTerm
685
def
betaConv
12
ref
9
ref
684
ref
appTerm
686
def
absTerm
687
def
32
ref
appTerm
688
def
betaConv
164
ref
12
ref
164
ref
494
ref
683
remove
assume
sym
656
remove
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
679
remove
assume
eqMp
nil
83
ref
9
ref
687
ref
appTerm
nil
cons
cons
85
ref
688
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
687
remove
nil
cons
cons
313
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
686
remove
nil
cons
cons
85
ref
685
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
684
remove
nil
cons
cons
518
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
689
def
subst
appThm
sym
608
ref
645
ref
nil
317
ref
6
ref
310
remove
cons
690
def
nil
cons
cons
nil
cons
cons
316
ref
20
ref
259
ref
361
ref
appTerm
691
def
appTerm
258
ref
320
ref
appTerm
318
ref
appTerm
692
def
appTerm
693
def
absTerm
694
def
318
ref
appTerm
695
def
betaConv
6
ref
9
ref
694
ref
appTerm
696
def
absTerm
697
def
21
ref
appTerm
698
def
betaConv
148
ref
9
ref
697
ref
appTerm
699
def
absTerm
700
def
151
ref
appTerm
701
def
betaConv
nil
9
ref
700
ref
appTerm
702
def
axiom
703
def
nil
83
ref
702
remove
nil
cons
cons
85
ref
701
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
700
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
699
remove
nil
cons
cons
85
ref
698
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
697
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
696
remove
nil
cons
cons
85
ref
695
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
694
remove
nil
cons
cons
331
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
704
def
subst
appThm
648
ref
appThm
appThm
nil
6
ref
23
ref
nil
cons
705
def
cons
nil
cons
nil
cons
cons
706
def
648
ref
subst
707
def
appThm
sym
608
ref
645
ref
nil
148
ref
259
remove
42
ref
appTerm
708
def
nil
cons
709
def
cons
nil
cons
nil
cons
cons
6
ref
20
ref
320
ref
appTerm
360
ref
151
ref
appTerm
appTerm
absTerm
710
def
21
ref
appTerm
711
def
betaConv
148
ref
9
ref
710
ref
appTerm
712
def
absTerm
713
def
151
ref
appTerm
714
def
betaConv
nil
9
ref
713
ref
appTerm
715
def
axiom
nil
83
ref
715
remove
nil
cons
cons
85
ref
714
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
713
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
712
remove
nil
cons
cons
85
ref
711
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
710
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
716
def
subst
appThm
648
ref
appThm
appThm
707
ref
appThm
sym
nil
212
ref
85
ref
20
ref
287
ref
360
ref
708
remove
appTerm
appTerm
21
ref
appTerm
appTerm
23
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
nil
6
ref
709
remove
cons
182
ref
cons
nil
cons
cons
148
ref
15
ref
17
ref
20
ref
151
ref
appTerm
717
def
23
ref
appTerm
718
def
appTerm
appTerm
20
ref
287
ref
320
remove
appTerm
151
ref
appTerm
appTerm
23
ref
appTerm
appTerm
719
def
absTerm
720
def
151
ref
appTerm
721
def
betaConv
6
ref
9
ref
720
ref
appTerm
722
def
absTerm
723
def
21
ref
appTerm
724
def
betaConv
nil
9
ref
148
ref
9
ref
6
ref
719
ref
absTerm
725
def
appTerm
726
def
absTerm
727
def
appTerm
728
def
axiom
nil
83
ref
728
remove
nil
cons
729
def
cons
730
def
85
ref
9
ref
723
ref
appTerm
nil
cons
731
def
cons
nil
cons
cons
nil
cons
cons
732
def
167
ref
subst
proveHyp
732
ref
102
ref
subst
732
remove
126
ref
subst
nil
5
ref
723
remove
nil
cons
cons
733
def
nil
cons
nil
cons
cons
76
ref
subst
6
ref
nil
77
ref
722
remove
nil
cons
734
def
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
720
remove
nil
cons
cons
735
def
nil
cons
nil
cons
cons
76
ref
subst
148
ref
nil
77
ref
719
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
725
ref
21
ref
appTerm
736
def
betaConv
727
ref
151
ref
appTerm
737
def
betaConv
nil
730
remove
85
ref
737
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
53
ref
5
ref
727
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
726
remove
nil
cons
cons
85
ref
736
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
725
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
127
ref
729
remove
cons
130
ref
731
ref
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
nil
83
ref
731
remove
cons
85
ref
724
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
733
remove
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
734
remove
cons
85
ref
721
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
735
remove
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
738
def
subst
eqMp
eqMp
eqMp
56
ref
"_44336"
1
ref
var
739
def
636
ref
287
ref
186
ref
739
remove
varTerm
appTerm
397
ref
appTerm
appTerm
21
ref
appTerm
appTerm
absTerm
740
def
287
ref
646
remove
appTerm
21
ref
appTerm
741
def
appTerm
742
def
appTerm
refl
740
ref
23
ref
appTerm
betaConv
appThm
103
ref
742
remove
betaConv
appThm
636
ref
287
ref
186
ref
23
ref
appTerm
743
def
397
ref
appTerm
appTerm
21
ref
appTerm
appTerm
refl
appThm
trans
740
remove
refl
20
ref
741
remove
appTerm
23
ref
appTerm
assume
appThm
eqMp
sym
644
remove
645
ref
nil
6
ref
397
ref
nil
cons
744
def
cons
nil
cons
nil
cons
cons
6
ref
20
ref
743
remove
21
ref
appTerm
appTerm
21
ref
appTerm
absTerm
745
def
21
ref
appTerm
746
def
betaConv
nil
9
ref
745
ref
appTerm
747
def
axiom
nil
83
ref
747
remove
nil
cons
cons
85
ref
746
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
745
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
appThm
648
ref
appThm
appThm
sym
nil
212
ref
85
ref
20
ref
287
ref
397
ref
appTerm
21
ref
appTerm
748
def
appTerm
397
ref
appTerm
749
def
nil
cons
750
def
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
148
ref
395
ref
749
remove
appTerm
751
def
absTerm
752
def
151
ref
appTerm
753
def
betaConv
6
ref
9
ref
752
ref
appTerm
754
def
absTerm
755
def
21
ref
appTerm
756
def
betaConv
nil
9
ref
755
ref
appTerm
757
def
axiom
758
def
nil
83
ref
757
remove
nil
cons
cons
759
def
85
ref
756
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
755
ref
nil
cons
cons
760
def
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
754
remove
nil
cons
cons
85
ref
753
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
752
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
761
def
eqMp
nil
83
ref
750
remove
cons
85
ref
636
remove
748
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
nil
168
ref
748
remove
nil
cons
cons
631
ref
744
remove
cons
nil
cons
cons
nil
cons
cons
55
ref
66
ref
15
ref
18
remove
0
ref
57
ref
58
ref
nil
cons
762
def
cons
opType
constTerm
763
def
172
ref
appTerm
764
def
"y"
57
ref
var
765
def
varTerm
766
def
appTerm
767
def
appTerm
763
ref
766
ref
appTerm
768
def
172
ref
appTerm
appTerm
769
def
absTerm
770
def
172
ref
appTerm
771
def
betaConv
765
ref
60
ref
770
ref
appTerm
772
def
absTerm
773
def
766
ref
appTerm
774
def
betaConv
nil
60
ref
66
ref
60
ref
765
ref
769
ref
absTerm
775
def
appTerm
776
def
absTerm
777
def
appTerm
778
def
axiom
nil
83
ref
778
remove
nil
cons
779
def
cons
780
def
85
ref
60
ref
773
ref
appTerm
nil
cons
781
def
cons
nil
cons
cons
nil
cons
cons
782
def
167
ref
subst
proveHyp
782
ref
102
ref
subst
782
remove
126
ref
subst
nil
61
ref
773
remove
nil
cons
cons
783
def
nil
cons
nil
cons
cons
75
ref
subst
765
ref
nil
77
ref
772
remove
nil
cons
784
def
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
61
ref
770
remove
nil
cons
cons
785
def
nil
cons
nil
cons
cons
75
ref
subst
66
ref
nil
77
ref
769
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
775
ref
766
ref
appTerm
786
def
betaConv
777
ref
172
ref
appTerm
787
def
betaConv
nil
780
remove
85
ref
787
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
423
ref
61
ref
777
remove
nil
cons
cons
424
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
776
remove
nil
cons
cons
85
ref
786
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
423
ref
61
ref
775
remove
nil
cons
cons
66
ref
766
ref
nil
cons
cons
nil
cons
788
def
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
127
ref
779
remove
cons
130
ref
781
ref
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
nil
83
ref
781
remove
cons
85
ref
774
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
423
ref
783
remove
788
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
784
remove
cons
85
ref
771
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
423
ref
785
remove
424
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
subst
eqMp
eqMp
eqMp
proveHyp
eqMp
eqMp
nil
127
ref
680
remove
cons
789
def
130
ref
671
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
absThm
eqMp
nil
83
ref
9
ref
638
remove
appTerm
nil
cons
cons
85
ref
639
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
640
remove
168
ref
149
remove
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
575
remove
635
ref
appTerm
nil
cons
cons
85
ref
20
ref
635
ref
appTerm
576
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
126
ref
subst
proveHyp
608
ref
645
ref
nil
316
ref
609
ref
cons
790
def
356
ref
150
remove
cons
cons
nil
cons
cons
704
ref
subst
258
ref
refl
791
def
791
ref
314
ref
appThm
27
ref
refl
792
def
appThm
appThm
568
ref
refl
appThm
trans
appThm
648
ref
appThm
appThm
576
ref
refl
appThm
sym
6
ref
9
ref
148
ref
9
ref
316
ref
395
ref
20
ref
287
ref
258
ref
397
ref
appTerm
287
ref
318
ref
appTerm
793
def
21
ref
appTerm
appTerm
appTerm
21
ref
appTerm
794
def
appTerm
287
ref
321
ref
appTerm
795
def
21
ref
appTerm
796
def
appTerm
797
def
appTerm
absTerm
appTerm
absTerm
appTerm
798
def
absTerm
799
def
21
ref
appTerm
800
def
betaConv
nil
9
ref
799
ref
appTerm
801
def
axiom
802
def
nil
83
ref
801
remove
nil
cons
cons
803
def
85
ref
800
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
799
ref
nil
cons
cons
804
def
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
798
remove
nil
cons
cons
85
ref
20
ref
287
ref
258
ref
258
ref
296
ref
appTerm
27
ref
appTerm
805
def
appTerm
568
ref
appTerm
appTerm
21
ref
appTerm
appTerm
576
ref
appTerm
806
def
nil
cons
807
def
cons
nil
cons
808
def
cons
nil
cons
cons
167
ref
subst
proveHyp
221
ref
164
ref
148
ref
164
ref
316
ref
673
remove
797
ref
refl
appThm
nil
77
ref
797
ref
nil
cons
cons
nil
cons
nil
cons
cons
677
ref
subst
trans
absThm
appThm
absThm
appThm
appThm
806
remove
refl
appThm
sym
nil
83
ref
9
ref
148
ref
9
ref
316
ref
797
ref
absTerm
appTerm
absTerm
appTerm
809
def
nil
cons
810
def
cons
808
remove
cons
nil
cons
cons
811
def
102
ref
subst
811
remove
126
ref
subst
608
ref
nil
790
ref
148
ref
805
ref
nil
cons
cons
nil
cons
812
def
cons
nil
cons
cons
316
ref
20
ref
796
remove
appTerm
794
remove
appTerm
813
def
absTerm
814
def
318
ref
appTerm
815
def
betaConv
148
ref
9
ref
814
ref
appTerm
816
def
absTerm
817
def
151
ref
appTerm
818
def
betaConv
164
ref
148
ref
164
ref
316
ref
813
remove
assume
sym
797
remove
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
809
remove
assume
eqMp
nil
83
ref
9
ref
817
ref
appTerm
nil
cons
cons
85
ref
818
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
817
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
816
remove
nil
cons
cons
85
ref
815
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
814
remove
nil
cons
cons
331
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
819
def
subst
appThm
nil
790
remove
342
ref
cons
nil
cons
cons
819
remove
subst
appThm
sym
645
ref
791
ref
333
ref
15
ref
17
ref
20
ref
334
ref
appTerm
23
ref
appTerm
appTerm
appTerm
820
def
20
ref
186
ref
258
ref
295
remove
334
ref
appTerm
appTerm
334
ref
appTerm
appTerm
287
ref
294
ref
appTerm
821
def
334
ref
appTerm
822
def
appTerm
appTerm
294
ref
appTerm
appTerm
absTerm
823
def
27
ref
appTerm
824
def
betaConv
148
ref
9
ref
6
ref
395
ref
20
ref
186
ref
258
ref
285
ref
151
ref
appTerm
21
ref
appTerm
appTerm
21
ref
appTerm
appTerm
397
remove
appTerm
appTerm
151
ref
appTerm
appTerm
absTerm
appTerm
absTerm
825
def
294
ref
appTerm
826
def
betaConv
nil
9
ref
825
ref
appTerm
827
def
axiom
828
def
nil
83
ref
827
remove
nil
cons
cons
829
def
85
ref
826
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
825
ref
nil
cons
cons
830
def
168
ref
429
remove
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
9
ref
823
ref
appTerm
nil
cons
cons
85
ref
824
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
823
remove
nil
cons
cons
309
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
831
def
nil
83
ref
15
ref
29
remove
appTerm
832
def
20
ref
186
ref
805
ref
appTerm
833
def
821
ref
27
ref
appTerm
834
def
appTerm
appTerm
294
ref
appTerm
835
def
appTerm
nil
cons
cons
836
def
85
ref
20
ref
287
ref
805
ref
appTerm
21
ref
appTerm
appTerm
650
ref
appTerm
837
def
nil
cons
838
def
cons
nil
cons
839
def
cons
nil
cons
cons
167
ref
subst
proveHyp
221
ref
221
ref
253
remove
appThm
840
def
835
ref
refl
appThm
nil
77
ref
835
remove
nil
cons
cons
nil
cons
nil
cons
cons
677
ref
subst
trans
appThm
837
ref
refl
841
def
appThm
sym
630
ref
755
remove
27
ref
appTerm
842
def
betaConv
758
remove
nil
759
remove
85
ref
842
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
760
remove
309
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
9
ref
148
ref
832
ref
20
ref
287
ref
396
remove
27
ref
appTerm
843
def
appTerm
27
ref
appTerm
appTerm
843
ref
appTerm
844
def
appTerm
absTerm
appTerm
845
def
nil
cons
cons
85
ref
20
ref
834
ref
appTerm
23
ref
appTerm
846
def
nil
cons
847
def
cons
nil
cons
848
def
cons
nil
cons
cons
167
ref
subst
proveHyp
799
remove
27
ref
appTerm
849
def
betaConv
802
remove
nil
803
remove
85
ref
849
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
804
remove
309
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
850
def
nil
83
ref
9
ref
148
ref
9
ref
316
ref
832
ref
20
ref
287
ref
258
ref
843
remove
appTerm
793
remove
27
ref
appTerm
851
def
appTerm
appTerm
27
ref
appTerm
852
def
appTerm
795
remove
27
ref
appTerm
853
def
appTerm
854
def
appTerm
absTerm
appTerm
absTerm
855
def
appTerm
856
def
nil
cons
cons
857
def
85
ref
15
ref
845
remove
appTerm
846
ref
appTerm
858
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
662
remove
27
ref
appTerm
859
def
betaConv
665
remove
nil
666
remove
85
ref
859
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
667
remove
309
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
9
ref
12
ref
9
ref
494
ref
832
ref
20
ref
287
ref
186
ref
649
ref
27
ref
appTerm
860
def
appTerm
861
def
652
ref
27
ref
appTerm
862
def
appTerm
appTerm
27
ref
appTerm
863
def
appTerm
654
remove
27
ref
appTerm
864
def
appTerm
865
def
appTerm
absTerm
appTerm
absTerm
appTerm
nil
cons
cons
85
ref
15
ref
856
remove
appTerm
858
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
221
ref
164
ref
12
ref
164
ref
494
ref
840
ref
865
ref
refl
appThm
nil
77
ref
865
ref
nil
cons
cons
nil
cons
nil
cons
cons
677
ref
subst
trans
absThm
appThm
absThm
appThm
appThm
221
ref
164
ref
148
ref
164
ref
316
ref
840
ref
854
ref
refl
appThm
nil
77
ref
854
ref
nil
cons
cons
nil
cons
nil
cons
cons
677
ref
subst
trans
absThm
appThm
absThm
appThm
appThm
221
ref
164
ref
148
ref
840
ref
844
ref
refl
appThm
nil
77
ref
844
ref
nil
cons
cons
nil
cons
nil
cons
cons
677
ref
subst
trans
absThm
appThm
appThm
846
ref
refl
866
def
appThm
appThm
appThm
sym
nil
83
ref
9
ref
12
ref
9
ref
494
ref
865
ref
absTerm
867
def
appTerm
868
def
absTerm
869
def
appTerm
870
def
nil
cons
871
def
cons
872
def
85
ref
15
ref
9
ref
148
ref
9
ref
316
ref
854
ref
absTerm
873
def
appTerm
874
def
absTerm
875
def
appTerm
876
def
appTerm
877
def
15
ref
9
ref
148
ref
844
remove
absTerm
878
def
appTerm
879
def
appTerm
880
def
846
ref
appTerm
appTerm
nil
cons
881
def
cons
nil
cons
cons
nil
cons
cons
882
def
102
ref
subst
882
remove
126
ref
subst
877
remove
refl
880
ref
refl
883
def
608
ref
nil
494
ref
341
ref
cons
nil
cons
nil
cons
cons
884
def
494
ref
20
ref
864
remove
appTerm
863
remove
appTerm
885
def
absTerm
886
def
495
ref
appTerm
887
def
betaConv
12
ref
9
ref
886
ref
appTerm
888
def
absTerm
889
def
32
ref
appTerm
890
def
betaConv
164
ref
12
ref
164
ref
494
ref
885
remove
assume
sym
865
remove
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
870
remove
assume
eqMp
nil
83
ref
9
ref
889
ref
appTerm
nil
cons
cons
85
ref
890
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
889
remove
nil
cons
cons
313
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
888
remove
nil
cons
cons
85
ref
887
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
886
remove
nil
cons
cons
518
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
appThm
707
ref
appThm
appThm
appThm
sym
nil
83
ref
876
ref
nil
cons
891
def
cons
892
def
85
ref
880
remove
20
ref
287
ref
861
ref
287
ref
293
ref
appTerm
893
def
27
ref
appTerm
894
def
appTerm
895
def
appTerm
27
ref
appTerm
896
def
appTerm
897
def
23
ref
appTerm
898
def
appTerm
nil
cons
899
def
cons
nil
cons
cons
nil
cons
cons
900
def
102
ref
subst
900
remove
126
ref
subst
883
remove
608
ref
645
ref
861
ref
refl
901
def
nil
359
remove
nil
cons
cons
316
ref
20
ref
853
remove
appTerm
852
remove
appTerm
902
def
absTerm
903
def
318
ref
appTerm
904
def
betaConv
148
ref
9
ref
903
ref
appTerm
905
def
absTerm
906
def
151
ref
appTerm
907
def
betaConv
164
ref
148
ref
164
ref
316
ref
902
remove
assume
sym
854
remove
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
876
remove
assume
eqMp
nil
83
ref
9
ref
906
ref
appTerm
nil
cons
cons
85
ref
907
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
906
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
905
remove
nil
cons
cons
85
ref
904
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
903
remove
nil
cons
cons
331
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
appThm
appThm
792
ref
appThm
appThm
707
ref
appThm
appThm
sym
nil
83
ref
879
remove
nil
cons
908
def
cons
909
def
85
ref
20
ref
287
ref
861
ref
287
ref
258
ref
287
ref
291
ref
appTerm
27
ref
appTerm
910
def
appTerm
911
def
287
ref
21
ref
appTerm
912
def
27
ref
appTerm
913
def
appTerm
appTerm
27
ref
appTerm
914
def
appTerm
915
def
appTerm
27
ref
appTerm
appTerm
23
ref
appTerm
nil
cons
916
def
cons
nil
cons
cons
nil
cons
cons
917
def
102
ref
subst
917
remove
126
ref
subst
608
ref
645
ref
901
ref
645
ref
791
ref
nil
394
ref
nil
cons
cons
878
ref
151
ref
appTerm
918
def
betaConv
nil
909
remove
85
ref
918
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
53
ref
5
ref
878
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
appThm
913
ref
refl
appThm
appThm
792
ref
appThm
appThm
appThm
792
ref
appThm
appThm
707
ref
appThm
sym
608
ref
645
ref
901
ref
nil
317
ref
394
remove
cons
nil
cons
cons
873
ref
318
ref
appTerm
919
def
betaConv
875
ref
151
ref
appTerm
920
def
betaConv
nil
892
remove
85
ref
920
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
53
ref
5
ref
875
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
874
remove
nil
cons
cons
85
ref
919
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
873
remove
nil
cons
cons
331
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
appThm
appThm
792
ref
appThm
appThm
707
ref
appThm
sym
608
ref
nil
494
ref
258
ref
289
ref
appTerm
921
def
21
ref
appTerm
922
def
nil
cons
cons
nil
cons
nil
cons
cons
867
ref
495
ref
appTerm
923
def
betaConv
869
ref
32
ref
appTerm
924
def
betaConv
nil
872
remove
85
ref
924
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
53
ref
5
ref
869
remove
nil
cons
cons
313
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
868
remove
nil
cons
cons
85
ref
923
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
867
remove
nil
cons
cons
518
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
appThm
707
ref
appThm
sym
20
ref
286
ref
922
ref
appTerm
925
def
appTerm
926
def
refl
nil
316
ref
615
remove
cons
193
remove
342
ref
cons
cons
nil
cons
cons
332
remove
subst
186
ref
refl
927
def
nil
342
ref
nil
cons
cons
928
def
263
remove
subst
appThm
nil
317
remove
690
remove
342
ref
cons
cons
nil
cons
cons
929
def
704
remove
subst
appThm
trans
appThm
nil
168
ref
925
ref
nil
cons
cons
nil
cons
nil
cons
cons
55
ref
nil
77
ref
764
ref
172
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
176
remove
eqMp
subst
930
def
subst
trans
sym
81
ref
eqMp
56
ref
"_44271"
1
ref
var
931
def
20
ref
287
ref
931
remove
varTerm
appTerm
27
ref
appTerm
appTerm
23
ref
appTerm
absTerm
932
def
925
remove
appTerm
933
def
appTerm
refl
932
ref
288
ref
189
remove
570
ref
appTerm
appTerm
934
def
appTerm
betaConv
appThm
103
ref
933
remove
betaConv
appThm
20
ref
287
ref
934
ref
appTerm
27
ref
appTerm
appTerm
23
ref
appTerm
refl
appThm
trans
932
remove
refl
926
remove
934
remove
appTerm
assume
appThm
eqMp
sym
608
ref
645
ref
288
ref
refl
nil
619
remove
271
remove
cons
nil
cons
cons
206
ref
subst
appThm
appThm
792
ref
appThm
appThm
707
ref
appThm
sym
56
ref
"_44273"
1
ref
var
935
def
20
ref
287
ref
288
ref
935
remove
varTerm
appTerm
appTerm
27
ref
appTerm
appTerm
23
ref
appTerm
absTerm
936
def
571
ref
appTerm
937
def
appTerm
refl
936
ref
569
ref
appTerm
betaConv
appThm
103
ref
937
remove
betaConv
appThm
20
ref
287
ref
288
ref
569
ref
appTerm
appTerm
27
ref
appTerm
appTerm
23
ref
appTerm
refl
appThm
trans
936
remove
refl
600
ref
sym
appThm
eqMp
sym
608
ref
645
ref
nil
6
ref
569
remove
nil
cons
cons
342
ref
cons
nil
cons
cons
716
ref
subst
appThm
792
ref
appThm
appThm
707
ref
appThm
sym
608
ref
645
ref
nil
316
ref
312
remove
cons
610
remove
256
ref
cons
cons
nil
cons
cons
316
ref
20
ref
692
remove
appTerm
691
remove
appTerm
938
def
absTerm
939
def
318
ref
appTerm
940
def
betaConv
6
ref
9
ref
939
ref
appTerm
941
def
absTerm
942
def
21
ref
appTerm
943
def
betaConv
148
ref
9
ref
942
ref
appTerm
944
def
absTerm
945
def
151
ref
appTerm
946
def
betaConv
164
ref
148
ref
164
ref
6
ref
164
ref
316
ref
938
remove
assume
sym
693
remove
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
absThm
appThm
703
remove
eqMp
nil
83
ref
9
ref
945
ref
appTerm
nil
cons
cons
85
ref
946
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
945
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
944
remove
nil
cons
cons
85
ref
943
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
942
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
941
remove
nil
cons
cons
85
ref
940
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
939
remove
nil
cons
cons
331
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
947
def
subst
appThm
792
ref
appThm
appThm
707
ref
appThm
sym
nil
248
ref
85
ref
20
ref
287
ref
270
remove
258
ref
568
ref
appTerm
32
ref
appTerm
948
def
appTerm
appTerm
27
ref
appTerm
appTerm
23
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
nil
6
ref
948
remove
nil
cons
cons
256
ref
cons
nil
cons
cons
738
ref
subst
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
proveHyp
eqMp
eqMp
eqMp
eqMp
nil
127
ref
908
remove
cons
130
ref
916
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
127
ref
891
remove
cons
130
ref
899
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
127
ref
871
remove
cons
130
ref
881
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
proveHyp
949
def
56
ref
"_44338"
1
ref
var
950
def
15
ref
20
ref
833
ref
950
remove
varTerm
appTerm
appTerm
294
ref
appTerm
appTerm
837
ref
appTerm
absTerm
951
def
834
ref
appTerm
952
def
appTerm
refl
951
ref
23
ref
appTerm
betaConv
appThm
103
ref
952
remove
betaConv
appThm
15
ref
20
ref
833
ref
23
ref
appTerm
appTerm
294
ref
appTerm
appTerm
837
remove
appTerm
refl
appThm
trans
951
remove
refl
846
ref
assume
953
def
appThm
eqMp
sym
221
ref
608
ref
nil
812
remove
nil
cons
cons
148
ref
20
ref
195
ref
23
ref
appTerm
appTerm
151
ref
appTerm
absTerm
954
def
151
ref
appTerm
955
def
betaConv
nil
9
ref
954
ref
appTerm
956
def
axiom
nil
83
ref
956
remove
nil
cons
cons
85
ref
955
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
954
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
957
def
subst
958
def
appThm
294
ref
refl
959
def
appThm
appThm
841
remove
appThm
sym
nil
83
ref
20
ref
805
ref
appTerm
960
def
294
ref
appTerm
961
def
nil
cons
962
def
cons
963
def
839
remove
cons
nil
cons
cons
964
def
102
ref
subst
964
remove
126
ref
subst
56
ref
"_44340"
1
ref
var
965
def
20
ref
287
ref
965
remove
varTerm
appTerm
21
ref
appTerm
appTerm
650
ref
appTerm
absTerm
966
def
805
ref
appTerm
967
def
appTerm
refl
966
ref
294
ref
appTerm
betaConv
appThm
103
ref
967
remove
betaConv
appThm
20
ref
821
remove
21
ref
appTerm
appTerm
650
ref
appTerm
968
def
refl
969
def
appThm
trans
966
remove
refl
961
remove
assume
970
def
appThm
eqMp
sym
668
ref
nil
669
ref
85
ref
968
remove
nil
cons
971
def
cons
nil
cons
972
def
cons
nil
cons
cons
167
ref
subst
proveHyp
678
remove
969
remove
appThm
sym
nil
681
remove
972
remove
cons
nil
cons
cons
973
def
102
ref
subst
973
remove
126
ref
subst
608
ref
884
remove
689
remove
subst
appThm
650
ref
refl
974
def
appThm
sym
608
ref
645
ref
nil
358
remove
nil
cons
cons
716
remove
subst
appThm
648
ref
appThm
appThm
707
ref
appThm
sym
nil
212
ref
85
ref
20
ref
287
ref
360
remove
291
ref
appTerm
appTerm
21
ref
appTerm
appTerm
23
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
nil
6
ref
357
ref
cons
182
remove
cons
nil
cons
cons
738
remove
subst
eqMp
eqMp
56
ref
"_44342"
1
ref
var
975
def
20
ref
287
ref
651
ref
975
remove
varTerm
appTerm
appTerm
21
ref
appTerm
appTerm
650
ref
appTerm
absTerm
976
def
893
ref
21
ref
appTerm
977
def
appTerm
978
def
appTerm
refl
976
ref
23
ref
appTerm
betaConv
appThm
103
ref
978
remove
betaConv
appThm
20
ref
287
ref
651
remove
23
ref
appTerm
appTerm
21
ref
appTerm
appTerm
650
ref
appTerm
refl
appThm
trans
976
remove
refl
20
ref
977
remove
appTerm
23
ref
appTerm
assume
appThm
eqMp
sym
608
ref
645
ref
nil
148
ref
650
ref
nil
cons
cons
nil
cons
nil
cons
cons
957
ref
subst
appThm
648
ref
appThm
appThm
974
remove
appThm
sym
nil
212
remove
85
ref
20
ref
287
ref
650
ref
appTerm
21
ref
appTerm
appTerm
650
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
928
remove
761
ref
subst
eqMp
eqMp
eqMp
proveHyp
eqMp
eqMp
nil
789
remove
130
ref
971
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
nil
127
ref
962
ref
cons
979
def
130
ref
838
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
proveHyp
eqMp
eqMp
appThm
287
ref
568
ref
appTerm
21
ref
appTerm
refl
appThm
appThm
648
ref
appThm
eqMp
eqMp
nil
127
ref
810
remove
cons
130
ref
807
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
53
ref
5
ref
634
ref
nil
cons
cons
168
ref
635
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
427
ref
subst
proveHyp
nil
83
ref
428
ref
634
remove
appTerm
nil
cons
cons
590
remove
cons
nil
cons
cons
167
ref
subst
proveHyp
nil
"z"
1
ref
var
980
def
576
remove
nil
cons
cons
168
ref
574
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
55
ref
"z"
57
ref
var
981
def
15
ref
406
remove
765
ref
16
ref
767
remove
appTerm
768
remove
981
ref
varTerm
982
def
appTerm
appTerm
983
def
absTerm
984
def
appTerm
985
def
appTerm
986
def
764
remove
982
ref
appTerm
987
def
appTerm
988
def
absTerm
989
def
982
ref
appTerm
990
def
betaConv
66
ref
60
ref
989
ref
appTerm
991
def
absTerm
992
def
172
ref
appTerm
993
def
betaConv
nil
60
ref
66
ref
60
ref
765
ref
60
ref
981
ref
15
ref
983
ref
appTerm
987
ref
appTerm
absTerm
994
def
appTerm
995
def
absTerm
996
def
appTerm
997
def
absTerm
998
def
appTerm
999
def
axiom
nil
83
ref
999
ref
nil
cons
1000
def
cons
1001
def
85
ref
60
ref
992
ref
appTerm
nil
cons
1002
def
cons
nil
cons
cons
nil
cons
cons
1003
def
167
ref
subst
proveHyp
1003
ref
102
ref
subst
1003
remove
126
ref
subst
nil
61
ref
992
remove
nil
cons
cons
1004
def
nil
cons
nil
cons
cons
75
ref
subst
66
ref
nil
77
ref
991
remove
nil
cons
1005
def
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
61
ref
989
remove
nil
cons
cons
1006
def
nil
cons
nil
cons
cons
75
ref
subst
981
remove
nil
77
ref
988
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
83
ref
985
remove
nil
cons
1007
def
cons
1008
def
85
ref
987
ref
nil
cons
1009
def
cons
nil
cons
1010
def
cons
nil
cons
cons
1011
def
102
ref
subst
1011
remove
126
ref
subst
nil
1001
ref
1010
ref
cons
nil
cons
cons
1012
def
167
ref
subst
nil
1008
remove
85
ref
15
ref
999
remove
appTerm
987
remove
appTerm
1013
def
nil
cons
1014
def
cons
nil
cons
1015
def
cons
nil
cons
cons
167
ref
subst
nil
61
ref
765
ref
15
ref
984
ref
766
ref
appTerm
1016
def
appTerm
1013
ref
appTerm
1017
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
75
remove
subst
765
ref
nil
77
ref
1017
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
83
ref
1016
ref
nil
cons
1018
def
cons
1015
ref
cons
nil
cons
cons
1019
def
102
ref
subst
1019
remove
126
ref
subst
1016
ref
betaConv
1016
remove
assume
eqMp
nil
83
ref
983
remove
nil
cons
1020
def
cons
1021
def
1015
remove
cons
nil
cons
cons
1022
def
167
ref
subst
proveHyp
1022
ref
102
ref
subst
1022
remove
126
ref
subst
1012
ref
102
ref
subst
1012
remove
126
ref
subst
nil
1021
remove
1010
remove
cons
nil
cons
cons
167
ref
subst
994
ref
982
ref
appTerm
1023
def
betaConv
996
ref
766
ref
appTerm
1024
def
betaConv
998
ref
172
ref
appTerm
1025
def
betaConv
nil
1001
remove
85
ref
1025
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
423
ref
61
ref
998
remove
nil
cons
cons
424
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
997
remove
nil
cons
cons
85
ref
1024
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
423
ref
61
ref
996
remove
nil
cons
cons
788
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
995
remove
nil
cons
cons
85
ref
1023
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
423
ref
61
ref
994
remove
nil
cons
cons
66
ref
982
remove
nil
cons
cons
nil
cons
1026
def
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
127
ref
1000
remove
cons
1027
def
130
ref
1009
remove
cons
nil
cons
1028
def
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
nil
127
ref
1020
remove
cons
130
ref
1014
remove
cons
nil
cons
1029
def
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
127
ref
1018
remove
cons
1029
ref
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
83
ref
60
ref
"x'"
57
ref
var
1030
def
15
ref
984
ref
1030
remove
varTerm
appTerm
appTerm
1013
ref
appTerm
absTerm
appTerm
nil
cons
cons
85
ref
986
remove
1013
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
423
ref
61
ref
984
remove
nil
cons
cons
1029
remove
cons
nil
cons
cons
491
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
127
ref
1007
remove
cons
1028
remove
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
1027
remove
130
ref
1002
ref
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
nil
83
ref
1002
remove
cons
85
ref
993
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
423
ref
1004
remove
424
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1005
remove
cons
85
ref
990
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
423
ref
1006
remove
1026
remove
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
1031
def
subst
eqMp
proveHyp
proveHyp
proveHyp
eqMp
nil
127
ref
588
remove
cons
130
ref
589
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
587
remove
appTerm
thm
nil
5
ref
6
ref
9
ref
10
ref
9
ref
567
ref
9
ref
11
ref
9
ref
12
ref
15
ref
572
ref
appTerm
1032
def
284
remove
186
ref
285
ref
32
ref
appTerm
1033
def
27
ref
appTerm
1034
def
appTerm
186
ref
285
ref
293
ref
appTerm
1035
def
27
ref
appTerm
1036
def
appTerm
"Data.Bool.cond"
const
1037
def
0
ref
2
ref
40
remove
cons
opType
constTerm
1038
def
20
ref
287
ref
288
remove
570
remove
appTerm
1039
def
appTerm
1040
def
27
ref
appTerm
1041
def
appTerm
23
ref
appTerm
1042
def
appTerm
23
ref
appTerm
188
ref
appTerm
1043
def
appTerm
1044
def
appTerm
1045
def
appTerm
1046
def
appTerm
1047
def
absTerm
1048
def
appTerm
1049
def
absTerm
1050
def
appTerm
1051
def
absTerm
1052
def
appTerm
1053
def
absTerm
1054
def
appTerm
1055
def
absTerm
1056
def
nil
cons
cons
1057
def
nil
cons
nil
cons
cons
76
ref
subst
6
ref
nil
77
ref
1055
remove
nil
cons
1058
def
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
1054
ref
nil
cons
cons
1059
def
nil
cons
nil
cons
cons
76
ref
subst
10
ref
nil
77
ref
1053
remove
nil
cons
1060
def
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
1052
ref
nil
cons
cons
1061
def
nil
cons
nil
cons
cons
76
ref
subst
567
ref
nil
77
ref
1051
remove
nil
cons
1062
def
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
1050
ref
nil
cons
cons
1063
def
nil
cons
nil
cons
cons
76
ref
subst
11
ref
nil
77
ref
1049
remove
nil
cons
1064
def
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
1048
ref
nil
cons
cons
1065
def
nil
cons
nil
cons
cons
76
ref
subst
12
ref
nil
77
ref
1047
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
83
ref
592
ref
cons
1066
def
85
ref
1046
ref
nil
cons
1067
def
cons
nil
cons
1068
def
cons
nil
cons
cons
1069
def
102
ref
subst
1069
ref
126
ref
subst
608
ref
314
remove
appThm
1045
ref
refl
appThm
sym
630
remove
nil
248
ref
85
ref
20
ref
296
ref
appTerm
1045
ref
appTerm
1070
def
nil
cons
1071
def
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
nil
316
ref
255
ref
cons
1072
def
6
ref
1045
remove
nil
cons
cons
148
ref
296
remove
nil
cons
cons
nil
cons
cons
cons
nil
cons
cons
316
ref
56
ref
"Data.Bool.\\/"
const
14
remove
constTerm
1073
def
717
ref
21
ref
appTerm
1074
def
appTerm
364
ref
appTerm
1075
def
appTerm
20
ref
321
ref
appTerm
361
ref
appTerm
1076
def
appTerm
1077
def
absTerm
1078
def
318
ref
appTerm
1079
def
betaConv
6
ref
9
ref
1078
ref
appTerm
1080
def
absTerm
1081
def
21
ref
appTerm
1082
def
betaConv
148
ref
9
ref
1081
ref
appTerm
1083
def
absTerm
1084
def
151
ref
appTerm
1085
def
betaConv
164
ref
148
ref
164
ref
6
ref
164
ref
316
ref
1077
remove
assume
sym
56
ref
1076
remove
appTerm
1075
remove
appTerm
1086
def
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
absThm
appThm
nil
9
ref
148
ref
9
ref
6
ref
9
ref
316
ref
1086
remove
absTerm
1087
def
appTerm
1088
def
absTerm
1089
def
appTerm
1090
def
absTerm
1091
def
appTerm
1092
def
axiom
1093
def
eqMp
nil
83
ref
9
ref
1084
ref
appTerm
nil
cons
cons
85
ref
1085
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1084
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1083
remove
nil
cons
cons
85
ref
1082
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1081
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1080
remove
nil
cons
cons
85
ref
1079
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1078
remove
nil
cons
cons
331
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
960
ref
refl
nil
1072
ref
6
ref
1044
remove
nil
cons
cons
148
ref
1034
ref
nil
cons
cons
nil
cons
cons
cons
nil
cons
cons
316
ref
20
ref
258
ref
196
ref
appTerm
318
ref
appTerm
appTerm
186
ref
321
ref
appTerm
361
ref
appTerm
appTerm
absTerm
1094
def
318
ref
appTerm
1095
def
betaConv
6
ref
9
ref
1094
ref
appTerm
1096
def
absTerm
1097
def
21
ref
appTerm
1098
def
betaConv
148
ref
9
ref
1097
ref
appTerm
1099
def
absTerm
1100
def
151
ref
appTerm
1101
def
betaConv
nil
9
ref
1100
ref
appTerm
1102
def
axiom
nil
83
ref
1102
remove
nil
cons
cons
85
ref
1101
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1100
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1099
remove
nil
cons
cons
85
ref
1098
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1097
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1096
remove
nil
cons
cons
85
ref
1095
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1094
remove
nil
cons
cons
331
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
1103
def
subst
186
ref
258
ref
1034
remove
appTerm
27
ref
appTerm
1104
def
appTerm
1105
def
refl
1106
def
nil
1072
ref
6
ref
1043
ref
nil
cons
cons
1107
def
148
ref
1036
ref
nil
cons
cons
nil
cons
cons
cons
nil
cons
cons
1103
remove
subst
appThm
trans
appThm
trans
sym
nil
1066
ref
848
remove
cons
nil
cons
cons
1108
def
102
ref
subst
1108
remove
126
ref
subst
949
remove
eqMp
nil
127
ref
592
remove
cons
1109
def
130
ref
847
ref
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
nil
83
ref
1032
remove
846
remove
appTerm
nil
cons
cons
85
ref
960
remove
1105
ref
186
ref
258
ref
1036
remove
appTerm
27
ref
appTerm
1110
def
appTerm
1111
def
258
ref
1043
ref
appTerm
27
ref
appTerm
1112
def
appTerm
1113
def
appTerm
1114
def
appTerm
1115
def
nil
cons
1116
def
cons
nil
cons
1117
def
cons
nil
cons
cons
167
ref
subst
proveHyp
221
ref
221
ref
608
ref
600
remove
appThm
571
ref
refl
appThm
nil
168
ref
571
ref
nil
cons
cons
nil
cons
nil
cons
cons
930
ref
subst
trans
appThm
866
remove
appThm
nil
77
ref
847
ref
cons
nil
cons
nil
cons
cons
677
ref
subst
trans
appThm
1115
remove
refl
1118
def
appThm
sym
nil
83
ref
847
ref
cons
1117
ref
cons
nil
cons
cons
1119
def
102
ref
subst
1119
remove
126
ref
subst
831
remove
nil
836
remove
1117
ref
cons
nil
cons
cons
167
ref
subst
proveHyp
221
ref
840
ref
608
ref
833
remove
refl
953
ref
appThm
958
remove
trans
appThm
959
remove
appThm
appThm
nil
77
ref
962
remove
cons
nil
cons
nil
cons
cons
677
ref
subst
trans
appThm
1118
remove
appThm
sym
nil
963
remove
1117
remove
cons
nil
cons
cons
1120
def
102
ref
subst
1120
remove
126
ref
subst
56
ref
"_44283"
1
ref
var
1121
def
20
ref
1121
remove
varTerm
appTerm
1114
ref
appTerm
absTerm
1122
def
805
remove
appTerm
1123
def
appTerm
refl
1122
ref
294
ref
appTerm
betaConv
appThm
103
ref
1123
remove
betaConv
appThm
20
ref
294
ref
appTerm
1114
ref
appTerm
refl
appThm
trans
1122
remove
refl
970
remove
appThm
eqMp
sym
nil
333
ref
1114
ref
nil
cons
cons
430
ref
cons
nil
cons
cons
333
ref
56
ref
717
ref
334
ref
appTerm
1124
def
appTerm
20
ref
195
ref
895
ref
appTerm
appTerm
186
ref
334
ref
appTerm
895
ref
appTerm
appTerm
1125
def
appTerm
1126
def
absTerm
1127
def
334
ref
appTerm
1128
def
betaConv
148
ref
9
ref
1127
ref
appTerm
1129
def
absTerm
1130
def
151
ref
appTerm
1131
def
betaConv
164
ref
148
ref
164
ref
333
ref
1126
remove
assume
sym
56
ref
1125
remove
appTerm
1124
remove
appTerm
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
316
ref
9
ref
148
ref
9
ref
6
ref
56
ref
20
ref
343
ref
appTerm
319
ref
appTerm
appTerm
1074
remove
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
1132
def
895
ref
appTerm
1133
def
betaConv
nil
9
ref
1132
ref
appTerm
1134
def
axiom
nil
83
ref
1134
remove
nil
cons
cons
85
ref
1133
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1132
remove
nil
cons
cons
168
ref
895
ref
nil
cons
1135
def
cons
nil
cons
1136
def
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
eqMp
nil
83
ref
9
ref
1130
ref
appTerm
nil
cons
cons
85
ref
1131
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1130
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1129
remove
nil
cons
cons
85
ref
1128
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1127
remove
nil
cons
cons
168
ref
334
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
sym
631
ref
16
ref
20
ref
186
ref
294
remove
appTerm
1137
def
895
ref
appTerm
1138
def
appTerm
1139
def
632
remove
appTerm
appTerm
633
remove
186
ref
1114
remove
appTerm
895
ref
appTerm
1140
def
appTerm
appTerm
absTerm
1141
def
186
ref
186
ref
1105
remove
860
ref
appTerm
1142
def
appTerm
1111
ref
894
ref
appTerm
1143
def
appTerm
appTerm
1112
ref
appTerm
1144
def
appTerm
betaConv
sym
6
ref
395
ref
20
ref
186
ref
258
ref
1033
ref
21
ref
appTerm
appTerm
21
ref
appTerm
appTerm
650
remove
appTerm
appTerm
32
ref
appTerm
appTerm
absTerm
1145
def
27
ref
appTerm
1146
def
betaConv
825
ref
32
ref
appTerm
1147
def
betaConv
828
ref
nil
829
ref
85
ref
1147
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
830
ref
313
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
9
ref
1145
ref
appTerm
nil
cons
cons
85
ref
1146
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1145
remove
nil
cons
cons
309
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
832
ref
20
ref
1142
ref
appTerm
32
ref
appTerm
1148
def
appTerm
nil
cons
cons
85
ref
1139
ref
1144
ref
appTerm
1149
def
nil
cons
1150
def
cons
nil
cons
1151
def
cons
nil
cons
cons
167
ref
subst
proveHyp
221
ref
840
ref
1148
ref
refl
appThm
nil
77
ref
1148
ref
nil
cons
1152
def
cons
nil
cons
nil
cons
cons
677
ref
subst
trans
appThm
1149
remove
refl
appThm
sym
nil
83
ref
1152
ref
cons
1151
remove
cons
nil
cons
cons
1153
def
102
ref
subst
1153
remove
126
ref
subst
56
ref
"_44285"
1
ref
var
1154
def
1139
ref
186
ref
186
ref
1154
remove
varTerm
appTerm
1143
ref
appTerm
appTerm
1112
ref
appTerm
appTerm
absTerm
1155
def
1142
ref
appTerm
1156
def
appTerm
refl
1155
ref
32
ref
appTerm
betaConv
appThm
103
ref
1156
remove
betaConv
appThm
1139
ref
186
ref
286
ref
1143
ref
appTerm
appTerm
1112
ref
appTerm
appTerm
1157
def
refl
1158
def
appThm
trans
1155
remove
refl
1148
remove
assume
appThm
eqMp
sym
333
ref
820
ref
20
ref
186
ref
258
ref
1035
remove
334
ref
appTerm
appTerm
334
ref
appTerm
appTerm
893
remove
334
ref
appTerm
1159
def
appTerm
appTerm
293
ref
appTerm
appTerm
absTerm
1160
def
27
ref
appTerm
1161
def
betaConv
825
remove
293
ref
appTerm
1162
def
betaConv
828
remove
nil
829
remove
85
ref
1162
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
830
remove
168
ref
341
remove
cons
nil
cons
1163
def
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
9
ref
1160
ref
appTerm
nil
cons
cons
85
ref
1161
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1160
remove
nil
cons
cons
309
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
832
ref
20
ref
1143
ref
appTerm
293
ref
appTerm
1164
def
appTerm
nil
cons
cons
85
ref
1157
remove
nil
cons
1165
def
cons
nil
cons
1166
def
cons
nil
cons
cons
167
ref
subst
proveHyp
221
ref
840
ref
1164
ref
refl
appThm
nil
77
ref
1164
ref
nil
cons
1167
def
cons
nil
cons
nil
cons
cons
677
ref
subst
trans
appThm
1158
remove
appThm
sym
nil
83
ref
1167
ref
cons
1166
remove
cons
nil
cons
cons
1168
def
102
ref
subst
1168
remove
126
ref
subst
56
ref
"_44287"
1
ref
var
1169
def
1139
ref
186
ref
286
remove
1169
remove
varTerm
appTerm
appTerm
1112
ref
appTerm
appTerm
absTerm
1170
def
1143
ref
appTerm
1171
def
appTerm
refl
1170
ref
293
ref
appTerm
betaConv
appThm
103
ref
1171
remove
betaConv
appThm
1139
ref
1137
remove
1112
ref
appTerm
appTerm
refl
appThm
trans
1170
remove
refl
1164
remove
assume
appThm
eqMp
sym
nil
316
ref
1112
ref
nil
cons
1172
def
cons
1173
def
6
ref
1135
ref
cons
430
remove
cons
cons
nil
cons
cons
316
ref
56
ref
197
ref
343
remove
appTerm
appTerm
22
remove
318
ref
appTerm
appTerm
absTerm
1174
def
318
ref
appTerm
1175
def
betaConv
6
ref
9
ref
1174
ref
appTerm
1176
def
absTerm
1177
def
21
ref
appTerm
1178
def
betaConv
148
ref
9
ref
1177
ref
appTerm
1179
def
absTerm
1180
def
151
ref
appTerm
1181
def
betaConv
nil
9
ref
1180
ref
appTerm
1182
def
axiom
nil
83
ref
1182
remove
nil
cons
cons
85
ref
1181
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1180
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1179
remove
nil
cons
cons
85
ref
1178
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1177
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1176
remove
nil
cons
cons
85
ref
1175
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1174
remove
nil
cons
cons
331
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
1183
def
subst
sym
494
ref
832
ref
56
ref
"Number.Natural.divides"
const
19
remove
constTerm
1184
def
27
ref
appTerm
1185
def
495
ref
appTerm
appTerm
20
ref
862
remove
appTerm
23
ref
appTerm
appTerm
appTerm
absTerm
1186
def
895
ref
appTerm
1187
def
betaConv
12
ref
9
ref
494
ref
15
ref
17
ref
20
ref
32
ref
appTerm
23
ref
appTerm
appTerm
appTerm
56
ref
1184
remove
32
ref
appTerm
495
ref
appTerm
appTerm
1188
def
20
ref
652
remove
32
ref
appTerm
appTerm
23
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
1189
def
27
ref
appTerm
1190
def
betaConv
nil
9
ref
1189
ref
appTerm
1191
def
axiom
nil
83
ref
1191
remove
nil
cons
cons
85
ref
1190
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1189
remove
nil
cons
cons
309
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
9
ref
1186
ref
appTerm
nil
cons
cons
85
ref
1187
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1186
remove
nil
cons
cons
1136
remove
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
832
ref
56
ref
1185
ref
895
ref
appTerm
1192
def
appTerm
1193
def
898
ref
appTerm
1194
def
appTerm
nil
cons
cons
85
ref
20
ref
895
ref
appTerm
1112
ref
appTerm
1195
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
221
ref
840
ref
1194
ref
refl
appThm
nil
77
ref
1194
ref
nil
cons
cons
nil
cons
nil
cons
cons
677
ref
subst
trans
appThm
1195
ref
refl
1196
def
appThm
sym
333
ref
820
remove
20
ref
287
ref
186
ref
649
remove
334
ref
appTerm
appTerm
1159
remove
appTerm
appTerm
334
ref
appTerm
appTerm
822
remove
appTerm
appTerm
absTerm
1197
def
27
ref
appTerm
1198
def
betaConv
494
ref
9
ref
6
ref
657
ref
absTerm
1199
def
appTerm
1200
def
absTerm
1201
def
293
remove
appTerm
1202
def
betaConv
nil
5
ref
1201
ref
nil
cons
cons
1203
def
nil
cons
nil
cons
cons
76
ref
subst
494
ref
nil
77
ref
1200
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
1199
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
6
ref
nil
77
ref
657
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
658
ref
495
ref
appTerm
1204
def
betaConv
660
ref
32
ref
appTerm
1205
def
betaConv
668
remove
nil
669
remove
85
ref
1205
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
660
remove
nil
cons
cons
313
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
659
remove
nil
cons
cons
85
ref
1204
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
658
remove
nil
cons
cons
518
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
83
ref
9
ref
1201
remove
appTerm
nil
cons
cons
85
ref
1202
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
1203
remove
1163
remove
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
9
ref
1197
ref
appTerm
nil
cons
cons
85
ref
1198
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1197
remove
nil
cons
cons
309
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
832
ref
897
ref
834
remove
appTerm
appTerm
nil
cons
cons
85
ref
15
ref
1194
remove
appTerm
1195
ref
appTerm
1206
def
nil
cons
1207
def
cons
nil
cons
1208
def
cons
nil
cons
cons
167
ref
subst
proveHyp
221
ref
840
ref
897
remove
refl
953
remove
appThm
appThm
nil
77
ref
898
ref
nil
cons
1209
def
cons
nil
cons
nil
cons
cons
677
ref
subst
trans
appThm
1206
remove
refl
appThm
sym
nil
83
ref
1209
ref
cons
1208
remove
cons
nil
cons
cons
1210
def
102
ref
subst
1210
remove
126
ref
subst
56
ref
"_44289"
1
ref
var
1211
def
15
ref
1193
ref
20
ref
1211
remove
varTerm
appTerm
23
ref
appTerm
appTerm
appTerm
1195
ref
appTerm
absTerm
1212
def
896
remove
appTerm
1213
def
appTerm
refl
1212
ref
23
ref
appTerm
betaConv
appThm
103
ref
1213
remove
betaConv
appThm
15
ref
1193
ref
621
ref
23
ref
appTerm
appTerm
appTerm
1195
ref
appTerm
1214
def
refl
appThm
trans
1212
remove
refl
898
remove
assume
appThm
eqMp
sym
316
ref
832
ref
20
ref
287
ref
911
remove
851
ref
appTerm
appTerm
27
ref
appTerm
appTerm
287
ref
292
ref
318
ref
appTerm
appTerm
27
ref
appTerm
appTerm
appTerm
absTerm
1215
def
21
ref
appTerm
1216
def
betaConv
855
ref
291
ref
appTerm
1217
def
betaConv
850
ref
nil
857
ref
85
ref
1217
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
855
ref
nil
cons
cons
1218
def
168
ref
357
remove
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
9
ref
1215
ref
appTerm
nil
cons
cons
85
ref
1216
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1215
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
832
ref
20
ref
914
ref
appTerm
894
ref
appTerm
1219
def
appTerm
nil
cons
cons
85
ref
1214
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
221
ref
840
ref
1219
ref
refl
appThm
nil
77
ref
1219
ref
nil
cons
1220
def
cons
nil
cons
nil
cons
cons
677
ref
subst
trans
appThm
221
ref
1193
remove
refl
nil
168
ref
705
ref
cons
nil
cons
nil
cons
cons
930
ref
subst
1221
def
appThm
nil
77
ref
1192
ref
nil
cons
cons
nil
cons
nil
cons
cons
77
ref
56
ref
80
ref
appTerm
78
ref
appTerm
absTerm
1222
def
78
ref
appTerm
1223
def
betaConv
nil
238
ref
1222
ref
appTerm
1224
def
axiom
nil
83
ref
1224
remove
nil
cons
cons
85
ref
1223
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
240
ref
241
ref
1222
remove
nil
cons
cons
268
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
trans
appThm
1196
remove
appThm
appThm
sym
nil
83
ref
1220
ref
cons
85
ref
15
ref
1192
remove
appTerm
1195
remove
appTerm
nil
cons
1225
def
cons
nil
cons
cons
nil
cons
cons
1226
def
102
ref
subst
1226
remove
126
ref
subst
56
ref
"_44291"
1
ref
var
1227
def
15
ref
1185
ref
861
ref
1227
remove
varTerm
appTerm
1228
def
appTerm
appTerm
20
ref
1228
remove
appTerm
1112
ref
appTerm
appTerm
absTerm
1229
def
894
ref
appTerm
1230
def
appTerm
refl
1229
ref
914
remove
appTerm
betaConv
appThm
103
ref
1230
remove
betaConv
appThm
15
ref
1185
ref
915
ref
appTerm
appTerm
20
ref
915
remove
appTerm
1112
ref
appTerm
appTerm
1231
def
refl
1232
def
appThm
trans
1229
remove
refl
1233
def
1219
remove
assume
sym
appThm
eqMp
sym
6
ref
395
remove
20
ref
287
ref
290
ref
21
ref
appTerm
1234
def
appTerm
21
ref
appTerm
appTerm
1234
remove
appTerm
appTerm
absTerm
1235
def
27
ref
appTerm
1236
def
betaConv
148
ref
9
ref
6
ref
751
ref
absTerm
1237
def
appTerm
1238
def
absTerm
1239
def
289
ref
appTerm
1240
def
betaConv
nil
5
ref
1239
ref
nil
cons
cons
1241
def
nil
cons
nil
cons
cons
76
ref
subst
148
ref
nil
77
ref
1238
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
1237
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
6
ref
nil
77
ref
751
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
761
remove
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
83
ref
9
ref
1239
remove
appTerm
nil
cons
cons
85
ref
1240
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
1241
remove
168
ref
393
ref
cons
nil
cons
1242
def
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
9
ref
1235
ref
appTerm
nil
cons
cons
85
ref
1236
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1235
remove
nil
cons
cons
309
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
832
ref
20
ref
910
ref
appTerm
291
ref
appTerm
1243
def
appTerm
nil
cons
cons
85
ref
1231
remove
nil
cons
1244
def
cons
nil
cons
1245
def
cons
nil
cons
cons
167
ref
subst
proveHyp
221
ref
840
ref
1243
ref
refl
appThm
nil
77
ref
1243
ref
nil
cons
1246
def
cons
nil
cons
nil
cons
cons
677
ref
subst
trans
appThm
1232
remove
appThm
sym
nil
83
ref
1246
ref
cons
1245
remove
cons
nil
cons
cons
1247
def
102
ref
subst
1247
remove
126
ref
subst
56
ref
"_44293"
1
ref
var
1248
def
15
ref
1185
ref
861
ref
287
ref
258
ref
1248
remove
varTerm
appTerm
913
ref
appTerm
appTerm
27
ref
appTerm
appTerm
1249
def
appTerm
appTerm
20
ref
1249
remove
appTerm
1112
ref
appTerm
appTerm
absTerm
1250
def
910
remove
appTerm
1251
def
appTerm
refl
1250
ref
291
remove
appTerm
betaConv
appThm
103
ref
1251
remove
betaConv
appThm
15
ref
1185
ref
861
ref
287
ref
292
ref
913
remove
appTerm
appTerm
27
ref
appTerm
1252
def
appTerm
1253
def
appTerm
appTerm
20
ref
1253
remove
appTerm
1112
ref
appTerm
appTerm
1254
def
refl
1255
def
appThm
trans
1250
remove
refl
1243
remove
assume
appThm
eqMp
sym
316
ref
832
ref
20
ref
287
ref
292
remove
851
remove
appTerm
appTerm
27
ref
appTerm
appTerm
287
ref
921
remove
318
ref
appTerm
appTerm
27
ref
appTerm
appTerm
appTerm
absTerm
1256
def
21
ref
appTerm
1257
def
betaConv
855
remove
289
ref
appTerm
1258
def
betaConv
850
remove
nil
857
remove
85
ref
1258
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
1218
remove
1242
remove
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
9
ref
1256
ref
appTerm
nil
cons
cons
85
ref
1257
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1256
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
832
ref
20
ref
1252
ref
appTerm
287
remove
922
remove
appTerm
27
ref
appTerm
1259
def
appTerm
1260
def
appTerm
nil
cons
cons
85
ref
1254
remove
nil
cons
1261
def
cons
nil
cons
1262
def
cons
nil
cons
cons
167
ref
subst
proveHyp
221
ref
840
ref
1260
ref
refl
appThm
nil
77
ref
1260
ref
nil
cons
1263
def
cons
nil
cons
nil
cons
cons
677
ref
subst
trans
appThm
1255
remove
appThm
sym
nil
83
ref
1263
ref
cons
1262
remove
cons
nil
cons
cons
1264
def
102
ref
subst
1264
remove
126
ref
subst
56
ref
"_44295"
1
ref
var
1265
def
15
ref
1185
ref
861
ref
1265
remove
varTerm
appTerm
1266
def
appTerm
appTerm
20
ref
1266
remove
appTerm
1112
ref
appTerm
appTerm
absTerm
1267
def
1252
remove
appTerm
1268
def
appTerm
refl
1267
remove
1259
ref
appTerm
betaConv
appThm
103
ref
1268
remove
betaConv
appThm
15
ref
1185
ref
861
ref
1259
remove
appTerm
1269
def
appTerm
appTerm
20
ref
1269
remove
appTerm
1112
ref
appTerm
appTerm
refl
appThm
trans
1233
remove
1260
remove
assume
appThm
eqMp
sym
221
ref
1185
remove
refl
901
ref
645
remove
929
remove
947
remove
subst
appThm
792
ref
appThm
appThm
1270
def
appThm
appThm
608
ref
1270
remove
appThm
1112
ref
refl
1271
def
appThm
appThm
sym
221
ref
nil
494
ref
861
ref
1041
ref
appTerm
1272
def
nil
cons
1273
def
cons
493
remove
nil
cons
cons
nil
cons
cons
494
remove
1188
remove
428
ref
"c"
1
ref
var
1274
def
20
ref
258
ref
1274
ref
varTerm
appTerm
1275
def
32
ref
appTerm
appTerm
495
ref
appTerm
absTerm
appTerm
appTerm
absTerm
1276
def
495
remove
appTerm
1277
def
betaConv
12
ref
9
ref
1276
ref
appTerm
1278
def
absTerm
1279
def
32
ref
appTerm
1280
def
betaConv
nil
9
ref
1279
ref
appTerm
1281
def
axiom
nil
83
ref
1281
remove
nil
cons
cons
85
ref
1280
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1279
remove
nil
cons
cons
313
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1278
remove
nil
cons
cons
85
ref
1277
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1276
remove
nil
cons
cons
518
remove
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
appThm
20
ref
1272
ref
appTerm
1282
def
1112
ref
appTerm
1283
def
refl
appThm
sym
nil
5
ref
"q"
1
ref
var
1284
def
15
ref
1274
remove
20
ref
1275
remove
27
ref
appTerm
appTerm
1272
ref
appTerm
absTerm
1285
def
1284
ref
varTerm
1286
def
appTerm
1287
def
appTerm
1283
ref
appTerm
1288
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
1284
remove
nil
77
ref
1288
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
83
ref
1287
ref
nil
cons
1289
def
cons
85
ref
1283
ref
nil
cons
1290
def
cons
nil
cons
1291
def
cons
nil
cons
cons
1292
def
102
ref
subst
1292
remove
126
ref
subst
1287
ref
betaConv
1287
remove
assume
eqMp
nil
83
ref
20
ref
258
ref
1286
ref
appTerm
27
ref
appTerm
1293
def
appTerm
1272
ref
appTerm
1294
def
nil
cons
1295
def
cons
1291
remove
cons
nil
cons
cons
1296
def
167
ref
subst
proveHyp
1296
ref
102
ref
subst
1296
remove
126
ref
subst
608
ref
1294
remove
assume
sym
1297
def
appThm
1271
remove
appThm
nil
1107
remove
1072
ref
148
ref
1286
ref
nil
cons
1298
def
cons
nil
cons
cons
cons
nil
cons
cons
1087
ref
318
ref
appTerm
1299
def
betaConv
1089
ref
21
ref
appTerm
1300
def
betaConv
1091
ref
151
ref
appTerm
1301
def
betaConv
1093
remove
nil
83
ref
1092
remove
nil
cons
cons
85
ref
1301
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1091
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1090
remove
nil
cons
cons
85
ref
1300
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1089
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1088
remove
nil
cons
cons
85
ref
1299
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1087
remove
nil
cons
cons
331
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
1073
ref
20
ref
1286
ref
appTerm
1302
def
1043
ref
appTerm
1303
def
appTerm
refl
252
ref
appThm
nil
77
ref
1303
ref
nil
cons
1304
def
cons
nil
cons
nil
cons
cons
77
ref
56
ref
1073
ref
78
ref
appTerm
213
ref
appTerm
appTerm
78
ref
appTerm
absTerm
1305
def
78
ref
appTerm
1306
def
betaConv
nil
238
ref
1305
ref
appTerm
1307
def
axiom
nil
83
ref
1307
remove
nil
cons
cons
85
ref
1306
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
240
ref
241
ref
1305
remove
nil
cons
cons
268
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
1308
def
subst
trans
trans
trans
sym
1297
remove
nil
83
ref
1282
ref
1293
remove
appTerm
1309
def
nil
cons
cons
85
ref
1304
remove
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
148
ref
1073
ref
718
ref
appTerm
428
ref
6
ref
717
remove
156
ref
appTerm
absTerm
appTerm
appTerm
absTerm
1310
def
1286
ref
appTerm
1311
def
betaConv
nil
9
ref
1310
ref
appTerm
1312
def
axiom
1313
def
nil
83
ref
1312
remove
nil
cons
cons
1314
def
85
ref
1311
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1310
ref
nil
cons
cons
1315
def
168
ref
1298
remove
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1073
ref
1302
ref
23
ref
appTerm
1316
def
appTerm
428
ref
6
ref
1302
ref
156
ref
appTerm
absTerm
1317
def
appTerm
1318
def
appTerm
nil
cons
1319
def
cons
85
ref
15
ref
1309
remove
appTerm
1303
remove
appTerm
1320
def
nil
cons
1321
def
cons
nil
cons
1322
def
cons
nil
cons
cons
1323
def
167
ref
subst
proveHyp
1323
ref
102
ref
subst
1323
remove
126
ref
subst
nil
5
ref
"qs"
1
ref
var
1324
def
15
ref
1317
ref
1324
ref
varTerm
1325
def
appTerm
1326
def
appTerm
1320
ref
appTerm
1327
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
1324
remove
nil
77
ref
1327
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
83
ref
1326
ref
nil
cons
1328
def
cons
1322
ref
cons
nil
cons
cons
1329
def
102
ref
subst
1329
remove
126
ref
subst
1326
ref
betaConv
1326
remove
assume
eqMp
nil
83
ref
1302
remove
155
ref
1325
ref
appTerm
1330
def
appTerm
1331
def
nil
cons
1332
def
cons
1322
ref
cons
nil
cons
cons
1333
def
167
ref
subst
proveHyp
1333
ref
102
ref
subst
1333
remove
126
ref
subst
56
ref
"_44303"
1
ref
var
1334
def
15
ref
1282
ref
258
ref
1334
remove
varTerm
1335
def
appTerm
27
ref
appTerm
appTerm
appTerm
20
ref
1335
remove
appTerm
1043
ref
appTerm
appTerm
absTerm
1336
def
1286
remove
appTerm
1337
def
appTerm
refl
1338
def
1336
ref
1330
ref
appTerm
betaConv
appThm
103
ref
1337
remove
betaConv
appThm
1339
def
15
ref
1282
ref
258
ref
1330
ref
appTerm
27
ref
appTerm
appTerm
appTerm
20
ref
1330
remove
appTerm
1043
ref
appTerm
appTerm
1340
def
refl
appThm
trans
1336
remove
refl
1341
def
1331
remove
assume
appThm
eqMp
sym
1310
remove
1325
ref
appTerm
1342
def
betaConv
1313
remove
nil
1314
remove
85
ref
1342
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
1315
remove
168
ref
1325
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1073
ref
20
ref
1325
ref
appTerm
1343
def
23
ref
appTerm
1344
def
appTerm
428
ref
6
ref
1343
ref
156
ref
appTerm
absTerm
1345
def
appTerm
1346
def
appTerm
nil
cons
1347
def
cons
85
ref
1340
ref
nil
cons
1348
def
cons
nil
cons
1349
def
cons
nil
cons
cons
1350
def
167
ref
subst
proveHyp
1350
ref
102
ref
subst
1350
remove
126
ref
subst
nil
5
ref
"qss"
1
ref
var
1351
def
15
ref
1345
ref
1351
ref
varTerm
1352
def
appTerm
1353
def
appTerm
1340
ref
appTerm
1354
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
1351
remove
nil
77
ref
1354
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
83
ref
1353
ref
nil
cons
1355
def
cons
1349
ref
cons
nil
cons
cons
1356
def
102
ref
subst
1356
remove
126
ref
subst
1353
ref
betaConv
1353
remove
assume
eqMp
nil
83
ref
1343
remove
155
ref
1352
ref
appTerm
1357
def
appTerm
1358
def
nil
cons
1359
def
cons
1349
ref
cons
nil
cons
cons
1360
def
167
ref
subst
proveHyp
1360
ref
102
ref
subst
1360
remove
126
ref
subst
56
ref
"_44315"
1
ref
var
1361
def
15
ref
1282
ref
258
ref
155
ref
1361
remove
varTerm
appTerm
1362
def
appTerm
27
ref
appTerm
appTerm
appTerm
20
ref
1362
remove
appTerm
1043
ref
appTerm
appTerm
absTerm
1363
def
1325
remove
appTerm
1364
def
appTerm
refl
1365
def
1363
ref
1357
ref
appTerm
betaConv
appThm
103
ref
1364
remove
betaConv
appThm
1366
def
15
ref
1282
ref
258
ref
155
ref
1357
ref
appTerm
1367
def
appTerm
27
ref
appTerm
1368
def
appTerm
1369
def
appTerm
20
ref
1367
ref
appTerm
1043
ref
appTerm
1370
def
appTerm
refl
appThm
trans
1363
remove
refl
1371
def
1358
remove
assume
appThm
eqMp
sym
nil
83
ref
1369
ref
nil
cons
1372
def
cons
85
ref
1370
remove
nil
cons
1373
def
cons
nil
cons
cons
nil
cons
cons
1374
def
102
ref
subst
1374
remove
126
ref
subst
6
ref
17
ref
344
remove
21
ref
appTerm
appTerm
absTerm
1375
def
1368
ref
appTerm
1376
def
betaConv
nil
9
ref
1375
ref
appTerm
1377
def
axiom
nil
83
ref
1377
remove
nil
cons
cons
85
ref
1376
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1375
remove
nil
cons
cons
168
ref
1368
ref
nil
cons
1378
def
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
17
ref
153
ref
1368
ref
appTerm
1368
ref
appTerm
1379
def
appTerm
nil
cons
1380
def
cons
220
ref
cons
nil
cons
cons
167
ref
subst
proveHyp
nil
77
ref
1380
remove
cons
nil
cons
nil
cons
cons
607
ref
subst
nil
77
ref
1379
remove
nil
cons
cons
nil
cons
nil
cons
cons
77
ref
56
ref
17
ref
603
remove
appTerm
appTerm
78
ref
appTerm
absTerm
1381
def
78
ref
appTerm
1382
def
betaConv
nil
238
ref
1381
ref
appTerm
1383
def
axiom
nil
83
ref
1383
remove
nil
cons
cons
85
ref
1382
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
240
ref
241
ref
1381
remove
nil
cons
cons
268
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
1384
def
subst
trans
sym
283
ref
1369
remove
assume
sym
appThm
1368
ref
refl
1385
def
appThm
sym
333
ref
16
ref
153
ref
1272
remove
appTerm
1386
def
334
ref
appTerm
appTerm
153
ref
334
ref
appTerm
1368
ref
appTerm
appTerm
absTerm
1387
def
520
ref
1041
ref
appTerm
1388
def
appTerm
betaConv
sym
nil
1072
ref
148
ref
1041
ref
nil
cons
1389
def
cons
6
ref
860
ref
nil
cons
1390
def
cons
1391
def
nil
cons
cons
cons
nil
cons
cons
316
ref
56
ref
153
ref
199
remove
appTerm
381
remove
appTerm
appTerm
345
ref
appTerm
absTerm
1392
def
318
ref
appTerm
1393
def
betaConv
6
ref
9
ref
1392
ref
appTerm
1394
def
absTerm
1395
def
21
ref
appTerm
1396
def
betaConv
148
ref
9
ref
1395
ref
appTerm
1397
def
absTerm
1398
def
151
ref
appTerm
1399
def
betaConv
nil
9
ref
1398
ref
appTerm
1400
def
axiom
nil
83
ref
1400
remove
nil
cons
cons
85
ref
1399
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1398
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1397
remove
nil
cons
cons
85
ref
1396
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1395
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1394
remove
nil
cons
cons
85
ref
1393
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1392
remove
nil
cons
cons
331
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
sym
nil
248
ref
85
ref
153
ref
860
ref
appTerm
27
ref
appTerm
1401
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
nil
356
ref
342
remove
cons
nil
cons
cons
404
ref
subst
1402
def
eqMp
eqMp
nil
83
ref
1386
ref
1388
ref
appTerm
nil
cons
cons
85
ref
153
ref
1388
ref
appTerm
1403
def
1368
ref
appTerm
nil
cons
cons
nil
cons
1404
def
cons
nil
cons
cons
126
ref
subst
proveHyp
333
remove
16
ref
1403
ref
334
remove
appTerm
appTerm
335
remove
1368
ref
appTerm
appTerm
absTerm
1405
def
520
remove
27
ref
appTerm
1406
def
appTerm
betaConv
sym
nil
1072
ref
6
ref
1389
remove
cons
1407
def
256
ref
cons
cons
nil
cons
cons
355
remove
subst
sym
nil
248
remove
85
ref
153
ref
1041
remove
appTerm
27
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
nil
356
ref
148
ref
1039
ref
nil
cons
1408
def
cons
nil
cons
cons
nil
cons
cons
404
remove
subst
eqMp
eqMp
nil
83
ref
1403
remove
1406
ref
appTerm
nil
cons
cons
85
ref
31
ref
1406
ref
appTerm
1368
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
126
ref
subst
proveHyp
31
ref
refl
1409
def
nil
356
ref
nil
cons
nil
cons
cons
1410
def
6
ref
20
ref
561
remove
appTerm
544
remove
appTerm
1411
def
absTerm
1412
def
21
ref
appTerm
1413
def
betaConv
164
ref
6
ref
1411
remove
assume
sym
562
remove
assume
sym
deductAntisym
absThm
appThm
566
remove
eqMp
nil
83
ref
9
ref
1412
ref
appTerm
nil
cons
cons
85
ref
1413
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1412
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
appThm
1385
remove
appThm
nil
6
ref
1367
ref
nil
cons
cons
1072
remove
148
ref
543
ref
nil
cons
cons
nil
cons
cons
cons
nil
cons
cons
316
ref
56
ref
31
ref
321
remove
appTerm
361
remove
appTerm
appTerm
1073
ref
152
ref
appTerm
364
remove
appTerm
appTerm
absTerm
1414
def
318
ref
appTerm
1415
def
betaConv
6
ref
9
ref
1414
ref
appTerm
1416
def
absTerm
1417
def
21
ref
appTerm
1418
def
betaConv
148
ref
9
ref
1417
ref
appTerm
1419
def
absTerm
1420
def
151
ref
appTerm
1421
def
betaConv
nil
9
ref
1420
ref
appTerm
1422
def
axiom
nil
83
ref
1422
remove
nil
cons
cons
85
ref
1421
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1420
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1419
remove
nil
cons
cons
85
ref
1418
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1417
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1416
remove
nil
cons
cons
85
ref
1415
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1414
remove
nil
cons
cons
331
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
1073
ref
31
ref
543
ref
appTerm
1367
ref
appTerm
1423
def
appTerm
refl
252
remove
appThm
nil
77
ref
1423
remove
nil
cons
cons
nil
cons
nil
cons
cons
1308
remove
subst
trans
trans
trans
sym
1409
remove
542
ref
refl
706
ref
6
ref
20
ref
187
remove
21
ref
appTerm
appTerm
155
ref
542
ref
21
ref
appTerm
appTerm
1424
def
appTerm
absTerm
1425
def
21
ref
appTerm
1426
def
betaConv
nil
9
ref
1425
ref
appTerm
1427
def
axiom
nil
83
ref
1427
remove
nil
cons
cons
85
ref
1426
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1425
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
155
ref
refl
1428
def
nil
20
ref
542
ref
23
ref
appTerm
appTerm
23
ref
appTerm
axiom
appThm
1429
def
trans
1430
def
appThm
706
ref
6
ref
20
ref
542
remove
156
ref
appTerm
appTerm
155
ref
1424
remove
appTerm
appTerm
absTerm
1431
def
21
ref
appTerm
1432
def
betaConv
nil
9
ref
1431
ref
appTerm
1433
def
axiom
nil
83
ref
1433
remove
nil
cons
cons
85
ref
1432
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1431
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
1428
remove
1429
remove
appThm
trans
trans
appThm
1367
remove
refl
appThm
nil
6
ref
1357
remove
nil
cons
cons
148
ref
155
ref
23
ref
appTerm
1434
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
6
ref
56
ref
31
ref
184
remove
appTerm
156
remove
appTerm
appTerm
152
remove
appTerm
absTerm
1435
def
21
ref
appTerm
1436
def
betaConv
148
ref
9
ref
1435
ref
appTerm
1437
def
absTerm
1438
def
151
ref
appTerm
1439
def
betaConv
nil
9
ref
1438
ref
appTerm
1440
def
axiom
nil
83
ref
1440
remove
nil
cons
cons
85
ref
1439
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1438
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1437
remove
nil
cons
cons
85
ref
1436
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1435
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
1441
def
subst
nil
6
ref
1352
remove
nil
cons
cons
1442
def
148
ref
705
ref
cons
nil
cons
cons
nil
cons
cons
1441
remove
subst
nil
1442
remove
nil
cons
nil
cons
cons
nil
77
ref
31
remove
23
ref
appTerm
21
ref
appTerm
1443
def
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
6
ref
1443
remove
absTerm
1444
def
21
ref
appTerm
1445
def
betaConv
nil
9
ref
1444
ref
appTerm
1446
def
axiom
nil
83
ref
1446
remove
nil
cons
cons
85
ref
1445
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1444
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
eqMp
subst
trans
trans
trans
sym
81
ref
eqMp
eqMp
eqMp
eqMp
53
ref
5
ref
1405
ref
nil
cons
cons
168
ref
1406
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
427
ref
subst
proveHyp
nil
83
ref
428
ref
1405
remove
appTerm
nil
cons
cons
1404
remove
cons
nil
cons
cons
167
ref
subst
proveHyp
nil
316
ref
1378
remove
cons
1447
def
148
ref
1388
remove
nil
cons
1448
def
cons
nil
cons
cons
nil
cons
cons
492
remove
subst
eqMp
eqMp
eqMp
53
ref
5
ref
1387
ref
nil
cons
cons
168
ref
1448
remove
cons
nil
cons
cons
nil
cons
cons
427
ref
subst
proveHyp
nil
83
ref
428
ref
1387
remove
appTerm
nil
cons
cons
85
ref
1386
remove
1368
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
nil
1447
remove
148
ref
1273
remove
cons
nil
cons
cons
nil
cons
cons
316
ref
15
ref
428
ref
6
ref
363
remove
345
remove
appTerm
1449
def
absTerm
1450
def
appTerm
1451
def
appTerm
1452
def
435
ref
appTerm
1453
def
absTerm
1454
def
318
ref
appTerm
1455
def
betaConv
148
ref
9
ref
1454
ref
appTerm
1456
def
absTerm
1457
def
151
ref
appTerm
1458
def
betaConv
nil
9
ref
148
ref
9
ref
6
ref
9
ref
316
ref
15
ref
1449
ref
appTerm
435
ref
appTerm
absTerm
1459
def
appTerm
1460
def
absTerm
1461
def
appTerm
1462
def
absTerm
1463
def
appTerm
1464
def
axiom
nil
83
ref
1464
ref
nil
cons
1465
def
cons
1466
def
85
ref
9
ref
1457
ref
appTerm
nil
cons
1467
def
cons
nil
cons
cons
nil
cons
cons
1468
def
167
ref
subst
proveHyp
1468
ref
102
ref
subst
1468
remove
126
ref
subst
nil
5
ref
1457
remove
nil
cons
cons
1469
def
nil
cons
nil
cons
cons
76
ref
subst
148
ref
nil
77
ref
1456
remove
nil
cons
1470
def
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
1454
remove
nil
cons
cons
1471
def
nil
cons
nil
cons
cons
76
ref
subst
316
ref
nil
77
ref
1453
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
83
ref
1451
remove
nil
cons
1472
def
cons
1473
def
458
ref
cons
nil
cons
cons
1474
def
102
ref
subst
1474
remove
126
ref
subst
nil
1466
ref
458
ref
cons
nil
cons
cons
1475
def
167
ref
subst
nil
1473
remove
85
ref
15
ref
1464
remove
appTerm
435
remove
appTerm
1476
def
nil
cons
1477
def
cons
nil
cons
1478
def
cons
nil
cons
cons
167
ref
subst
nil
5
ref
6
ref
15
ref
1450
ref
21
ref
appTerm
1479
def
appTerm
1476
ref
appTerm
1480
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
6
ref
nil
77
ref
1480
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
83
ref
1479
ref
nil
cons
1481
def
cons
1478
ref
cons
nil
cons
cons
1482
def
102
ref
subst
1482
remove
126
ref
subst
1479
ref
betaConv
1479
remove
assume
eqMp
nil
83
ref
1449
remove
nil
cons
1483
def
cons
1484
def
1478
remove
cons
nil
cons
cons
1485
def
167
ref
subst
proveHyp
1485
ref
102
ref
subst
1485
remove
126
ref
subst
1475
ref
102
ref
subst
1475
remove
126
ref
subst
nil
1484
remove
458
remove
cons
nil
cons
cons
167
ref
subst
1459
ref
318
ref
appTerm
1486
def
betaConv
1461
ref
21
ref
appTerm
1487
def
betaConv
1463
ref
151
ref
appTerm
1488
def
betaConv
nil
1466
remove
85
ref
1488
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
53
ref
5
ref
1463
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1462
remove
nil
cons
cons
85
ref
1487
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1461
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1460
remove
nil
cons
cons
85
ref
1486
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1459
remove
nil
cons
cons
331
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
127
ref
1465
remove
cons
1489
def
475
ref
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
nil
127
ref
1483
remove
cons
130
ref
1477
remove
cons
nil
cons
1490
def
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
127
ref
1481
remove
cons
1490
ref
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
83
ref
9
ref
168
ref
15
ref
1450
ref
477
ref
appTerm
appTerm
1476
ref
appTerm
absTerm
appTerm
nil
cons
cons
85
ref
1452
remove
1476
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1450
remove
nil
cons
cons
1490
remove
cons
nil
cons
cons
491
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
127
ref
1472
remove
cons
475
remove
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
1489
remove
130
ref
1467
ref
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
nil
83
ref
1467
remove
cons
85
ref
1458
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
1469
remove
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1470
remove
cons
85
ref
1455
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
1471
remove
331
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
eqMp
eqMp
nil
127
ref
1373
ref
cons
nil
cons
nil
cons
cons
243
remove
subst
proveHyp
eqMp
nil
127
ref
1372
remove
cons
130
ref
1373
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
127
ref
1359
remove
cons
130
ref
1348
ref
cons
nil
cons
1491
def
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
127
ref
1355
remove
cons
1491
ref
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
83
ref
9
ref
168
ref
15
ref
1345
ref
477
ref
appTerm
appTerm
1340
ref
appTerm
absTerm
appTerm
nil
cons
cons
85
ref
15
ref
1346
ref
appTerm
1340
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1345
remove
nil
cons
cons
1491
ref
cons
nil
cons
cons
491
ref
subst
eqMp
nil
83
ref
1344
ref
nil
cons
1492
def
cons
1349
remove
cons
nil
cons
cons
1493
def
102
ref
subst
1493
remove
126
ref
subst
1365
remove
"_44309"
1
ref
var
1494
def
15
ref
1282
ref
258
ref
155
remove
1494
remove
varTerm
appTerm
1495
def
appTerm
27
ref
appTerm
appTerm
appTerm
20
ref
1495
remove
appTerm
1043
ref
appTerm
appTerm
absTerm
23
ref
appTerm
betaConv
appThm
1366
remove
15
ref
1282
ref
258
ref
1434
ref
appTerm
27
ref
appTerm
appTerm
appTerm
20
ref
1434
ref
appTerm
1496
def
1043
ref
appTerm
appTerm
refl
appThm
trans
1371
remove
1344
remove
assume
appThm
eqMp
sym
221
ref
1282
ref
refl
1497
def
791
ref
1496
remove
188
ref
appTerm
assume
sym
20
ref
188
ref
appTerm
1498
def
1434
remove
appTerm
assume
sym
deductAntisym
1430
ref
eqMp
1499
def
appThm
792
ref
appThm
257
remove
148
ref
20
ref
258
ref
188
ref
appTerm
151
ref
appTerm
appTerm
151
ref
appTerm
absTerm
1500
def
151
ref
appTerm
1501
def
betaConv
nil
9
ref
1500
ref
appTerm
1502
def
axiom
nil
83
ref
1502
remove
nil
cons
cons
85
ref
1501
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1500
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
trans
appThm
appThm
608
ref
1499
remove
appThm
1043
ref
refl
appThm
appThm
sym
103
ref
"_44321"
1
ref
var
1503
def
15
ref
1282
ref
27
ref
appTerm
1504
def
appTerm
1505
def
1498
ref
1503
remove
varTerm
appTerm
appTerm
absTerm
1506
def
1043
ref
appTerm
betaConv
appThm
210
remove
15
ref
1042
ref
appTerm
1507
def
refl
1506
ref
23
ref
appTerm
betaConv
appThm
appThm
15
ref
17
ref
1042
ref
appTerm
1508
def
appTerm
1509
def
refl
1506
ref
188
ref
appTerm
betaConv
appThm
appThm
appThm
nil
"_485"
1
ref
var
192
ref
cons
"_482"
1
ref
var
705
ref
cons
"_483"
2
ref
var
1510
def
1042
ref
nil
cons
1511
def
cons
nil
cons
cons
cons
nil
cons
cons
nil
"_484"
4
remove
var
1506
remove
nil
cons
cons
nil
cons
nil
cons
cons
55
ref
nil
66
ref
"_482"
57
ref
var
varTerm
nil
cons
cons
"c"
2
ref
var
1512
def
1510
remove
varTerm
nil
cons
cons
64
ref
"_484"
58
ref
var
varTerm
nil
cons
cons
765
ref
"_485"
57
ref
var
varTerm
nil
cons
cons
nil
cons
cons
cons
cons
nil
cons
cons
765
ref
56
ref
65
ref
1037
remove
0
ref
2
ref
0
ref
57
ref
0
ref
57
ref
422
remove
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
1513
def
1512
ref
varTerm
1514
def
appTerm
1515
def
172
ref
appTerm
766
ref
appTerm
appTerm
appTerm
16
ref
15
ref
1514
ref
appTerm
409
remove
appTerm
appTerm
15
ref
17
ref
1514
ref
appTerm
1516
def
appTerm
65
ref
766
ref
appTerm
appTerm
appTerm
appTerm
absTerm
1517
def
766
ref
appTerm
1518
def
betaConv
66
ref
60
ref
1517
ref
appTerm
1519
def
absTerm
1520
def
172
ref
appTerm
1521
def
betaConv
1512
ref
60
ref
1520
ref
appTerm
1522
def
absTerm
1523
def
1514
ref
appTerm
1524
def
betaConv
64
remove
238
ref
1523
ref
appTerm
1525
def
absTerm
1526
def
65
ref
appTerm
1527
def
betaConv
nil
7
remove
71
remove
constTerm
1526
ref
appTerm
1528
def
axiom
nil
83
ref
1528
remove
nil
cons
cons
85
ref
1527
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
"A"
762
remove
cons
nil
cons
"P"
59
remove
var
1526
remove
nil
cons
cons
"x"
58
remove
var
65
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1525
remove
nil
cons
cons
85
ref
1524
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
240
ref
241
ref
1523
remove
nil
cons
cons
242
ref
1514
ref
nil
cons
cons
nil
cons
1529
def
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1522
remove
nil
cons
cons
85
ref
1521
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
423
ref
61
ref
1520
remove
nil
cons
cons
424
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1519
remove
nil
cons
cons
85
ref
1518
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
423
ref
61
ref
1517
remove
nil
cons
cons
788
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
subst
subst
subst
eqMp
sym
nil
83
ref
1511
ref
cons
85
ref
1505
ref
1498
ref
23
ref
appTerm
appTerm
1530
def
nil
cons
1531
def
cons
nil
cons
cons
nil
cons
cons
1532
def
102
ref
subst
1532
remove
126
ref
subst
221
ref
608
ref
901
ref
1042
ref
assume
1533
def
appThm
nil
148
ref
1390
ref
cons
nil
cons
1534
def
nil
cons
cons
957
remove
subst
trans
appThm
792
ref
appThm
appThm
608
ref
1430
remove
appThm
707
ref
appThm
706
remove
628
remove
nil
83
ref
624
remove
nil
cons
cons
85
ref
56
ref
623
ref
appTerm
213
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
nil
127
ref
623
remove
nil
cons
cons
nil
cons
nil
cons
cons
244
remove
subst
eqMp
subst
trans
appThm
nil
77
ref
20
ref
860
ref
appTerm
1535
def
27
ref
appTerm
1536
def
nil
cons
1537
def
cons
nil
cons
nil
cons
cons
607
ref
subst
1538
def
trans
sym
1538
remove
nil
83
ref
1537
ref
cons
220
ref
cons
nil
cons
cons
1539
def
102
ref
subst
1539
remove
126
ref
subst
1402
remove
nil
83
ref
832
ref
1401
remove
appTerm
nil
cons
1540
def
cons
220
remove
cons
nil
cons
cons
167
ref
subst
proveHyp
nil
77
ref
1540
remove
cons
nil
cons
nil
cons
cons
607
ref
subst
211
remove
840
remove
283
remove
1536
remove
assume
appThm
792
remove
appThm
appThm
nil
77
ref
153
remove
27
ref
appTerm
27
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
677
ref
subst
trans
appThm
nil
356
remove
256
remove
cons
nil
cons
cons
6
ref
56
ref
17
ref
362
remove
appTerm
appTerm
382
ref
151
ref
appTerm
appTerm
absTerm
1541
def
21
ref
appTerm
1542
def
betaConv
148
ref
9
ref
1541
ref
appTerm
1543
def
absTerm
1544
def
151
ref
appTerm
1545
def
betaConv
nil
9
ref
1544
ref
appTerm
1546
def
axiom
nil
83
ref
1546
remove
nil
cons
cons
85
ref
1545
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1544
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1543
remove
nil
cons
cons
85
ref
1542
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1541
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
1410
ref
nil
77
ref
382
remove
21
ref
appTerm
1547
def
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
6
ref
1547
remove
absTerm
1548
def
21
ref
appTerm
1549
def
betaConv
nil
9
ref
1548
ref
appTerm
1550
def
axiom
nil
83
ref
1550
remove
nil
cons
cons
85
ref
1549
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1548
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
eqMp
subst
trans
trans
trans
sym
81
ref
eqMp
eqMp
eqMp
nil
127
ref
1537
remove
cons
629
remove
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
127
ref
1511
ref
cons
130
ref
1531
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
nil
83
ref
1507
remove
1530
remove
appTerm
nil
cons
cons
85
ref
1509
remove
1505
ref
1498
remove
188
ref
appTerm
appTerm
1551
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
126
ref
subst
proveHyp
nil
83
ref
1508
remove
nil
cons
1552
def
cons
85
ref
1551
remove
nil
cons
1553
def
cons
nil
cons
cons
nil
cons
cons
1554
def
102
ref
subst
1554
remove
126
ref
subst
1505
remove
refl
nil
168
ref
192
ref
cons
1555
def
nil
cons
nil
cons
cons
930
remove
subst
appThm
nil
77
ref
1504
remove
nil
cons
cons
nil
cons
nil
cons
cons
77
ref
56
ref
602
ref
67
ref
appTerm
appTerm
67
ref
appTerm
absTerm
1556
def
78
ref
appTerm
1557
def
betaConv
nil
238
ref
1556
ref
appTerm
1558
def
axiom
nil
83
ref
1558
remove
nil
cons
cons
85
ref
1557
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
240
ref
241
ref
1556
remove
nil
cons
cons
268
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
1559
def
subst
trans
sym
81
ref
eqMp
eqMp
nil
127
ref
1552
remove
cons
130
ref
1553
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
nil
127
ref
1492
remove
cons
1560
def
1491
ref
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
nil
1560
remove
130
ref
1346
remove
nil
cons
cons
"R"
2
ref
var
1561
def
1348
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
83
ref
15
ref
134
ref
appTerm
1562
def
1561
ref
varTerm
1563
def
appTerm
1564
def
nil
cons
cons
85
ref
1563
ref
nil
cons
1565
def
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
nil
83
ref
234
ref
1563
ref
appTerm
nil
cons
cons
85
ref
15
ref
1564
remove
appTerm
1563
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
"r"
2
ref
var
1566
def
15
ref
234
remove
1566
ref
varTerm
1567
def
appTerm
appTerm
1568
def
15
ref
1562
remove
1567
ref
appTerm
appTerm
1567
ref
appTerm
appTerm
absTerm
1569
def
1563
remove
appTerm
1570
def
betaConv
56
ref
1073
ref
132
ref
appTerm
1571
def
134
ref
appTerm
1572
def
appTerm
refl
85
ref
238
ref
1566
ref
1568
remove
15
ref
229
remove
1567
ref
appTerm
appTerm
1567
ref
appTerm
1573
def
appTerm
absTerm
appTerm
absTerm
134
remove
appTerm
betaConv
appThm
115
remove
1571
remove
appTerm
refl
83
ref
85
ref
238
ref
1566
remove
15
ref
89
remove
1567
remove
appTerm
appTerm
1573
remove
appTerm
absTerm
appTerm
absTerm
absTerm
1574
def
132
remove
appTerm
betaConv
appThm
nil
99
remove
1073
ref
appTerm
1574
remove
appTerm
axiom
140
remove
appThm
eqMp
137
remove
appThm
eqMp
1572
remove
assume
eqMp
nil
83
ref
238
ref
1569
ref
appTerm
nil
cons
cons
85
ref
1570
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
240
ref
241
ref
1569
remove
nil
cons
cons
242
ref
1565
remove
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
eqMp
eqMp
1575
def
subst
proveHyp
proveHyp
eqMp
nil
127
ref
1347
remove
cons
1491
remove
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
127
ref
1332
remove
cons
130
ref
1321
ref
cons
nil
cons
1576
def
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
127
ref
1328
remove
cons
1576
ref
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
83
ref
9
ref
168
ref
15
ref
1317
ref
477
ref
appTerm
appTerm
1320
ref
appTerm
absTerm
appTerm
nil
cons
cons
85
ref
15
ref
1318
ref
appTerm
1320
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1317
remove
nil
cons
cons
1576
ref
cons
nil
cons
cons
491
ref
subst
eqMp
nil
83
ref
1316
ref
nil
cons
1577
def
cons
1322
remove
cons
nil
cons
cons
1578
def
102
ref
subst
1578
remove
126
ref
subst
1338
remove
"_44297"
1
ref
var
1579
def
15
ref
1282
ref
258
ref
1579
remove
varTerm
1580
def
appTerm
27
ref
appTerm
appTerm
appTerm
20
ref
1580
remove
appTerm
1043
ref
appTerm
appTerm
absTerm
23
ref
appTerm
betaConv
appThm
1339
remove
15
ref
1282
remove
598
remove
27
ref
appTerm
appTerm
appTerm
621
ref
1043
remove
appTerm
1581
def
appTerm
refl
appThm
trans
1341
remove
1316
remove
assume
appThm
eqMp
sym
221
ref
1497
remove
1410
remove
614
remove
subst
appThm
nil
1407
remove
1534
ref
cons
nil
cons
cons
6
ref
56
ref
197
remove
23
ref
appTerm
appTerm
16
ref
718
remove
appTerm
24
remove
appTerm
appTerm
absTerm
1582
def
21
ref
appTerm
1583
def
betaConv
148
ref
9
ref
1582
ref
appTerm
1584
def
absTerm
1585
def
151
ref
appTerm
1586
def
betaConv
nil
9
ref
1585
ref
appTerm
1587
def
axiom
nil
83
ref
1587
remove
nil
cons
cons
85
ref
1586
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1585
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1584
remove
nil
cons
cons
85
ref
1583
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1582
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
trans
appThm
1581
ref
refl
appThm
sym
nil
83
ref
16
remove
1535
remove
23
ref
appTerm
1588
def
appTerm
1042
remove
appTerm
nil
cons
1589
def
cons
85
ref
1581
remove
nil
cons
1590
def
cons
nil
cons
cons
nil
cons
cons
1591
def
102
ref
subst
1591
remove
126
ref
subst
nil
127
ref
1588
remove
nil
cons
cons
130
ref
1511
remove
cons
nil
cons
cons
nil
cons
cons
143
remove
subst
621
remove
refl
1038
ref
refl
1592
def
608
ref
1533
remove
appThm
707
ref
appThm
1221
ref
trans
appThm
707
ref
appThm
194
remove
648
ref
subst
1593
def
appThm
nil
"t2"
1
ref
var
192
remove
cons
"t1"
1
remove
var
705
ref
cons
nil
cons
cons
nil
cons
cons
55
ref
"t2"
57
ref
var
1594
def
763
ref
1513
ref
67
ref
appTerm
"t1"
57
remove
var
1595
def
varTerm
1596
def
appTerm
1594
remove
varTerm
1597
def
appTerm
appTerm
1596
ref
appTerm
absTerm
1598
def
1597
ref
appTerm
1599
def
betaConv
1595
remove
60
ref
1598
ref
appTerm
1600
def
absTerm
1601
def
1596
ref
appTerm
1602
def
betaConv
nil
60
ref
1601
ref
appTerm
1603
def
axiom
nil
83
ref
1603
remove
nil
cons
cons
85
ref
1602
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
423
ref
61
ref
1601
remove
nil
cons
cons
66
ref
1596
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1600
remove
nil
cons
cons
85
ref
1599
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
423
ref
61
ref
1598
remove
nil
cons
cons
66
ref
1597
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
subst
trans
appThm
1221
remove
trans
sym
81
ref
eqMp
proveHyp
eqMp
nil
127
ref
1589
remove
cons
130
ref
1590
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
127
ref
1577
remove
cons
1604
def
1576
ref
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
nil
1604
remove
130
ref
1318
remove
nil
cons
cons
1561
ref
1321
remove
cons
nil
cons
cons
cons
nil
cons
cons
1575
ref
subst
proveHyp
proveHyp
eqMp
nil
127
ref
1319
remove
cons
1576
remove
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
nil
127
ref
1295
remove
cons
130
ref
1290
remove
cons
nil
cons
1605
def
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
127
ref
1289
remove
cons
1605
ref
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
83
ref
9
ref
168
ref
15
ref
1285
ref
477
ref
appTerm
appTerm
1283
ref
appTerm
absTerm
appTerm
nil
cons
cons
85
ref
15
ref
428
ref
1285
ref
appTerm
appTerm
1283
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1285
remove
nil
cons
cons
1605
remove
cons
nil
cons
cons
491
ref
subst
eqMp
eqMp
eqMp
eqMp
eqMp
nil
127
ref
1263
remove
cons
130
ref
1261
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
nil
127
ref
1246
remove
cons
130
ref
1244
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
nil
127
ref
1220
remove
cons
130
ref
1225
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
nil
127
ref
1209
remove
cons
130
ref
1207
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
nil
127
ref
1167
remove
cons
130
ref
1165
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
nil
127
ref
1152
remove
cons
130
ref
1150
ref
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
83
ref
1150
remove
cons
85
ref
20
ref
1144
ref
appTerm
1140
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
126
ref
subst
proveHyp
608
ref
nil
1173
ref
6
ref
1143
ref
nil
cons
cons
148
ref
1142
remove
nil
cons
cons
nil
cons
cons
cons
nil
cons
cons
316
ref
20
ref
186
ref
196
remove
appTerm
318
ref
appTerm
1606
def
appTerm
195
remove
319
remove
appTerm
1607
def
appTerm
1608
def
absTerm
1609
def
318
remove
appTerm
1610
def
betaConv
6
ref
9
ref
1609
ref
appTerm
1611
def
absTerm
1612
def
21
ref
appTerm
1613
def
betaConv
148
ref
9
ref
1612
ref
appTerm
1614
def
absTerm
1615
def
151
remove
appTerm
1616
def
betaConv
164
ref
148
ref
164
ref
6
ref
164
remove
316
ref
1608
remove
assume
sym
20
ref
1607
remove
appTerm
1606
remove
appTerm
1617
def
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
absThm
appThm
nil
9
ref
148
ref
9
ref
6
ref
9
ref
316
ref
1617
remove
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
83
ref
9
ref
1615
ref
appTerm
nil
cons
cons
85
ref
1616
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1615
remove
nil
cons
cons
170
remove
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1614
remove
nil
cons
cons
85
ref
1613
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1612
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1611
remove
nil
cons
cons
85
ref
1610
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1609
remove
nil
cons
cons
331
remove
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
1618
def
subst
nil
316
ref
186
ref
1143
remove
appTerm
1112
ref
appTerm
nil
cons
cons
1391
ref
148
ref
1104
remove
nil
cons
cons
nil
cons
1619
def
cons
cons
nil
cons
cons
1618
ref
subst
trans
1106
ref
901
remove
nil
1173
remove
6
ref
894
ref
nil
cons
1620
def
cons
148
ref
1110
remove
nil
cons
cons
nil
cons
1621
def
cons
cons
nil
cons
cons
1618
ref
subst
appThm
appThm
trans
appThm
nil
316
ref
1135
remove
cons
1622
def
6
ref
1113
remove
nil
cons
cons
1619
ref
cons
cons
nil
cons
cons
1618
ref
subst
1106
remove
nil
1622
remove
6
ref
1172
ref
cons
1623
def
1621
ref
cons
cons
nil
cons
cons
1618
ref
subst
appThm
trans
appThm
nil
316
ref
1111
ref
186
ref
1112
ref
appTerm
1624
def
895
remove
appTerm
1625
def
appTerm
1626
def
nil
cons
cons
6
ref
861
remove
1111
ref
186
ref
894
remove
appTerm
1627
def
1112
remove
appTerm
1628
def
appTerm
1629
def
appTerm
nil
cons
cons
1619
remove
cons
cons
nil
cons
cons
1183
ref
subst
trans
sym
608
ref
nil
6
ref
1629
remove
nil
cons
cons
1534
remove
cons
nil
cons
cons
206
ref
subst
appThm
1626
remove
refl
1630
def
appThm
sym
608
ref
nil
316
ref
1390
remove
cons
1631
def
6
ref
1628
remove
nil
cons
cons
1621
ref
cons
cons
nil
cons
cons
1618
ref
subst
1111
remove
refl
nil
1631
remove
1623
remove
148
ref
1620
ref
cons
nil
cons
1632
def
cons
cons
nil
cons
cons
1618
ref
subst
appThm
trans
appThm
1630
remove
appThm
nil
316
ref
1625
ref
nil
cons
cons
6
ref
1627
remove
1624
remove
860
remove
appTerm
1633
def
appTerm
nil
cons
cons
1621
remove
cons
cons
nil
cons
cons
1183
remove
subst
trans
sym
608
ref
nil
6
ref
1633
remove
nil
cons
cons
1632
remove
cons
nil
cons
cons
206
remove
subst
appThm
1625
remove
refl
appThm
sym
nil
316
remove
1620
remove
cons
1391
remove
148
remove
1172
remove
cons
nil
cons
cons
cons
nil
cons
cons
1618
remove
subst
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
53
ref
5
ref
1141
ref
nil
cons
cons
168
ref
1144
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
427
ref
subst
proveHyp
nil
83
ref
428
ref
1141
remove
appTerm
nil
cons
cons
85
ref
1139
remove
1140
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
nil
980
remove
1140
remove
nil
cons
cons
168
ref
1138
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
1031
remove
subst
eqMp
eqMp
eqMp
eqMp
nil
979
remove
130
ref
1116
remove
cons
nil
cons
1634
def
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
127
ref
847
remove
cons
1634
remove
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
83
ref
1073
ref
1070
ref
appTerm
28
remove
appTerm
nil
cons
cons
85
ref
832
remove
1070
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
nil
"y"
2
ref
var
1635
def
1071
remove
cons
242
ref
249
remove
cons
nil
cons
cons
nil
cons
cons
nil
83
ref
56
ref
1635
ref
varTerm
1636
def
appTerm
1637
def
213
ref
appTerm
1638
def
nil
cons
1639
def
cons
85
ref
15
ref
1073
ref
1636
ref
appTerm
242
ref
varTerm
1640
def
appTerm
appTerm
15
ref
17
ref
1640
ref
appTerm
1641
def
appTerm
1642
def
1636
ref
appTerm
appTerm
1643
def
nil
cons
1644
def
cons
nil
cons
1645
def
cons
nil
cons
cons
1646
def
102
ref
subst
1646
remove
126
ref
subst
56
ref
"_44277"
2
ref
var
1647
def
15
ref
1073
ref
1647
remove
varTerm
1648
def
appTerm
1640
ref
appTerm
appTerm
1642
ref
1648
remove
appTerm
appTerm
absTerm
1649
def
1636
ref
appTerm
appTerm
refl
1650
def
1649
remove
213
ref
appTerm
betaConv
appThm
103
remove
1635
remove
1643
remove
absTerm
1651
def
1636
ref
appTerm
betaConv
appThm
1652
def
15
ref
1073
ref
213
ref
appTerm
1653
def
1640
ref
appTerm
appTerm
1642
ref
213
ref
appTerm
appTerm
refl
appThm
trans
1651
remove
refl
1654
def
1638
remove
assume
appThm
eqMp
sym
221
ref
nil
77
ref
1640
ref
nil
cons
cons
nil
cons
nil
cons
cons
1655
def
77
ref
56
ref
1653
remove
78
ref
appTerm
appTerm
78
ref
appTerm
absTerm
1656
def
78
ref
appTerm
1657
def
betaConv
nil
238
ref
1656
ref
appTerm
1658
def
axiom
nil
83
ref
1658
remove
nil
cons
cons
85
ref
1657
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
240
ref
241
ref
1656
remove
nil
cons
cons
268
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
appThm
nil
77
ref
1641
remove
nil
cons
cons
nil
cons
nil
cons
cons
1659
def
607
remove
subst
1655
ref
1384
remove
subst
trans
appThm
1655
ref
nil
77
ref
602
remove
78
ref
appTerm
1660
def
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
77
ref
1660
remove
absTerm
1661
def
78
ref
appTerm
1662
def
betaConv
nil
238
ref
1661
ref
appTerm
1663
def
axiom
nil
83
ref
1663
remove
nil
cons
cons
85
ref
1662
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
240
ref
241
ref
1661
remove
nil
cons
cons
268
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
eqMp
subst
trans
sym
81
ref
eqMp
eqMp
eqMp
nil
127
ref
1639
ref
cons
130
ref
1644
ref
cons
nil
cons
1664
def
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
nil
83
ref
1637
remove
67
ref
appTerm
1665
def
nil
cons
1666
def
cons
1645
remove
cons
nil
cons
cons
1667
def
102
ref
subst
1667
remove
126
ref
subst
1650
remove
"_44275"
2
ref
var
1668
def
15
ref
1073
ref
1668
remove
varTerm
1669
def
appTerm
1640
ref
appTerm
appTerm
1642
ref
1669
remove
appTerm
appTerm
absTerm
67
ref
appTerm
betaConv
appThm
1652
remove
15
ref
1073
ref
67
ref
appTerm
1670
def
1640
remove
appTerm
appTerm
1642
remove
67
ref
appTerm
appTerm
refl
appThm
trans
1654
remove
1665
remove
assume
appThm
eqMp
sym
221
remove
1655
remove
77
ref
56
remove
1670
remove
78
ref
appTerm
appTerm
67
remove
appTerm
absTerm
1671
def
78
remove
appTerm
1672
def
betaConv
nil
238
ref
1671
ref
appTerm
1673
def
axiom
nil
83
ref
1673
remove
nil
cons
cons
85
ref
1672
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
240
ref
241
ref
1671
remove
nil
cons
cons
268
remove
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
appThm
1659
remove
1559
remove
subst
appThm
264
remove
677
remove
subst
trans
sym
81
remove
eqMp
eqMp
eqMp
nil
127
ref
1666
remove
cons
1674
def
1664
remove
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
77
ref
1073
remove
80
remove
appTerm
79
remove
213
remove
appTerm
appTerm
absTerm
1675
def
1636
ref
appTerm
1676
def
betaConv
nil
238
ref
1675
ref
appTerm
1677
def
axiom
nil
83
ref
1677
remove
nil
cons
cons
85
ref
1676
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
240
ref
241
ref
1675
remove
nil
cons
cons
242
ref
1636
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
1674
remove
130
ref
1639
remove
cons
1561
remove
1644
remove
cons
nil
cons
cons
cons
nil
cons
cons
1575
remove
subst
proveHyp
proveHyp
proveHyp
subst
eqMp
eqMp
proveHyp
eqMp
eqMp
nil
1109
ref
130
ref
1067
remove
cons
nil
cons
1678
def
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
1679
def
nil
9
ref
1056
ref
appTerm
1680
def
thm
nil
5
ref
6
ref
9
ref
10
ref
9
ref
567
ref
9
ref
11
ref
9
ref
12
ref
15
ref
20
ref
258
ref
"Number.Natural.^"
const
39
ref
constTerm
543
remove
appTerm
1681
def
27
ref
appTerm
1682
def
appTerm
568
ref
appTerm
appTerm
571
remove
appTerm
1683
def
appTerm
20
ref
41
remove
1682
ref
appTerm
42
ref
appTerm
32
ref
appTerm
appTerm
1684
def
186
ref
"Number.Natural.Bits.shiftRight"
const
39
ref
constTerm
1685
def
32
ref
appTerm
27
ref
appTerm
appTerm
186
ref
1685
ref
258
ref
"Number.Natural.Bits.bound"
const
39
remove
constTerm
1686
def
289
remove
appTerm
27
ref
appTerm
appTerm
21
ref
appTerm
1687
def
appTerm
27
ref
appTerm
appTerm
"Number.Natural.fromBool"
const
0
remove
2
ref
37
remove
cons
opType
constTerm
1688
def
17
remove
20
ref
1686
ref
1039
remove
appTerm
27
ref
appTerm
appTerm
23
ref
appTerm
1689
def
appTerm
1690
def
appTerm
appTerm
appTerm
appTerm
1691
def
appTerm
1692
def
absTerm
1693
def
appTerm
1694
def
absTerm
1695
def
appTerm
1696
def
absTerm
1697
def
appTerm
1698
def
absTerm
1699
def
appTerm
1700
def
absTerm
1701
def
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
6
ref
nil
77
ref
1700
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
1699
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
10
ref
nil
77
ref
1698
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
1697
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
567
ref
nil
77
ref
1696
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
1695
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
11
ref
nil
77
ref
1694
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
1693
remove
nil
cons
cons
nil
cons
nil
cons
cons
76
ref
subst
12
ref
nil
77
ref
1692
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
83
ref
1683
ref
nil
cons
1702
def
cons
85
ref
1691
remove
nil
cons
1703
def
cons
nil
cons
cons
nil
cons
cons
1704
def
102
ref
subst
1704
remove
126
ref
subst
1684
ref
refl
927
ref
nil
11
ref
255
remove
cons
1705
def
380
remove
cons
nil
cons
cons
11
ref
20
ref
1685
remove
21
ref
appTerm
42
ref
appTerm
appTerm
285
ref
21
ref
appTerm
1681
remove
42
ref
appTerm
1706
def
appTerm
appTerm
absTerm
1707
def
42
ref
appTerm
1708
def
betaConv
6
ref
9
ref
1707
ref
appTerm
1709
def
absTerm
1710
def
21
ref
appTerm
1711
def
betaConv
nil
9
ref
1710
ref
appTerm
1712
def
axiom
nil
83
ref
1712
remove
nil
cons
cons
85
ref
1711
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1710
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1709
remove
nil
cons
cons
85
ref
1708
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1707
remove
nil
cons
cons
311
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
1713
def
subst
appThm
927
remove
nil
1705
ref
6
ref
1687
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
1713
remove
subst
285
ref
refl
791
remove
nil
1705
ref
6
ref
393
remove
cons
nil
cons
cons
nil
cons
cons
11
ref
20
ref
1686
remove
21
ref
appTerm
42
ref
appTerm
appTerm
912
remove
1706
remove
appTerm
appTerm
absTerm
1714
def
42
ref
appTerm
1715
def
betaConv
6
ref
9
ref
1714
ref
appTerm
1716
def
absTerm
1717
def
21
ref
appTerm
1718
def
betaConv
nil
9
ref
1717
ref
appTerm
1719
def
axiom
nil
83
ref
1719
remove
nil
cons
cons
85
ref
1718
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1717
remove
nil
cons
cons
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1716
remove
nil
cons
cons
85
ref
1715
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
ref
1714
remove
nil
cons
cons
311
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
1720
def
subst
appThm
648
remove
appThm
appThm
1682
ref
refl
appThm
trans
appThm
nil
"b"
2
remove
var
1721
def
1690
remove
nil
cons
cons
nil
cons
nil
cons
cons
1721
ref
20
ref
1688
remove
1721
remove
varTerm
1722
def
appTerm
appTerm
1038
ref
1722
ref
appTerm
188
ref
appTerm
23
ref
appTerm
appTerm
absTerm
1723
def
1722
ref
appTerm
1724
def
betaConv
nil
238
ref
1723
ref
appTerm
1725
def
axiom
nil
83
ref
1725
remove
nil
cons
cons
85
ref
1724
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
240
ref
241
ref
1723
remove
nil
cons
cons
242
remove
1722
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
nil
631
remove
705
remove
cons
1555
remove
1512
ref
1689
remove
nil
cons
cons
nil
cons
cons
cons
nil
cons
cons
55
remove
765
remove
763
remove
1513
remove
1516
remove
appTerm
172
ref
appTerm
766
ref
appTerm
appTerm
1515
remove
766
ref
appTerm
172
ref
appTerm
appTerm
absTerm
1726
def
766
remove
appTerm
1727
def
betaConv
66
remove
60
ref
1726
ref
appTerm
1728
def
absTerm
1729
def
172
remove
appTerm
1730
def
betaConv
1512
remove
60
remove
1729
ref
appTerm
1731
def
absTerm
1732
def
1514
remove
appTerm
1733
def
betaConv
nil
238
remove
1732
ref
appTerm
1734
def
axiom
nil
83
ref
1734
remove
nil
cons
cons
85
ref
1733
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
240
remove
241
remove
1732
remove
nil
cons
cons
1529
remove
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1731
remove
nil
cons
cons
85
ref
1730
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
423
ref
61
ref
1729
remove
nil
cons
cons
424
remove
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1728
remove
nil
cons
cons
85
ref
1727
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
423
remove
61
remove
1726
remove
nil
cons
cons
788
remove
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
subst
subst
trans
1592
remove
608
remove
nil
1705
remove
6
ref
1408
remove
cons
nil
cons
cons
nil
cons
cons
1720
remove
subst
appThm
707
ref
appThm
appThm
707
remove
appThm
1593
remove
appThm
trans
appThm
appThm
appThm
sym
567
ref
1683
ref
absTerm
1735
def
568
ref
appTerm
betaConv
sym
1683
remove
assume
eqMp
53
ref
5
ref
1735
ref
nil
cons
cons
168
ref
609
remove
cons
nil
cons
1736
def
cons
nil
cons
cons
427
remove
subst
proveHyp
nil
83
ref
428
ref
1735
remove
appTerm
nil
cons
cons
85
ref
1684
remove
186
ref
1033
remove
1682
ref
appTerm
appTerm
186
remove
285
remove
258
remove
290
remove
1682
ref
appTerm
appTerm
21
ref
appTerm
appTerm
1682
ref
appTerm
appTerm
1038
remove
20
remove
1040
remove
1682
ref
appTerm
appTerm
23
ref
appTerm
appTerm
23
remove
appTerm
188
remove
appTerm
appTerm
appTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
nil
10
ref
1682
remove
nil
cons
cons
nil
cons
nil
cons
cons
10
ref
15
ref
428
remove
567
ref
572
remove
absTerm
1737
def
appTerm
1738
def
appTerm
1739
def
1046
ref
appTerm
1740
def
absTerm
1741
def
27
ref
appTerm
1742
def
betaConv
6
ref
9
ref
1741
ref
appTerm
1743
def
absTerm
1744
def
21
ref
appTerm
1745
def
betaConv
11
ref
9
ref
1744
ref
appTerm
1746
def
absTerm
1747
def
42
ref
appTerm
1748
def
betaConv
12
ref
9
ref
1747
ref
appTerm
1749
def
absTerm
1750
def
32
ref
appTerm
1751
def
betaConv
1679
remove
nil
83
ref
1680
ref
nil
cons
1752
def
cons
1753
def
85
ref
9
ref
1750
ref
appTerm
nil
cons
1754
def
cons
nil
cons
cons
nil
cons
cons
1755
def
167
ref
subst
proveHyp
1755
ref
102
ref
subst
1755
remove
126
ref
subst
nil
5
ref
1750
remove
nil
cons
cons
1756
def
nil
cons
nil
cons
cons
76
ref
subst
12
remove
nil
77
ref
1749
remove
nil
cons
1757
def
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
1747
remove
nil
cons
cons
1758
def
nil
cons
nil
cons
cons
76
ref
subst
11
remove
nil
77
ref
1746
remove
nil
cons
1759
def
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
1744
remove
nil
cons
cons
1760
def
nil
cons
nil
cons
cons
76
ref
subst
6
remove
nil
77
ref
1743
remove
nil
cons
1761
def
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
5
ref
1741
remove
nil
cons
cons
1762
def
nil
cons
nil
cons
cons
76
ref
subst
10
remove
nil
77
ref
1740
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
nil
83
ref
1738
remove
nil
cons
1763
def
cons
1764
def
1068
ref
cons
nil
cons
cons
1765
def
102
ref
subst
1765
remove
126
ref
subst
nil
1753
ref
1068
remove
cons
nil
cons
cons
1766
def
167
ref
subst
nil
1764
remove
85
ref
15
ref
1680
remove
appTerm
1046
remove
appTerm
1767
def
nil
cons
1768
def
cons
nil
cons
1769
def
cons
nil
cons
cons
167
ref
subst
nil
5
ref
567
ref
15
ref
1737
ref
568
ref
appTerm
1770
def
appTerm
1767
ref
appTerm
1771
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
76
remove
subst
567
remove
nil
77
remove
1771
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
remove
subst
nil
83
ref
1770
ref
nil
cons
1772
def
cons
1769
ref
cons
nil
cons
cons
1773
def
102
ref
subst
1773
remove
126
ref
subst
1770
ref
betaConv
1770
remove
assume
eqMp
nil
1066
remove
1769
remove
cons
nil
cons
cons
1774
def
167
ref
subst
proveHyp
1774
ref
102
ref
subst
1774
remove
126
ref
subst
1766
ref
102
remove
subst
1766
remove
126
remove
subst
1069
remove
167
ref
subst
1048
remove
32
remove
appTerm
1775
def
betaConv
1050
remove
42
remove
appTerm
1776
def
betaConv
1052
remove
568
remove
appTerm
1777
def
betaConv
1054
remove
27
remove
appTerm
1778
def
betaConv
1056
remove
21
remove
appTerm
1779
def
betaConv
nil
1753
remove
85
ref
1779
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
53
ref
1057
remove
179
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1058
remove
cons
85
ref
1778
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
1059
remove
309
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1060
remove
cons
85
ref
1777
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
1061
remove
1736
remove
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1062
remove
cons
85
ref
1776
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
1063
remove
311
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1064
remove
cons
85
ref
1775
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
1065
remove
313
ref
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
127
ref
1752
remove
cons
1780
def
1678
ref
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
nil
1109
remove
130
ref
1768
remove
cons
nil
cons
1781
def
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
127
ref
1772
remove
cons
1781
ref
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
83
ref
9
ref
168
remove
15
remove
1737
ref
477
remove
appTerm
appTerm
1767
ref
appTerm
absTerm
appTerm
nil
cons
cons
85
ref
1739
remove
1767
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
5
remove
1737
remove
nil
cons
cons
1781
remove
cons
nil
cons
cons
491
remove
subst
eqMp
eqMp
eqMp
eqMp
nil
127
ref
1763
remove
cons
1678
remove
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
1780
remove
130
ref
1754
ref
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
nil
83
ref
1754
remove
cons
85
ref
1751
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
1756
remove
313
remove
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1757
remove
cons
85
ref
1748
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
1758
remove
311
remove
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
ref
1759
remove
cons
85
ref
1745
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
ref
subst
proveHyp
53
ref
1760
remove
179
remove
cons
nil
cons
cons
177
ref
subst
eqMp
eqMp
nil
83
remove
1761
remove
cons
85
remove
1742
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
167
remove
subst
proveHyp
53
remove
1762
remove
309
remove
cons
nil
cons
cons
177
remove
subst
eqMp
eqMp
subst
eqMp
eqMp
eqMp
nil
127
remove
1702
remove
cons
130
remove
1703
remove
cons
nil
cons
cons
nil
cons
cons
142
remove
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
remove
1701
remove
appTerm
thm