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