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