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