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