6
version
"Set.finite"
const
"->"
typeOp
0
def
"Set.set"
typeOp
1
def
"A"
varType
2
def
nil
cons
3
def
opType
4
def
"bool"
typeOp
nil
opType
5
def
nil
cons
6
def
cons
opType
7
def
constTerm
8
def
refl
9
def
nil
"="
const
10
def
0
ref
4
ref
7
ref
nil
cons
11
def
cons
opType
constTerm
12
def
"Data.List.toSet"
const
13
def
0
ref
"Data.List.list"
typeOp
14
def
3
ref
opType
15
def
4
ref
nil
cons
16
def
cons
opType
constTerm
17
def
"Data.List.[]"
const
15
ref
constTerm
18
def
appTerm
19
def
appTerm
"Set.{}"
const
4
ref
constTerm
20
def
appTerm
21
def
axiom
22
def
appThm
nil
"t"
5
ref
var
23
def
8
ref
20
ref
appTerm
24
def
nil
cons
cons
nil
cons
nil
cons
cons
10
ref
0
ref
5
ref
0
ref
5
ref
6
ref
cons
opType
25
def
nil
cons
cons
opType
26
def
constTerm
27
def
23
ref
varTerm
28
def
appTerm
29
def
"Data.Bool.T"
const
5
ref
constTerm
30
def
appTerm
assume
sym
nil
30
ref
axiom
31
def
eqMp
28
ref
assume
31
ref
deductAntisym
deductAntisym
32
def
subst
nil
24
remove
axiom
eqMp
trans
sym
31
ref
eqMp
nil
"p"
5
ref
var
33
def
8
ref
19
ref
appTerm
34
def
nil
cons
cons
"q"
5
ref
var
35
def
"Data.Bool.!"
const
36
def
0
ref
0
ref
2
ref
6
ref
cons
opType
37
def
6
ref
cons
opType
38
def
constTerm
39
def
"h"
2
ref
var
40
def
36
ref
0
ref
0
ref
15
ref
6
ref
cons
opType
41
def
6
ref
cons
opType
42
def
constTerm
43
def
"t"
15
ref
var
44
def
"Data.Bool.==>"
const
26
ref
constTerm
45
def
8
ref
17
ref
44
ref
varTerm
46
def
appTerm
47
def
appTerm
48
def
appTerm
49
def
8
ref
17
ref
"Data.List.::"
const
0
ref
2
ref
0
ref
15
ref
15
ref
nil
cons
50
def
cons
opType
nil
cons
cons
opType
constTerm
40
ref
varTerm
51
def
appTerm
46
ref
appTerm
52
def
appTerm
53
def
appTerm
54
def
appTerm
55
def
absTerm
56
def
appTerm
57
def
absTerm
58
def
appTerm
59
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
27
ref
refl
60
def
"f"
26
ref
var
61
def
61
ref
varTerm
62
def
33
ref
varTerm
63
def
appTerm
35
ref
varTerm
64
def
appTerm
absTerm
65
def
33
ref
35
ref
64
ref
absTerm
66
def
absTerm
67
def
appTerm
betaConv
67
ref
63
ref
appTerm
betaConv
64
ref
refl
68
def
appThm
66
ref
64
ref
appTerm
betaConv
trans
trans
appThm
61
ref
62
ref
30
ref
appTerm
30
ref
appTerm
absTerm
69
def
67
ref
appTerm
betaConv
67
ref
30
ref
appTerm
betaConv
30
ref
refl
70
def
appThm
66
ref
30
ref
appTerm
betaConv
trans
trans
71
def
appThm
27
ref
"Data.Bool./\\"
const
26
ref
constTerm
72
def
63
ref
appTerm
73
def
64
ref
appTerm
74
def
appTerm
75
def
refl
35
ref
10
ref
0
ref
0
ref
26
ref
6
ref
cons
opType
76
def
0
ref
76
ref
6
ref
cons
opType
nil
cons
cons
opType
constTerm
77
def
65
remove
appTerm
69
ref
appTerm
absTerm
78
def
64
ref
appTerm
betaConv
appThm
10
ref
0
ref
25
ref
0
ref
25
ref
6
ref
cons
opType
79
def
nil
cons
cons
opType
constTerm
80
def
73
ref
appTerm
refl
33
ref
78
remove
absTerm
81
def
63
ref
appTerm
betaConv
appThm
nil
10
ref
0
ref
26
ref
76
remove
nil
cons
cons
opType
constTerm
82
def
72
ref
appTerm
81
ref
appTerm
axiom
83
def
63
ref
refl
84
def
appThm
eqMp
68
ref
appThm
eqMp
85
def
74
ref
assume
eqMp
67
ref
refl
86
def
appThm
eqMp
sym
31
ref
eqMp
87
def
85
remove
sym
61
ref
62
ref
refl
nil
23
ref
63
ref
nil
cons
88
def
cons
nil
cons
nil
cons
cons
32
ref
subst
63
ref
assume
89
def
eqMp
appThm
nil
23
ref
64
ref
nil
cons
90
def
cons
nil
cons
nil
cons
cons
32
ref
subst
64
ref
assume
91
def
eqMp
appThm
absThm
eqMp
92
def
deductAntisym
93
def
subst
proveHyp
nil
"P"
37
ref
var
94
def
58
remove
nil
cons
cons
nil
cons
nil
cons
cons
27
ref
39
ref
94
ref
varTerm
95
def
appTerm
96
def
appTerm
refl
"p"
37
ref
var
97
def
10
ref
0
ref
37
ref
38
ref
nil
cons
cons
opType
constTerm
97
ref
varTerm
98
def
appTerm
"x"
2
ref
var
99
def
30
ref
absTerm
100
def
appTerm
absTerm
101
def
95
ref
appTerm
betaConv
102
def
appThm
nil
10
ref
0
ref
38
ref
0
ref
38
ref
6
ref
cons
opType
103
def
nil
cons
cons
opType
constTerm
104
def
39
ref
appTerm
101
remove
appTerm
axiom
95
ref
refl
105
def
appThm
106
def
eqMp
sym
107
def
subst
40
ref
nil
23
ref
57
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
"P"
41
ref
var
108
def
56
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
50
ref
cons
nil
cons
109
def
nil
nil
cons
110
def
cons
111
def
107
ref
subst
112
def
subst
44
ref
nil
23
ref
55
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
33
ref
48
ref
nil
cons
113
def
cons
35
ref
54
remove
nil
cons
114
def
cons
nil
cons
cons
nil
cons
cons
115
def
27
ref
45
ref
63
ref
appTerm
116
def
64
ref
appTerm
117
def
appTerm
refl
33
ref
35
ref
75
remove
63
ref
appTerm
absTerm
118
def
absTerm
119
def
63
ref
appTerm
betaConv
68
ref
appThm
118
remove
64
ref
appTerm
betaConv
trans
appThm
nil
82
ref
45
ref
appTerm
119
remove
appTerm
axiom
84
remove
appThm
68
ref
appThm
eqMp
120
def
sym
121
def
subst
115
remove
93
ref
subst
9
remove
44
ref
12
ref
53
ref
appTerm
122
def
"Set.insert"
const
0
ref
2
ref
0
ref
4
ref
16
ref
cons
opType
nil
cons
cons
opType
constTerm
123
def
51
ref
appTerm
124
def
47
ref
appTerm
125
def
appTerm
absTerm
126
def
46
ref
appTerm
127
def
betaConv
40
ref
43
ref
126
ref
appTerm
128
def
absTerm
129
def
51
ref
appTerm
130
def
betaConv
nil
39
ref
129
ref
appTerm
131
def
axiom
nil
33
ref
131
remove
nil
cons
cons
35
ref
130
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
121
ref
92
remove
nil
"P"
5
ref
var
132
def
88
ref
cons
"Q"
5
ref
var
133
def
90
ref
cons
nil
cons
134
def
cons
nil
cons
cons
60
ref
61
ref
62
remove
132
ref
varTerm
135
def
appTerm
136
def
133
ref
varTerm
137
def
appTerm
absTerm
138
def
33
ref
35
ref
63
ref
absTerm
absTerm
139
def
appTerm
betaConv
139
ref
135
ref
appTerm
betaConv
137
ref
refl
140
def
appThm
35
ref
135
ref
absTerm
137
ref
appTerm
betaConv
trans
trans
appThm
69
ref
139
ref
appTerm
betaConv
139
ref
30
ref
appTerm
betaConv
70
remove
appThm
35
ref
30
ref
absTerm
30
ref
appTerm
betaConv
trans
trans
appThm
27
ref
72
ref
135
ref
appTerm
141
def
137
ref
appTerm
142
def
appTerm
refl
35
ref
77
remove
61
remove
136
remove
64
ref
appTerm
absTerm
appTerm
69
remove
appTerm
absTerm
137
ref
appTerm
betaConv
appThm
80
ref
141
remove
appTerm
refl
81
remove
135
ref
appTerm
betaConv
appThm
83
remove
135
ref
refl
143
def
appThm
eqMp
140
ref
appThm
eqMp
142
remove
assume
eqMp
144
def
139
remove
refl
appThm
eqMp
sym
31
ref
eqMp
145
def
subst
deductAntisym
eqMp
120
remove
117
ref
assume
eqMp
sym
89
remove
eqMp
87
remove
proveHyp
deductAntisym
146
def
subst
proveHyp
"A"
3
ref
cons
147
def
nil
cons
148
def
94
ref
129
remove
nil
cons
cons
99
ref
51
ref
nil
cons
149
def
cons
nil
cons
150
def
cons
nil
cons
cons
nil
33
ref
96
ref
nil
cons
151
def
cons
35
ref
95
ref
99
ref
varTerm
152
def
appTerm
153
def
nil
cons
154
def
cons
nil
cons
cons
nil
cons
cons
155
def
121
ref
subst
155
remove
93
ref
subst
27
ref
153
ref
appTerm
refl
100
ref
152
ref
appTerm
betaConv
156
def
appThm
102
remove
106
remove
96
remove
assume
eqMp
eqMp
152
ref
refl
157
def
appThm
eqMp
sym
31
ref
eqMp
eqMp
nil
132
ref
151
remove
cons
133
ref
154
ref
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
158
def
subst
eqMp
eqMp
nil
33
ref
128
remove
nil
cons
cons
35
ref
127
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
109
ref
108
ref
126
remove
nil
cons
cons
"x"
15
ref
var
159
def
46
ref
nil
cons
160
def
cons
nil
cons
161
def
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
162
def
appThm
nil
"s"
4
ref
var
163
def
47
ref
nil
cons
164
def
cons
165
def
150
ref
cons
nil
cons
cons
166
def
99
ref
27
ref
8
ref
123
ref
152
ref
appTerm
163
ref
varTerm
167
def
appTerm
168
def
appTerm
appTerm
8
ref
167
ref
appTerm
169
def
appTerm
absTerm
170
def
152
ref
appTerm
171
def
betaConv
163
ref
39
ref
170
ref
appTerm
172
def
absTerm
173
def
167
ref
appTerm
174
def
betaConv
nil
36
ref
0
ref
7
ref
6
ref
cons
opType
constTerm
175
def
173
ref
appTerm
176
def
axiom
nil
33
ref
176
remove
nil
cons
cons
35
ref
174
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
"A"
16
remove
cons
nil
cons
177
def
"P"
7
remove
var
178
def
173
remove
nil
cons
cons
"x"
4
ref
var
179
def
167
ref
nil
cons
cons
nil
cons
180
def
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
172
remove
nil
cons
cons
35
ref
171
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
148
ref
94
ref
170
remove
nil
cons
cons
99
ref
152
ref
nil
cons
cons
nil
cons
181
def
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
nil
23
ref
113
ref
cons
nil
cons
nil
cons
cons
32
ref
subst
48
remove
assume
eqMp
trans
trans
sym
31
ref
eqMp
eqMp
nil
132
ref
113
remove
cons
133
ref
114
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
33
ref
72
ref
34
remove
appTerm
59
remove
appTerm
nil
cons
cons
35
ref
43
ref
"l"
15
ref
var
182
def
8
remove
17
ref
182
ref
varTerm
183
def
appTerm
184
def
appTerm
185
def
absTerm
186
def
appTerm
187
def
nil
cons
188
def
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
45
ref
refl
189
def
72
ref
refl
190
def
186
ref
18
ref
appTerm
betaConv
appThm
39
ref
refl
191
def
40
ref
43
ref
refl
192
def
44
ref
189
ref
186
ref
46
ref
appTerm
betaConv
appThm
186
ref
52
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
192
ref
182
ref
186
ref
183
ref
appTerm
193
def
betaConv
194
def
absThm
appThm
appThm
nil
"p"
41
ref
var
195
def
186
remove
nil
cons
196
def
cons
nil
cons
nil
cons
cons
195
ref
45
ref
72
ref
195
ref
varTerm
197
def
18
ref
appTerm
appTerm
39
ref
40
ref
43
ref
44
ref
45
ref
197
ref
46
ref
appTerm
appTerm
197
ref
52
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
43
ref
182
ref
197
ref
183
ref
appTerm
absTerm
appTerm
appTerm
absTerm
198
def
197
ref
appTerm
199
def
betaConv
nil
36
ref
0
ref
42
ref
6
ref
cons
opType
constTerm
198
ref
appTerm
200
def
axiom
nil
33
ref
200
remove
nil
cons
cons
35
ref
199
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
"A"
41
ref
nil
cons
201
def
cons
nil
cons
"P"
42
remove
var
198
remove
nil
cons
cons
"x"
41
ref
var
197
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
202
def
subst
eqMp
eqMp
203
def
nil
187
remove
thm
192
ref
182
ref
nil
97
ref
100
ref
nil
cons
cons
nil
cons
nil
cons
cons
182
ref
27
ref
"Data.List.all"
const
204
def
0
ref
37
ref
201
ref
cons
opType
205
def
constTerm
206
def
98
ref
appTerm
207
def
183
ref
appTerm
208
def
appTerm
39
ref
99
ref
45
ref
"Set.member"
const
209
def
0
ref
2
ref
11
remove
cons
opType
constTerm
210
def
152
ref
appTerm
211
def
184
ref
appTerm
212
def
appTerm
213
def
98
ref
152
ref
appTerm
214
def
appTerm
215
def
absTerm
216
def
appTerm
217
def
appTerm
absTerm
218
def
183
ref
appTerm
219
def
betaConv
220
def
60
ref
nil
23
ref
207
ref
18
ref
appTerm
221
def
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
97
ref
221
ref
absTerm
222
def
98
ref
appTerm
223
def
betaConv
nil
36
ref
103
remove
constTerm
224
def
222
ref
appTerm
225
def
axiom
nil
33
ref
225
remove
nil
cons
cons
35
ref
223
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
"A"
37
ref
nil
cons
226
def
cons
nil
cons
227
def
"P"
38
ref
var
228
def
222
remove
nil
cons
cons
"x"
37
ref
var
229
def
98
ref
nil
cons
230
def
cons
nil
cons
231
def
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
eqMp
232
def
appThm
191
ref
99
ref
189
ref
211
ref
refl
233
def
22
ref
appThm
99
ref
"Data.Bool.~"
const
25
ref
constTerm
234
def
211
ref
20
ref
appTerm
235
def
appTerm
236
def
absTerm
237
def
152
ref
appTerm
238
def
betaConv
nil
39
ref
237
ref
appTerm
239
def
axiom
nil
33
ref
239
remove
nil
cons
cons
35
ref
238
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
148
ref
94
ref
237
remove
nil
cons
cons
181
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
236
remove
nil
cons
cons
35
ref
27
ref
235
ref
appTerm
"Data.Bool.F"
const
5
ref
constTerm
240
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
132
ref
235
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
33
ref
234
ref
135
ref
appTerm
241
def
nil
cons
242
def
cons
35
ref
27
ref
135
ref
appTerm
240
ref
appTerm
nil
cons
243
def
cons
nil
cons
cons
nil
cons
cons
244
def
121
ref
subst
244
remove
93
ref
subst
nil
33
ref
135
ref
nil
cons
245
def
cons
246
def
35
ref
240
ref
nil
cons
247
def
cons
nil
cons
cons
nil
cons
cons
189
ref
27
ref
63
ref
appTerm
64
ref
appTerm
248
def
assume
249
def
appThm
68
remove
appThm
sym
nil
33
ref
90
ref
cons
250
def
35
ref
90
ref
cons
nil
cons
cons
nil
cons
cons
251
def
121
ref
subst
251
remove
93
ref
subst
91
remove
eqMp
nil
132
ref
90
ref
cons
134
remove
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
252
def
eqMp
253
def
nil
33
ref
117
remove
nil
cons
254
def
cons
35
ref
45
ref
64
ref
appTerm
255
def
63
ref
appTerm
nil
cons
256
def
cons
nil
cons
cons
nil
cons
cons
93
ref
subst
proveHyp
255
ref
refl
249
remove
appThm
sym
252
remove
eqMp
eqMp
nil
250
remove
35
ref
88
ref
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
nil
132
ref
254
ref
cons
133
ref
256
remove
cons
nil
cons
cons
nil
cons
cons
257
def
60
ref
138
remove
67
ref
appTerm
betaConv
67
remove
135
ref
appTerm
betaConv
140
ref
appThm
66
remove
137
ref
appTerm
betaConv
trans
trans
appThm
71
remove
appThm
144
remove
86
remove
appThm
eqMp
sym
31
ref
eqMp
258
def
subst
eqMp
146
ref
257
remove
145
ref
subst
eqMp
deductAntisym
deductAntisym
259
def
subst
27
ref
241
ref
appTerm
refl
33
ref
116
ref
240
ref
appTerm
absTerm
260
def
135
ref
appTerm
betaConv
appThm
nil
80
ref
234
ref
appTerm
260
remove
appTerm
axiom
143
ref
appThm
eqMp
241
remove
assume
eqMp
nil
33
ref
45
ref
135
ref
appTerm
261
def
240
ref
appTerm
nil
cons
cons
35
ref
45
ref
240
ref
appTerm
262
def
135
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
93
ref
subst
proveHyp
nil
33
ref
247
ref
cons
35
ref
245
ref
cons
nil
cons
cons
nil
cons
cons
263
def
121
ref
subst
263
remove
93
ref
subst
33
ref
63
ref
absTerm
264
def
135
ref
appTerm
265
def
betaConv
nil
27
ref
240
ref
appTerm
266
def
36
ref
79
remove
constTerm
267
def
264
ref
appTerm
268
def
appTerm
axiom
240
ref
assume
eqMp
nil
33
ref
268
remove
nil
cons
cons
35
ref
265
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
"A"
6
ref
cons
nil
cons
269
def
"P"
25
remove
var
270
def
264
remove
nil
cons
cons
"x"
5
ref
var
271
def
245
ref
cons
nil
cons
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
eqMp
nil
132
ref
247
ref
cons
133
ref
245
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
132
ref
242
remove
cons
133
ref
243
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
272
def
subst
eqMp
trans
273
def
appThm
214
ref
refl
274
def
appThm
nil
23
ref
214
ref
nil
cons
275
def
cons
nil
cons
nil
cons
cons
276
def
23
ref
27
ref
262
remove
28
ref
appTerm
appTerm
30
ref
appTerm
absTerm
277
def
28
ref
appTerm
278
def
betaConv
nil
267
ref
277
ref
appTerm
279
def
axiom
nil
33
ref
279
remove
nil
cons
cons
35
ref
278
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
277
remove
nil
cons
cons
271
ref
28
ref
nil
cons
280
def
cons
nil
cons
281
def
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
trans
absThm
appThm
nil
23
ref
30
ref
nil
cons
cons
nil
cons
nil
cons
cons
282
def
23
ref
27
ref
39
ref
99
ref
28
ref
absTerm
appTerm
appTerm
28
ref
appTerm
absTerm
283
def
28
ref
appTerm
284
def
betaConv
nil
267
ref
283
ref
appTerm
285
def
axiom
nil
33
ref
285
remove
nil
cons
cons
35
ref
284
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
283
remove
nil
cons
cons
281
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
286
def
subst
287
def
trans
appThm
282
ref
23
ref
27
ref
27
ref
30
ref
appTerm
28
ref
appTerm
appTerm
28
ref
appTerm
absTerm
288
def
28
ref
appTerm
289
def
betaConv
nil
267
ref
288
ref
appTerm
290
def
axiom
nil
33
ref
290
remove
nil
cons
cons
35
ref
289
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
288
remove
nil
cons
cons
281
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
291
def
trans
sym
31
ref
eqMp
nil
33
ref
27
ref
221
ref
appTerm
39
ref
99
ref
45
ref
211
ref
19
ref
appTerm
292
def
appTerm
214
ref
appTerm
absTerm
appTerm
appTerm
293
def
nil
cons
cons
35
ref
39
ref
40
ref
43
ref
44
ref
45
ref
27
ref
207
ref
46
ref
appTerm
294
def
appTerm
39
ref
99
ref
45
ref
211
ref
47
ref
appTerm
295
def
appTerm
214
ref
appTerm
296
def
absTerm
297
def
appTerm
298
def
appTerm
299
def
appTerm
27
ref
207
remove
52
ref
appTerm
300
def
appTerm
301
def
39
ref
99
ref
45
ref
211
ref
53
ref
appTerm
302
def
appTerm
214
ref
appTerm
absTerm
appTerm
appTerm
303
def
appTerm
304
def
absTerm
305
def
appTerm
306
def
absTerm
307
def
appTerm
308
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
93
ref
subst
proveHyp
nil
94
ref
307
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
40
ref
nil
23
ref
306
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
108
ref
305
remove
nil
cons
cons
nil
cons
nil
cons
cons
112
ref
subst
44
ref
nil
23
ref
304
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
33
ref
299
ref
nil
cons
309
def
cons
35
ref
303
remove
nil
cons
310
def
cons
nil
cons
cons
nil
cons
cons
311
def
121
ref
subst
311
remove
93
ref
subst
60
ref
44
ref
301
remove
72
ref
98
ref
51
ref
appTerm
312
def
appTerm
313
def
294
ref
appTerm
314
def
appTerm
absTerm
315
def
46
ref
appTerm
316
def
betaConv
40
ref
43
ref
315
ref
appTerm
317
def
absTerm
318
def
51
ref
appTerm
319
def
betaConv
97
ref
39
ref
318
ref
appTerm
320
def
absTerm
321
def
98
ref
appTerm
322
def
betaConv
nil
224
ref
321
ref
appTerm
323
def
axiom
nil
33
ref
323
remove
nil
cons
cons
35
ref
322
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
227
ref
228
ref
321
remove
nil
cons
cons
231
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
320
remove
nil
cons
cons
35
ref
319
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
148
ref
94
ref
318
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
317
remove
nil
cons
cons
35
ref
316
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
109
ref
108
ref
315
remove
nil
cons
cons
161
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
324
def
appThm
191
ref
99
ref
189
ref
233
ref
162
ref
appThm
nil
165
remove
"y"
2
ref
var
325
def
149
remove
cons
nil
cons
cons
nil
cons
cons
163
ref
27
ref
211
ref
123
remove
325
ref
varTerm
326
def
appTerm
167
ref
appTerm
appTerm
appTerm
"Data.Bool.\\/"
const
26
remove
constTerm
327
def
10
ref
0
ref
2
ref
226
remove
cons
opType
constTerm
328
def
152
ref
appTerm
329
def
326
ref
appTerm
appTerm
211
remove
167
ref
appTerm
330
def
appTerm
appTerm
absTerm
331
def
167
ref
appTerm
332
def
betaConv
325
ref
175
ref
331
ref
appTerm
333
def
absTerm
334
def
326
ref
appTerm
335
def
betaConv
99
ref
39
ref
334
ref
appTerm
336
def
absTerm
337
def
152
ref
appTerm
338
def
betaConv
nil
39
ref
337
ref
appTerm
339
def
axiom
nil
33
ref
339
remove
nil
cons
cons
35
ref
338
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
148
ref
94
ref
337
remove
nil
cons
cons
181
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
336
remove
nil
cons
cons
35
ref
335
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
148
ref
94
ref
334
remove
nil
cons
cons
99
ref
326
ref
nil
cons
cons
nil
cons
340
def
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
333
remove
nil
cons
cons
35
ref
332
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
177
ref
178
ref
331
remove
nil
cons
cons
180
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
trans
341
def
appThm
274
ref
appThm
absThm
appThm
appThm
sym
27
ref
"_17659"
5
ref
var
342
def
27
ref
313
ref
342
remove
varTerm
appTerm
appTerm
39
ref
99
ref
45
ref
327
ref
329
ref
51
ref
appTerm
343
def
appTerm
344
def
295
ref
appTerm
345
def
appTerm
214
ref
appTerm
346
def
absTerm
347
def
appTerm
348
def
appTerm
absTerm
349
def
294
ref
appTerm
350
def
appTerm
refl
349
ref
298
ref
appTerm
betaConv
appThm
60
ref
350
remove
betaConv
appThm
27
ref
313
remove
298
ref
appTerm
351
def
appTerm
348
ref
appTerm
refl
appThm
trans
349
remove
refl
299
remove
assume
appThm
eqMp
sym
nil
33
ref
351
ref
nil
cons
352
def
cons
35
ref
348
ref
nil
cons
353
def
cons
nil
cons
cons
nil
cons
cons
354
def
259
ref
subst
354
ref
121
ref
subst
354
remove
93
ref
subst
nil
132
ref
312
ref
nil
cons
355
def
cons
356
def
133
ref
298
remove
nil
cons
357
def
cons
nil
cons
cons
nil
cons
cons
358
def
145
ref
subst
358
remove
258
ref
subst
nil
94
ref
347
ref
nil
cons
cons
359
def
nil
cons
nil
cons
cons
107
ref
subst
99
ref
nil
23
ref
346
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
33
ref
345
remove
nil
cons
360
def
cons
35
ref
275
ref
cons
361
def
nil
cons
362
def
cons
nil
cons
cons
363
def
121
ref
subst
363
ref
93
ref
subst
297
ref
152
ref
appTerm
364
def
betaConv
nil
33
ref
357
ref
cons
35
ref
364
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
148
ref
94
ref
297
remove
nil
cons
cons
365
def
181
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
343
ref
nil
cons
366
def
cons
362
ref
cons
nil
cons
cons
367
def
121
ref
subst
367
remove
93
ref
subst
98
ref
refl
343
remove
assume
appThm
nil
23
ref
355
ref
cons
nil
cons
nil
cons
cons
32
ref
subst
312
ref
assume
eqMp
trans
sym
31
ref
eqMp
eqMp
nil
132
ref
366
remove
cons
368
def
133
ref
275
ref
cons
nil
cons
369
def
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
nil
368
ref
133
ref
295
ref
nil
cons
370
def
cons
371
def
"R"
5
ref
var
372
def
275
ref
cons
nil
cons
cons
cons
nil
cons
cons
nil
33
ref
45
ref
137
ref
appTerm
373
def
372
remove
varTerm
374
def
appTerm
375
def
nil
cons
cons
35
ref
374
ref
nil
cons
376
def
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
nil
33
ref
261
ref
374
ref
appTerm
nil
cons
cons
35
ref
45
ref
375
remove
appTerm
374
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
"r"
5
ref
var
377
def
45
ref
261
ref
377
ref
varTerm
378
def
appTerm
appTerm
379
def
45
ref
373
ref
378
ref
appTerm
appTerm
378
ref
appTerm
appTerm
absTerm
380
def
374
remove
appTerm
381
def
betaConv
27
ref
327
ref
135
ref
appTerm
382
def
137
ref
appTerm
383
def
appTerm
refl
35
ref
267
ref
377
ref
379
remove
45
ref
255
remove
378
ref
appTerm
384
def
appTerm
378
ref
appTerm
385
def
appTerm
absTerm
appTerm
absTerm
137
ref
appTerm
betaConv
appThm
80
remove
382
remove
appTerm
refl
33
ref
35
ref
267
ref
377
ref
45
ref
116
ref
378
ref
appTerm
appTerm
385
remove
appTerm
absTerm
appTerm
absTerm
absTerm
386
def
135
remove
appTerm
betaConv
appThm
nil
82
remove
327
ref
appTerm
386
remove
appTerm
axiom
143
remove
appThm
eqMp
140
remove
appThm
eqMp
387
def
383
remove
assume
eqMp
nil
33
ref
267
ref
380
ref
appTerm
nil
cons
cons
35
ref
381
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
380
remove
nil
cons
cons
271
ref
376
remove
cons
nil
cons
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
eqMp
eqMp
subst
proveHyp
proveHyp
eqMp
nil
132
ref
360
ref
cons
369
ref
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
proveHyp
proveHyp
eqMp
nil
132
ref
352
ref
cons
133
ref
353
ref
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
nil
33
ref
45
ref
351
ref
appTerm
348
ref
appTerm
nil
cons
cons
35
ref
45
ref
348
remove
appTerm
351
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
93
ref
subst
proveHyp
nil
33
ref
353
ref
cons
388
def
35
ref
352
ref
cons
nil
cons
cons
nil
cons
cons
389
def
121
ref
subst
389
remove
93
ref
subst
51
ref
refl
nil
132
ref
328
remove
51
ref
appTerm
51
ref
appTerm
390
def
nil
cons
cons
133
ref
210
remove
51
ref
appTerm
391
def
47
ref
appTerm
392
def
nil
cons
393
def
cons
nil
cons
cons
nil
cons
cons
387
remove
sym
394
def
nil
270
ref
23
ref
45
ref
261
remove
28
ref
appTerm
395
def
appTerm
45
ref
373
remove
28
ref
appTerm
396
def
appTerm
28
ref
appTerm
397
def
appTerm
398
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
269
ref
110
ref
cons
399
def
107
ref
subst
400
def
subst
401
def
23
ref
nil
23
ref
398
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
402
def
nil
33
ref
395
ref
nil
cons
403
def
cons
35
ref
397
remove
nil
cons
404
def
cons
nil
cons
cons
nil
cons
cons
405
def
121
ref
subst
406
def
405
remove
93
ref
subst
407
def
nil
33
ref
396
ref
nil
cons
408
def
cons
35
ref
280
ref
cons
nil
cons
409
def
cons
nil
cons
cons
410
def
121
ref
subst
411
def
410
remove
93
ref
subst
412
def
nil
246
remove
409
ref
cons
nil
cons
cons
146
ref
subst
395
remove
assume
eqMp
eqMp
nil
132
ref
408
remove
cons
133
ref
280
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
413
def
deductAntisym
eqMp
eqMp
nil
132
ref
403
remove
cons
133
ref
404
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
414
def
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
subst
proveHyp
nil
33
ref
327
ref
390
remove
appTerm
392
ref
appTerm
nil
cons
cons
35
ref
355
ref
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
150
ref
nil
cons
cons
415
def
347
remove
152
ref
appTerm
416
def
betaConv
nil
388
remove
35
ref
416
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
148
ref
359
remove
181
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
417
def
subst
eqMp
nil
33
ref
355
ref
cons
418
def
35
ref
357
remove
cons
nil
cons
cons
nil
cons
cons
93
ref
subst
proveHyp
nil
365
remove
nil
cons
nil
cons
cons
107
ref
subst
99
ref
nil
23
ref
296
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
33
ref
370
ref
cons
362
ref
cons
nil
cons
cons
419
def
121
ref
subst
419
remove
93
ref
subst
nil
368
remove
371
remove
nil
cons
cons
nil
cons
cons
394
remove
401
remove
23
ref
402
remove
406
remove
407
remove
411
remove
412
remove
nil
33
ref
137
ref
nil
cons
420
def
cons
409
remove
cons
nil
cons
cons
146
ref
subst
396
remove
assume
eqMp
eqMp
413
remove
deductAntisym
eqMp
eqMp
414
remove
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
subst
363
remove
146
ref
subst
proveHyp
417
remove
eqMp
eqMp
nil
132
ref
370
remove
cons
369
ref
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
eqMp
nil
132
ref
353
remove
cons
133
ref
352
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
nil
132
ref
309
remove
cons
133
ref
310
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
33
ref
72
ref
293
remove
appTerm
308
remove
appTerm
nil
cons
cons
35
ref
43
ref
218
ref
appTerm
421
def
nil
cons
422
def
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
189
ref
190
ref
218
ref
18
ref
appTerm
betaConv
appThm
191
ref
40
ref
192
ref
44
ref
189
ref
218
ref
46
ref
appTerm
betaConv
appThm
218
ref
52
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
192
ref
182
ref
220
remove
absThm
appThm
appThm
nil
195
ref
218
remove
nil
cons
423
def
cons
nil
cons
nil
cons
cons
202
ref
subst
eqMp
eqMp
424
def
nil
33
ref
422
ref
cons
35
ref
219
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
109
ref
108
ref
423
remove
cons
159
remove
183
ref
nil
cons
cons
nil
cons
425
def
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
426
def
subst
191
ref
99
ref
213
ref
refl
427
def
156
remove
appThm
nil
23
ref
212
ref
nil
cons
428
def
cons
nil
cons
nil
cons
cons
429
def
23
ref
27
ref
45
ref
28
ref
appTerm
430
def
30
ref
appTerm
appTerm
30
ref
appTerm
absTerm
431
def
28
ref
appTerm
432
def
betaConv
nil
267
ref
431
ref
appTerm
433
def
axiom
nil
33
ref
433
remove
nil
cons
cons
35
ref
432
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
431
remove
nil
cons
cons
281
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
434
def
subst
trans
absThm
appThm
287
ref
trans
trans
absThm
appThm
282
ref
111
remove
286
ref
subst
subst
435
def
trans
sym
31
ref
eqMp
nil
43
ref
182
ref
206
ref
100
remove
appTerm
183
ref
appTerm
absTerm
appTerm
thm
"Number.Natural.<="
const
0
ref
"Number.Natural.natural"
typeOp
nil
opType
436
def
0
ref
436
ref
6
ref
cons
opType
437
def
nil
cons
cons
opType
438
def
constTerm
439
def
refl
440
def
"Set.size"
const
0
ref
4
ref
436
ref
nil
cons
441
def
cons
opType
constTerm
442
def
refl
443
def
22
ref
appThm
nil
10
ref
438
remove
constTerm
444
def
442
ref
20
ref
appTerm
appTerm
"Number.Natural.zero"
const
436
ref
constTerm
445
def
appTerm
axiom
trans
appThm
"Data.List.length"
const
0
ref
15
ref
441
ref
cons
opType
constTerm
446
def
18
ref
appTerm
447
def
refl
appThm
nil
"n"
436
ref
var
448
def
447
ref
nil
cons
cons
nil
cons
nil
cons
cons
nil
23
ref
439
ref
445
remove
appTerm
448
ref
varTerm
449
def
appTerm
450
def
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
448
ref
450
remove
absTerm
451
def
449
ref
appTerm
452
def
betaConv
nil
36
ref
0
ref
437
ref
6
ref
cons
opType
453
def
constTerm
454
def
451
ref
appTerm
455
def
axiom
nil
33
ref
455
remove
nil
cons
cons
35
ref
452
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
"A"
441
ref
cons
nil
cons
456
def
"P"
437
ref
var
457
def
451
remove
nil
cons
cons
"x"
436
ref
var
458
def
449
ref
nil
cons
cons
nil
cons
459
def
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
eqMp
subst
trans
sym
31
ref
eqMp
nil
33
ref
439
ref
442
ref
19
remove
appTerm
appTerm
447
remove
appTerm
460
def
nil
cons
cons
35
ref
39
ref
40
ref
43
ref
44
ref
45
ref
439
ref
442
ref
47
ref
appTerm
461
def
appTerm
462
def
446
ref
46
ref
appTerm
463
def
appTerm
464
def
appTerm
439
ref
442
ref
53
remove
appTerm
appTerm
446
ref
52
ref
appTerm
465
def
appTerm
466
def
appTerm
467
def
absTerm
468
def
appTerm
469
def
absTerm
470
def
appTerm
471
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
93
ref
subst
proveHyp
nil
94
ref
470
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
40
ref
nil
23
ref
469
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
108
ref
468
remove
nil
cons
cons
nil
cons
nil
cons
cons
112
ref
subst
44
ref
nil
23
ref
467
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
33
ref
464
ref
nil
cons
472
def
cons
35
ref
466
remove
nil
cons
473
def
cons
nil
cons
cons
nil
cons
cons
474
def
121
ref
subst
474
remove
93
ref
subst
440
remove
443
remove
162
ref
appThm
appThm
44
ref
444
ref
465
remove
appTerm
"Number.Natural.suc"
const
0
ref
436
ref
441
remove
cons
opType
475
def
constTerm
476
def
463
ref
appTerm
477
def
appTerm
absTerm
478
def
46
ref
appTerm
479
def
betaConv
40
ref
43
ref
478
ref
appTerm
480
def
absTerm
481
def
51
ref
appTerm
482
def
betaConv
nil
39
ref
481
ref
appTerm
483
def
axiom
nil
33
ref
483
remove
nil
cons
cons
35
ref
482
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
148
ref
94
ref
481
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
480
remove
nil
cons
cons
35
ref
479
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
109
ref
108
ref
478
remove
nil
cons
cons
161
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
appThm
sym
163
ref
45
ref
169
ref
appTerm
484
def
444
ref
442
ref
124
remove
167
ref
appTerm
appTerm
appTerm
"Data.Bool.cond"
const
485
def
0
ref
5
ref
0
ref
436
ref
475
remove
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
486
def
391
remove
167
ref
appTerm
appTerm
442
ref
167
ref
appTerm
487
def
appTerm
476
ref
487
ref
appTerm
488
def
appTerm
appTerm
appTerm
absTerm
489
def
47
ref
appTerm
490
def
betaConv
99
ref
175
ref
163
ref
484
ref
444
ref
442
ref
168
ref
appTerm
appTerm
486
ref
330
ref
appTerm
487
ref
appTerm
488
remove
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
491
def
51
ref
appTerm
492
def
betaConv
nil
39
ref
491
ref
appTerm
493
def
axiom
nil
33
ref
493
remove
nil
cons
cons
35
ref
492
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
148
ref
94
ref
491
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
175
ref
489
ref
appTerm
nil
cons
cons
35
ref
490
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
177
ref
178
ref
489
remove
nil
cons
cons
179
ref
164
remove
cons
nil
cons
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
49
remove
444
ref
442
ref
125
remove
appTerm
494
def
appTerm
486
remove
392
ref
appTerm
461
ref
appTerm
476
ref
461
ref
appTerm
495
def
appTerm
496
def
appTerm
497
def
appTerm
nil
cons
cons
35
ref
439
ref
494
ref
appTerm
477
ref
appTerm
498
def
nil
cons
499
def
cons
nil
cons
500
def
cons
nil
cons
cons
146
ref
subst
proveHyp
189
ref
189
ref
nil
182
ref
160
remove
cons
nil
cons
nil
cons
cons
nil
23
ref
185
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
194
remove
203
remove
nil
33
ref
188
remove
cons
35
ref
193
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
109
ref
108
ref
196
remove
cons
425
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
eqMp
subst
appThm
497
ref
refl
appThm
nil
23
ref
497
ref
nil
cons
501
def
cons
nil
cons
nil
cons
cons
23
ref
27
ref
45
ref
30
ref
appTerm
28
ref
appTerm
appTerm
28
ref
appTerm
absTerm
502
def
28
ref
appTerm
503
def
betaConv
nil
267
ref
502
ref
appTerm
504
def
axiom
nil
33
ref
504
remove
nil
cons
cons
35
ref
503
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
502
remove
nil
cons
cons
281
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
505
def
subst
trans
appThm
498
remove
refl
appThm
sym
nil
33
ref
501
ref
cons
500
remove
cons
nil
cons
cons
506
def
121
ref
subst
506
remove
93
ref
subst
27
ref
"_17651"
436
ref
var
507
def
439
ref
507
remove
varTerm
appTerm
477
ref
appTerm
absTerm
508
def
494
remove
appTerm
509
def
appTerm
refl
508
ref
496
ref
appTerm
betaConv
appThm
60
ref
509
remove
betaConv
appThm
439
ref
496
ref
appTerm
510
def
477
ref
appTerm
511
def
refl
appThm
trans
508
remove
refl
497
remove
assume
appThm
eqMp
sym
448
ref
72
ref
510
ref
449
ref
appTerm
appTerm
439
ref
449
ref
appTerm
512
def
477
ref
appTerm
appTerm
absTerm
513
def
495
ref
appTerm
betaConv
sym
72
ref
510
remove
495
ref
appTerm
514
def
appTerm
refl
nil
448
ref
463
remove
nil
cons
cons
"m"
436
ref
var
515
def
461
ref
nil
cons
516
def
cons
nil
cons
517
def
cons
nil
cons
cons
448
ref
27
ref
439
ref
476
ref
515
ref
varTerm
518
def
appTerm
appTerm
476
remove
449
ref
appTerm
519
def
appTerm
appTerm
439
ref
518
ref
appTerm
520
def
449
ref
appTerm
521
def
appTerm
absTerm
522
def
449
ref
appTerm
523
def
betaConv
515
ref
454
ref
522
ref
appTerm
524
def
absTerm
525
def
518
ref
appTerm
526
def
betaConv
nil
454
ref
525
ref
appTerm
527
def
axiom
nil
33
ref
527
remove
nil
cons
cons
35
ref
526
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
456
ref
457
ref
525
remove
nil
cons
cons
458
ref
518
ref
nil
cons
cons
nil
cons
528
def
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
524
remove
nil
cons
cons
35
ref
523
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
456
ref
457
ref
522
remove
nil
cons
cons
459
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
529
def
subst
nil
23
ref
472
ref
cons
nil
cons
nil
cons
cons
32
ref
subst
464
remove
assume
eqMp
trans
appThm
nil
23
ref
514
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
27
ref
72
ref
28
ref
appTerm
30
ref
appTerm
appTerm
28
ref
appTerm
absTerm
530
def
28
ref
appTerm
531
def
betaConv
nil
267
ref
530
ref
appTerm
532
def
axiom
nil
33
ref
532
remove
nil
cons
cons
35
ref
531
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
530
remove
nil
cons
cons
281
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
trans
sym
60
ref
"_17653"
436
ref
var
533
def
439
ref
533
remove
varTerm
appTerm
495
ref
appTerm
absTerm
534
def
496
ref
appTerm
betaConv
appThm
190
ref
45
ref
392
ref
appTerm
535
def
refl
534
ref
461
remove
appTerm
betaConv
appThm
appThm
45
ref
234
ref
392
remove
appTerm
536
def
appTerm
537
def
refl
534
ref
495
ref
appTerm
betaConv
appThm
appThm
appThm
nil
"_485"
436
ref
var
495
ref
nil
cons
538
def
cons
"_482"
436
ref
var
516
ref
cons
"_483"
5
ref
var
539
def
393
ref
cons
nil
cons
cons
cons
nil
cons
cons
nil
"_484"
437
remove
var
534
remove
nil
cons
cons
nil
cons
nil
cons
cons
456
ref
110
ref
cons
540
def
nil
99
ref
"_482"
2
ref
var
varTerm
nil
cons
cons
"c"
5
ref
var
541
def
539
remove
varTerm
nil
cons
cons
97
ref
"_484"
37
ref
var
varTerm
nil
cons
cons
325
ref
"_485"
2
ref
var
varTerm
nil
cons
cons
nil
cons
cons
cons
cons
nil
cons
cons
325
remove
27
ref
98
ref
485
remove
0
ref
5
ref
0
ref
2
ref
0
ref
2
ref
3
remove
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
541
ref
varTerm
542
def
appTerm
152
ref
appTerm
326
ref
appTerm
appTerm
appTerm
72
ref
45
ref
542
ref
appTerm
214
ref
appTerm
appTerm
45
ref
234
ref
542
ref
appTerm
appTerm
98
ref
326
ref
appTerm
appTerm
appTerm
appTerm
absTerm
543
def
326
remove
appTerm
544
def
betaConv
99
ref
39
ref
543
ref
appTerm
545
def
absTerm
546
def
152
ref
appTerm
547
def
betaConv
541
remove
39
ref
546
ref
appTerm
548
def
absTerm
549
def
542
ref
appTerm
550
def
betaConv
97
ref
267
ref
549
ref
appTerm
551
def
absTerm
552
def
98
ref
appTerm
553
def
betaConv
nil
224
ref
552
ref
appTerm
554
def
axiom
nil
33
ref
554
remove
nil
cons
cons
35
ref
553
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
227
ref
228
ref
552
remove
nil
cons
cons
231
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
551
remove
nil
cons
cons
35
ref
550
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
549
remove
nil
cons
cons
271
ref
542
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
548
remove
nil
cons
cons
35
ref
547
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
148
ref
94
ref
546
remove
nil
cons
cons
181
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
545
remove
nil
cons
cons
35
ref
544
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
148
ref
94
ref
543
remove
nil
cons
cons
340
remove
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
subst
subst
subst
eqMp
sym
nil
33
ref
393
ref
cons
35
ref
462
remove
495
ref
appTerm
555
def
nil
cons
556
def
cons
nil
cons
cons
nil
cons
cons
557
def
121
ref
subst
557
remove
93
ref
subst
nil
448
ref
516
remove
cons
558
def
nil
cons
nil
cons
cons
559
def
448
ref
512
ref
519
remove
appTerm
absTerm
560
def
449
ref
appTerm
561
def
betaConv
nil
454
ref
560
ref
appTerm
562
def
axiom
nil
33
ref
562
remove
nil
cons
cons
35
ref
561
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
456
ref
457
ref
560
remove
nil
cons
cons
459
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
eqMp
nil
132
ref
393
remove
cons
133
ref
556
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
nil
33
ref
535
remove
555
remove
appTerm
nil
cons
cons
35
ref
537
remove
439
ref
495
ref
appTerm
495
remove
appTerm
563
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
93
ref
subst
proveHyp
nil
33
ref
536
remove
nil
cons
564
def
cons
35
ref
563
remove
nil
cons
565
def
cons
nil
cons
cons
nil
cons
cons
566
def
121
ref
subst
566
remove
93
ref
subst
nil
558
remove
517
remove
cons
nil
cons
cons
529
remove
subst
559
remove
nil
23
ref
512
ref
449
ref
appTerm
567
def
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
448
ref
567
remove
absTerm
568
def
449
ref
appTerm
569
def
betaConv
nil
454
ref
568
ref
appTerm
570
def
axiom
nil
33
ref
570
remove
nil
cons
cons
35
ref
569
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
456
ref
457
ref
568
remove
nil
cons
cons
459
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
eqMp
subst
trans
sym
31
ref
eqMp
eqMp
nil
132
ref
564
remove
cons
133
ref
565
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
456
ref
457
ref
513
ref
nil
cons
cons
458
ref
538
remove
cons
nil
cons
cons
nil
cons
cons
27
ref
"Data.Bool.?"
const
571
def
38
remove
constTerm
572
def
95
ref
appTerm
573
def
appTerm
574
def
refl
97
ref
267
ref
35
ref
45
ref
39
ref
99
ref
45
ref
214
ref
appTerm
575
def
64
ref
appTerm
absTerm
appTerm
appTerm
64
ref
appTerm
absTerm
appTerm
absTerm
576
def
95
remove
appTerm
betaConv
appThm
nil
104
remove
572
ref
appTerm
576
remove
appTerm
axiom
105
remove
appThm
eqMp
577
def
sym
nil
270
ref
133
ref
45
ref
39
ref
99
ref
45
ref
153
remove
appTerm
578
def
137
ref
appTerm
absTerm
579
def
appTerm
580
def
appTerm
137
ref
appTerm
581
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
400
remove
subst
133
ref
nil
23
ref
581
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
33
ref
580
remove
nil
cons
582
def
cons
583
def
35
ref
420
ref
cons
nil
cons
584
def
cons
nil
cons
cons
585
def
121
ref
subst
585
ref
93
ref
subst
nil
33
ref
154
remove
cons
584
ref
cons
nil
cons
cons
146
ref
subst
579
ref
152
ref
appTerm
586
def
betaConv
nil
583
ref
35
ref
586
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
148
ref
94
ref
579
remove
nil
cons
cons
181
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
132
ref
582
remove
cons
587
def
133
ref
420
ref
cons
nil
cons
588
def
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
589
def
subst
proveHyp
nil
33
ref
571
ref
453
remove
constTerm
590
def
513
remove
appTerm
nil
cons
cons
35
ref
511
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
"p"
436
remove
var
591
def
477
remove
nil
cons
cons
515
ref
496
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
591
ref
45
ref
590
remove
448
ref
72
ref
521
remove
appTerm
512
remove
591
ref
varTerm
592
def
appTerm
appTerm
593
def
absTerm
594
def
appTerm
595
def
appTerm
596
def
520
remove
592
ref
appTerm
597
def
appTerm
598
def
absTerm
599
def
592
ref
appTerm
600
def
betaConv
515
ref
454
ref
599
ref
appTerm
601
def
absTerm
602
def
518
ref
appTerm
603
def
betaConv
nil
454
ref
515
ref
454
ref
448
ref
454
ref
591
ref
45
ref
593
ref
appTerm
597
ref
appTerm
absTerm
604
def
appTerm
605
def
absTerm
606
def
appTerm
607
def
absTerm
608
def
appTerm
609
def
axiom
nil
33
ref
609
ref
nil
cons
610
def
cons
611
def
35
ref
454
ref
602
ref
appTerm
nil
cons
612
def
cons
nil
cons
cons
nil
cons
cons
613
def
146
ref
subst
proveHyp
613
ref
121
ref
subst
613
remove
93
ref
subst
nil
457
ref
602
remove
nil
cons
cons
614
def
nil
cons
nil
cons
cons
540
remove
107
ref
subst
615
def
subst
515
remove
nil
23
ref
601
remove
nil
cons
616
def
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
457
ref
599
remove
nil
cons
cons
617
def
nil
cons
nil
cons
cons
615
ref
subst
591
remove
nil
23
ref
598
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
33
ref
595
remove
nil
cons
618
def
cons
619
def
35
ref
597
ref
nil
cons
620
def
cons
nil
cons
621
def
cons
nil
cons
cons
622
def
121
ref
subst
622
remove
93
ref
subst
nil
611
ref
621
ref
cons
nil
cons
cons
623
def
146
ref
subst
nil
619
remove
35
ref
45
ref
609
remove
appTerm
597
remove
appTerm
624
def
nil
cons
625
def
cons
nil
cons
626
def
cons
nil
cons
cons
146
ref
subst
nil
457
ref
448
ref
45
ref
594
ref
449
ref
appTerm
627
def
appTerm
624
ref
appTerm
628
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
615
remove
subst
448
remove
nil
23
ref
628
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
33
ref
627
ref
nil
cons
629
def
cons
626
ref
cons
nil
cons
cons
630
def
121
ref
subst
630
remove
93
ref
subst
627
ref
betaConv
627
remove
assume
eqMp
nil
33
ref
593
remove
nil
cons
631
def
cons
632
def
626
remove
cons
nil
cons
cons
633
def
146
ref
subst
proveHyp
633
ref
121
ref
subst
633
remove
93
ref
subst
623
ref
121
ref
subst
623
remove
93
ref
subst
nil
632
remove
621
remove
cons
nil
cons
cons
146
ref
subst
604
ref
592
ref
appTerm
634
def
betaConv
606
ref
449
remove
appTerm
635
def
betaConv
608
ref
518
remove
appTerm
636
def
betaConv
nil
611
remove
35
ref
636
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
456
ref
457
ref
608
remove
nil
cons
cons
528
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
607
remove
nil
cons
cons
35
ref
635
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
456
ref
457
ref
606
remove
nil
cons
cons
459
remove
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
605
remove
nil
cons
cons
35
ref
634
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
456
ref
457
ref
604
remove
nil
cons
cons
458
ref
592
remove
nil
cons
cons
nil
cons
637
def
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
132
ref
610
remove
cons
638
def
133
ref
620
remove
cons
nil
cons
639
def
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
nil
132
ref
631
remove
cons
133
ref
625
remove
cons
nil
cons
640
def
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
132
ref
629
remove
cons
640
ref
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
33
ref
454
remove
458
ref
45
ref
594
ref
458
remove
varTerm
appTerm
appTerm
624
ref
appTerm
absTerm
appTerm
nil
cons
cons
35
ref
596
remove
624
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
456
ref
457
remove
594
remove
nil
cons
cons
640
remove
cons
nil
cons
cons
nil
583
remove
35
ref
45
ref
573
ref
appTerm
641
def
137
ref
appTerm
nil
cons
642
def
cons
nil
cons
cons
nil
cons
cons
643
def
121
ref
subst
643
remove
93
ref
subst
nil
33
ref
573
remove
nil
cons
644
def
cons
645
def
584
remove
cons
nil
cons
cons
646
def
121
ref
subst
646
remove
93
ref
subst
585
remove
146
ref
subst
35
ref
45
ref
39
ref
99
ref
578
remove
64
ref
appTerm
absTerm
appTerm
appTerm
64
ref
appTerm
absTerm
647
def
137
remove
appTerm
648
def
betaConv
nil
645
remove
35
ref
267
ref
647
ref
appTerm
649
def
nil
cons
650
def
cons
nil
cons
cons
nil
cons
cons
651
def
146
ref
subst
577
remove
nil
33
ref
574
remove
649
ref
appTerm
nil
cons
cons
35
ref
641
remove
649
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
651
remove
nil
33
ref
248
remove
nil
cons
652
def
cons
35
ref
254
ref
cons
nil
cons
cons
nil
cons
cons
653
def
121
ref
subst
653
remove
93
ref
subst
253
remove
eqMp
nil
132
ref
652
remove
cons
133
ref
254
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
33
ref
650
remove
cons
35
ref
648
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
647
remove
nil
cons
cons
271
ref
420
remove
cons
nil
cons
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
132
ref
644
remove
cons
588
remove
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
nil
587
remove
133
ref
642
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
654
def
subst
eqMp
eqMp
eqMp
eqMp
nil
132
ref
618
remove
cons
639
remove
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
638
remove
133
ref
612
ref
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
nil
33
ref
612
remove
cons
35
ref
603
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
456
ref
614
remove
528
remove
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
616
remove
cons
35
ref
600
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
456
remove
617
remove
637
remove
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
eqMp
nil
132
ref
501
remove
cons
133
ref
499
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
nil
132
ref
472
remove
cons
133
ref
473
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
33
ref
72
ref
460
remove
appTerm
471
remove
appTerm
nil
cons
cons
35
ref
43
ref
182
ref
439
remove
442
remove
184
ref
appTerm
appTerm
446
ref
183
ref
appTerm
appTerm
absTerm
655
def
appTerm
656
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
189
ref
190
ref
655
ref
18
ref
appTerm
betaConv
appThm
191
ref
40
ref
192
ref
44
ref
189
ref
655
ref
46
ref
appTerm
betaConv
appThm
655
ref
52
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
192
ref
182
ref
655
ref
183
ref
appTerm
betaConv
absThm
appThm
appThm
nil
195
ref
655
remove
nil
cons
cons
nil
cons
nil
cons
cons
202
ref
subst
eqMp
eqMp
nil
656
remove
thm
192
ref
182
ref
60
ref
nil
97
ref
99
ref
240
ref
absTerm
657
def
nil
cons
cons
nil
cons
nil
cons
cons
426
ref
subst
191
ref
99
ref
427
ref
657
ref
152
ref
appTerm
betaConv
appThm
429
ref
23
ref
27
ref
430
remove
240
ref
appTerm
appTerm
234
ref
28
ref
appTerm
658
def
appTerm
absTerm
659
def
28
ref
appTerm
660
def
betaConv
nil
267
ref
659
ref
appTerm
661
def
axiom
nil
33
ref
661
remove
nil
cons
cons
35
ref
660
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
659
remove
nil
cons
cons
281
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
trans
absThm
appThm
60
ref
191
ref
99
ref
234
ref
refl
662
def
99
ref
212
ref
absTerm
663
def
152
ref
appTerm
betaConv
664
def
appThm
absThm
appThm
appThm
662
ref
572
ref
refl
665
def
99
ref
664
remove
absThm
appThm
appThm
appThm
nil
97
ref
663
remove
nil
cons
cons
nil
cons
nil
cons
cons
97
ref
27
ref
39
ref
99
ref
234
ref
214
ref
appTerm
666
def
absTerm
667
def
appTerm
668
def
appTerm
234
ref
572
ref
99
ref
214
ref
absTerm
669
def
appTerm
appTerm
670
def
appTerm
671
def
absTerm
672
def
98
ref
appTerm
673
def
betaConv
224
ref
refl
674
def
97
ref
671
remove
assume
sym
27
ref
670
remove
appTerm
668
remove
appTerm
675
def
assume
sym
deductAntisym
absThm
appThm
nil
224
ref
97
ref
675
remove
absTerm
appTerm
axiom
eqMp
nil
33
ref
224
ref
672
ref
appTerm
nil
cons
cons
35
ref
673
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
227
ref
228
ref
672
remove
nil
cons
cons
231
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
eqMp
662
ref
nil
163
ref
184
ref
nil
cons
cons
nil
cons
nil
cons
cons
163
ref
27
ref
572
ref
99
ref
330
ref
absTerm
appTerm
appTerm
234
ref
12
ref
167
ref
appTerm
20
ref
appTerm
appTerm
appTerm
absTerm
676
def
167
ref
appTerm
677
def
betaConv
nil
175
ref
676
ref
appTerm
678
def
axiom
nil
33
ref
678
remove
nil
cons
cons
35
ref
677
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
177
ref
178
ref
676
remove
nil
cons
cons
180
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
appThm
nil
23
ref
12
ref
184
remove
appTerm
20
ref
appTerm
679
def
nil
cons
680
def
cons
nil
cons
nil
cons
cons
23
ref
27
ref
234
ref
658
ref
appTerm
681
def
appTerm
28
ref
appTerm
682
def
absTerm
683
def
28
ref
appTerm
684
def
betaConv
nil
267
ref
683
ref
appTerm
685
def
axiom
686
def
nil
33
ref
685
remove
nil
cons
cons
35
ref
684
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
683
remove
nil
cons
cons
281
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
687
def
subst
trans
trans
trans
trans
appThm
182
ref
27
ref
"Data.List.null"
const
41
remove
constTerm
688
def
183
ref
appTerm
689
def
appTerm
690
def
679
ref
appTerm
691
def
absTerm
692
def
183
ref
appTerm
693
def
betaConv
192
ref
182
ref
691
remove
assume
sym
27
ref
679
remove
appTerm
694
def
689
ref
appTerm
695
def
assume
sym
deductAntisym
absThm
appThm
60
ref
12
ref
refl
696
def
22
remove
appThm
20
ref
refl
697
def
appThm
nil
179
remove
20
ref
nil
cons
cons
nil
cons
nil
cons
cons
177
ref
110
ref
cons
698
def
nil
23
ref
329
remove
152
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
157
remove
eqMp
699
def
subst
subst
trans
appThm
nil
23
ref
688
ref
18
ref
appTerm
700
def
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
700
ref
axiom
eqMp
appThm
291
ref
trans
sym
31
ref
eqMp
nil
33
ref
27
ref
21
remove
appTerm
700
remove
appTerm
701
def
nil
cons
cons
35
ref
39
ref
40
ref
43
ref
44
ref
45
ref
27
ref
12
ref
47
remove
appTerm
20
ref
appTerm
appTerm
688
ref
46
ref
appTerm
appTerm
702
def
appTerm
27
ref
122
remove
20
ref
appTerm
appTerm
688
remove
52
ref
appTerm
703
def
appTerm
704
def
appTerm
705
def
absTerm
706
def
appTerm
707
def
absTerm
708
def
appTerm
709
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
93
ref
subst
proveHyp
nil
94
ref
708
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
40
ref
nil
23
ref
707
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
108
ref
706
remove
nil
cons
cons
nil
cons
nil
cons
cons
112
ref
subst
44
ref
nil
23
ref
705
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
33
ref
702
remove
nil
cons
710
def
cons
35
ref
704
remove
nil
cons
711
def
cons
nil
cons
cons
nil
cons
cons
712
def
121
ref
subst
712
remove
93
ref
subst
60
ref
696
remove
162
remove
appThm
697
remove
appThm
166
remove
163
ref
234
ref
12
ref
168
remove
appTerm
20
remove
appTerm
713
def
appTerm
714
def
absTerm
715
def
167
ref
appTerm
716
def
betaConv
99
ref
175
ref
715
ref
appTerm
717
def
absTerm
718
def
152
ref
appTerm
719
def
betaConv
nil
39
ref
718
ref
appTerm
720
def
axiom
nil
33
ref
720
remove
nil
cons
cons
35
ref
719
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
148
ref
94
ref
718
remove
nil
cons
cons
181
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
717
remove
nil
cons
cons
35
ref
716
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
177
ref
178
ref
715
remove
nil
cons
cons
180
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
714
remove
nil
cons
cons
35
ref
27
ref
713
ref
appTerm
240
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
132
ref
713
remove
nil
cons
cons
nil
cons
nil
cons
cons
272
ref
subst
eqMp
subst
trans
appThm
44
ref
234
ref
703
ref
appTerm
721
def
absTerm
722
def
46
ref
appTerm
723
def
betaConv
40
ref
43
ref
722
ref
appTerm
724
def
absTerm
725
def
51
ref
appTerm
726
def
betaConv
nil
39
ref
725
ref
appTerm
727
def
axiom
nil
33
ref
727
remove
nil
cons
cons
35
ref
726
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
148
ref
94
ref
725
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
724
remove
nil
cons
cons
35
ref
723
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
109
ref
108
ref
722
remove
nil
cons
cons
161
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
721
remove
nil
cons
cons
35
ref
27
ref
703
ref
appTerm
240
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
132
ref
703
remove
nil
cons
cons
nil
cons
nil
cons
cons
272
ref
subst
eqMp
appThm
nil
23
ref
247
remove
cons
nil
cons
nil
cons
cons
23
ref
27
ref
266
remove
28
ref
appTerm
appTerm
658
remove
appTerm
absTerm
728
def
28
ref
appTerm
729
def
betaConv
nil
267
ref
728
ref
appTerm
730
def
axiom
nil
33
ref
730
remove
nil
cons
cons
35
ref
729
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
728
remove
nil
cons
cons
281
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
nil
27
ref
234
ref
240
ref
appTerm
appTerm
30
ref
appTerm
axiom
731
def
trans
732
def
trans
sym
31
ref
eqMp
eqMp
nil
132
ref
710
remove
cons
133
ref
711
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
33
ref
72
ref
701
remove
appTerm
709
remove
appTerm
nil
cons
cons
35
ref
43
ref
182
ref
695
remove
absTerm
733
def
appTerm
734
def
nil
cons
735
def
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
189
ref
190
ref
733
ref
18
ref
appTerm
betaConv
appThm
191
ref
40
ref
192
ref
44
ref
189
ref
733
ref
46
ref
appTerm
betaConv
appThm
733
ref
52
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
192
ref
182
ref
733
ref
183
ref
appTerm
736
def
betaConv
737
def
absThm
appThm
appThm
nil
195
ref
733
remove
nil
cons
738
def
cons
nil
cons
nil
cons
cons
202
ref
subst
eqMp
eqMp
739
def
eqMp
nil
33
ref
43
ref
692
ref
appTerm
nil
cons
cons
35
ref
693
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
109
ref
108
ref
692
remove
nil
cons
cons
425
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
appThm
nil
271
ref
680
remove
cons
nil
cons
nil
cons
cons
399
remove
699
remove
subst
740
def
subst
trans
absThm
appThm
435
ref
trans
sym
31
ref
eqMp
nil
43
ref
182
ref
27
ref
206
ref
657
remove
appTerm
183
ref
appTerm
appTerm
689
remove
appTerm
absTerm
appTerm
thm
739
ref
nil
734
remove
thm
192
ref
182
ref
60
ref
737
remove
739
remove
nil
33
ref
735
remove
cons
35
ref
736
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
109
ref
108
ref
738
remove
cons
425
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
182
ref
690
remove
10
ref
0
ref
15
remove
201
ref
cons
opType
constTerm
183
ref
appTerm
18
ref
appTerm
741
def
appTerm
absTerm
742
def
183
ref
appTerm
743
def
betaConv
nil
43
ref
742
ref
appTerm
744
def
axiom
nil
33
ref
744
remove
nil
cons
cons
35
ref
743
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
109
ref
108
ref
742
remove
nil
cons
cons
425
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
trans
appThm
741
ref
refl
appThm
nil
271
ref
741
ref
nil
cons
cons
nil
cons
nil
cons
cons
740
ref
subst
trans
absThm
appThm
435
ref
trans
sym
31
ref
eqMp
nil
43
ref
182
ref
694
remove
741
remove
appTerm
absTerm
appTerm
thm
nil
178
ref
163
ref
484
ref
12
remove
17
remove
"Data.List.fromSet"
const
0
ref
4
remove
50
remove
cons
opType
constTerm
167
ref
appTerm
745
def
appTerm
appTerm
167
ref
appTerm
746
def
appTerm
747
def
absTerm
748
def
nil
cons
cons
nil
cons
nil
cons
cons
698
remove
107
ref
subst
749
def
subst
163
ref
nil
23
ref
747
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
33
ref
169
ref
nil
cons
750
def
cons
751
def
35
ref
746
ref
nil
cons
752
def
cons
nil
cons
753
def
cons
nil
cons
cons
754
def
121
ref
subst
754
remove
93
ref
subst
163
ref
484
ref
72
ref
746
ref
appTerm
444
remove
446
remove
745
ref
appTerm
appTerm
487
remove
appTerm
755
def
appTerm
756
def
appTerm
757
def
absTerm
758
def
167
remove
appTerm
759
def
betaConv
nil
175
ref
758
ref
appTerm
760
def
axiom
nil
33
ref
760
remove
nil
cons
cons
35
ref
759
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
177
remove
178
ref
758
remove
nil
cons
cons
180
remove
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
761
def
nil
33
ref
757
remove
nil
cons
cons
762
def
753
ref
cons
nil
cons
cons
146
ref
subst
proveHyp
189
ref
189
ref
nil
23
ref
750
ref
cons
nil
cons
nil
cons
cons
32
ref
subst
169
remove
assume
eqMp
appThm
756
ref
refl
appThm
nil
23
ref
756
remove
nil
cons
763
def
cons
nil
cons
nil
cons
cons
505
ref
subst
trans
appThm
764
def
746
remove
refl
appThm
sym
nil
33
ref
763
ref
cons
765
def
753
remove
cons
nil
cons
cons
766
def
121
ref
subst
766
remove
93
ref
subst
nil
132
ref
752
ref
cons
133
ref
755
ref
nil
cons
767
def
cons
nil
cons
768
def
cons
nil
cons
cons
769
def
145
ref
subst
eqMp
nil
132
ref
763
remove
cons
770
def
133
ref
752
remove
cons
nil
cons
771
def
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
eqMp
772
def
eqMp
nil
132
ref
750
remove
cons
773
def
771
remove
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
175
ref
748
remove
appTerm
thm
nil
178
ref
163
ref
484
ref
755
ref
appTerm
774
def
absTerm
775
def
nil
cons
cons
nil
cons
nil
cons
cons
749
ref
subst
163
ref
nil
23
ref
774
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
751
ref
35
ref
767
remove
cons
nil
cons
776
def
cons
nil
cons
cons
777
def
121
ref
subst
777
remove
93
ref
subst
761
remove
nil
762
remove
776
ref
cons
nil
cons
cons
146
ref
subst
proveHyp
764
remove
755
remove
refl
appThm
sym
nil
765
remove
776
remove
cons
nil
cons
cons
778
def
121
ref
subst
778
remove
93
ref
subst
769
remove
258
ref
subst
eqMp
nil
770
remove
768
ref
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
773
ref
768
remove
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
175
ref
775
remove
appTerm
thm
191
ref
99
ref
60
ref
99
ref
234
ref
"Data.List.member"
const
0
ref
2
ref
201
remove
cons
opType
constTerm
152
ref
appTerm
779
def
18
ref
appTerm
780
def
appTerm
781
def
absTerm
782
def
152
ref
appTerm
783
def
betaConv
nil
39
ref
782
ref
appTerm
784
def
axiom
nil
33
ref
784
remove
nil
cons
cons
35
ref
783
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
148
ref
94
ref
782
remove
nil
cons
cons
181
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
781
remove
nil
cons
cons
35
ref
27
ref
780
ref
appTerm
785
def
240
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
132
ref
780
remove
nil
cons
cons
nil
cons
nil
cons
cons
272
ref
subst
eqMp
appThm
273
remove
appThm
732
remove
trans
absThm
appThm
287
ref
trans
sym
31
ref
eqMp
nil
33
ref
39
ref
99
ref
785
remove
292
remove
appTerm
absTerm
appTerm
786
def
nil
cons
cons
35
ref
39
ref
40
ref
43
ref
44
ref
45
ref
39
ref
99
ref
27
ref
779
ref
46
ref
appTerm
787
def
appTerm
295
remove
appTerm
absTerm
788
def
appTerm
789
def
appTerm
39
ref
99
ref
27
ref
779
ref
52
ref
appTerm
appTerm
790
def
302
remove
appTerm
absTerm
appTerm
791
def
appTerm
792
def
absTerm
793
def
appTerm
794
def
absTerm
795
def
appTerm
796
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
93
ref
subst
proveHyp
nil
94
ref
795
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
40
ref
nil
23
ref
794
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
108
ref
793
remove
nil
cons
cons
nil
cons
nil
cons
cons
112
ref
subst
44
ref
nil
23
ref
792
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
33
ref
789
remove
nil
cons
797
def
cons
798
def
35
ref
791
remove
nil
cons
799
def
cons
nil
cons
cons
nil
cons
cons
800
def
121
ref
subst
800
remove
93
ref
subst
191
ref
99
ref
60
ref
44
ref
790
remove
344
ref
787
remove
appTerm
appTerm
absTerm
801
def
46
ref
appTerm
802
def
betaConv
40
ref
43
ref
801
ref
appTerm
803
def
absTerm
804
def
51
ref
appTerm
805
def
betaConv
99
ref
39
ref
804
ref
appTerm
806
def
absTerm
807
def
152
ref
appTerm
808
def
betaConv
nil
39
ref
807
ref
appTerm
809
def
axiom
nil
33
ref
809
remove
nil
cons
cons
35
ref
808
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
148
ref
94
ref
807
remove
nil
cons
cons
181
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
806
remove
nil
cons
cons
35
ref
805
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
148
ref
94
ref
804
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
803
remove
nil
cons
cons
35
ref
802
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
109
ref
108
ref
801
remove
nil
cons
cons
161
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
344
remove
refl
788
ref
152
ref
appTerm
810
def
betaConv
nil
798
remove
35
ref
810
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
148
ref
94
ref
788
remove
nil
cons
cons
181
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
appThm
trans
appThm
341
remove
appThm
nil
271
ref
360
remove
cons
nil
cons
nil
cons
cons
740
ref
subst
trans
absThm
appThm
287
ref
trans
sym
31
ref
eqMp
eqMp
nil
132
ref
797
remove
cons
133
ref
799
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
33
ref
72
ref
786
remove
appTerm
796
remove
appTerm
nil
cons
cons
35
ref
43
ref
182
ref
39
ref
99
ref
27
ref
779
ref
183
ref
appTerm
811
def
appTerm
212
ref
appTerm
absTerm
812
def
appTerm
813
def
absTerm
814
def
appTerm
815
def
nil
cons
816
def
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
189
ref
190
ref
814
ref
18
ref
appTerm
betaConv
appThm
191
ref
40
ref
192
ref
44
ref
189
ref
814
ref
46
ref
appTerm
betaConv
appThm
814
ref
52
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
192
ref
182
ref
814
ref
183
ref
appTerm
817
def
betaConv
818
def
absThm
appThm
appThm
nil
195
ref
814
remove
nil
cons
819
def
cons
nil
cons
nil
cons
cons
202
ref
subst
eqMp
eqMp
820
def
nil
815
remove
thm
nil
228
ref
97
ref
43
ref
182
ref
27
ref
234
ref
208
ref
appTerm
821
def
appTerm
822
def
"Data.List.any"
const
823
def
205
remove
constTerm
824
def
667
ref
appTerm
183
ref
appTerm
825
def
appTerm
826
def
absTerm
827
def
appTerm
828
def
absTerm
829
def
nil
cons
cons
nil
cons
nil
cons
cons
227
ref
110
ref
cons
830
def
107
ref
subst
831
def
subst
97
ref
nil
23
ref
828
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
108
ref
827
remove
nil
cons
cons
nil
cons
nil
cons
cons
112
ref
subst
182
ref
nil
23
ref
826
ref
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
822
remove
refl
832
def
nil
97
ref
667
ref
nil
cons
cons
nil
cons
nil
cons
cons
833
def
182
ref
27
ref
824
ref
98
ref
appTerm
834
def
183
ref
appTerm
835
def
appTerm
836
def
234
ref
206
ref
667
ref
appTerm
837
def
183
ref
appTerm
838
def
appTerm
839
def
appTerm
840
def
absTerm
841
def
183
ref
appTerm
842
def
betaConv
97
ref
43
ref
841
ref
appTerm
843
def
absTerm
844
def
98
ref
appTerm
845
def
betaConv
674
ref
97
ref
192
ref
182
ref
840
remove
assume
sym
27
ref
839
remove
appTerm
835
ref
appTerm
846
def
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
674
ref
97
ref
192
ref
182
ref
60
ref
662
ref
182
ref
27
ref
838
ref
appTerm
234
ref
835
ref
appTerm
847
def
appTerm
848
def
absTerm
849
def
183
ref
appTerm
850
def
betaConv
97
ref
43
ref
849
ref
appTerm
851
def
absTerm
852
def
98
ref
appTerm
853
def
betaConv
674
ref
97
ref
192
ref
182
ref
848
remove
assume
sym
27
ref
847
remove
appTerm
838
remove
appTerm
854
def
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
nil
228
ref
97
ref
43
ref
182
ref
854
remove
absTerm
855
def
appTerm
856
def
absTerm
857
def
nil
cons
cons
nil
cons
nil
cons
cons
831
ref
subst
97
ref
nil
23
ref
856
remove
nil
cons
858
def
cons
nil
cons
nil
cons
cons
32
ref
subst
60
ref
662
ref
97
ref
234
ref
834
ref
18
ref
appTerm
859
def
appTerm
860
def
absTerm
861
def
98
ref
appTerm
862
def
betaConv
nil
224
ref
861
ref
appTerm
863
def
axiom
nil
33
ref
863
remove
nil
cons
cons
35
ref
862
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
227
ref
228
ref
861
remove
nil
cons
cons
231
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
860
ref
nil
cons
cons
35
ref
27
ref
859
ref
appTerm
240
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
nil
132
ref
859
remove
nil
cons
cons
nil
cons
nil
cons
cons
272
remove
subst
eqMp
appThm
731
remove
trans
appThm
833
ref
232
ref
subst
appThm
291
ref
trans
sym
31
ref
eqMp
nil
33
ref
27
ref
860
remove
appTerm
837
ref
18
ref
appTerm
appTerm
864
def
nil
cons
cons
35
ref
39
ref
40
ref
43
ref
44
ref
45
ref
27
ref
234
ref
834
ref
46
ref
appTerm
865
def
appTerm
appTerm
837
ref
46
ref
appTerm
866
def
appTerm
867
def
appTerm
27
ref
234
ref
834
remove
52
ref
appTerm
868
def
appTerm
appTerm
837
remove
52
ref
appTerm
appTerm
869
def
appTerm
870
def
absTerm
871
def
appTerm
872
def
absTerm
873
def
appTerm
874
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
93
ref
subst
proveHyp
nil
94
ref
873
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
40
ref
nil
23
ref
872
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
108
ref
871
remove
nil
cons
cons
nil
cons
nil
cons
cons
112
ref
subst
44
ref
nil
23
ref
870
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
33
ref
867
ref
nil
cons
875
def
cons
35
ref
869
remove
nil
cons
876
def
cons
nil
cons
cons
nil
cons
cons
877
def
121
ref
subst
877
remove
93
ref
subst
60
ref
662
ref
44
ref
27
ref
868
remove
appTerm
327
ref
312
ref
appTerm
865
ref
appTerm
appTerm
absTerm
878
def
46
ref
appTerm
879
def
betaConv
40
ref
43
ref
878
ref
appTerm
880
def
absTerm
881
def
51
ref
appTerm
882
def
betaConv
97
ref
39
ref
881
ref
appTerm
883
def
absTerm
884
def
98
ref
appTerm
885
def
betaConv
nil
224
ref
884
ref
appTerm
886
def
axiom
nil
33
ref
886
remove
nil
cons
cons
35
ref
885
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
227
ref
228
ref
884
remove
nil
cons
cons
231
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
883
remove
nil
cons
cons
35
ref
882
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
148
ref
94
ref
881
remove
nil
cons
cons
150
remove
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
880
remove
nil
cons
cons
35
ref
879
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
109
ref
108
ref
878
remove
nil
cons
cons
161
remove
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
appThm
nil
"t2"
5
ref
var
887
def
865
remove
nil
cons
cons
"t1"
5
remove
var
888
def
355
remove
cons
nil
cons
cons
nil
cons
cons
887
ref
27
ref
234
ref
327
remove
888
ref
varTerm
889
def
appTerm
887
ref
varTerm
890
def
appTerm
appTerm
appTerm
72
ref
234
ref
889
ref
appTerm
appTerm
234
ref
890
ref
appTerm
891
def
appTerm
appTerm
absTerm
892
def
890
ref
appTerm
893
def
betaConv
888
ref
267
ref
892
ref
appTerm
894
def
absTerm
895
def
889
ref
appTerm
896
def
betaConv
nil
267
ref
895
ref
appTerm
897
def
axiom
nil
33
ref
897
remove
nil
cons
cons
35
ref
896
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
895
remove
nil
cons
cons
271
ref
889
ref
nil
cons
cons
nil
cons
898
def
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
894
remove
nil
cons
cons
35
ref
893
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
892
remove
nil
cons
cons
271
ref
890
ref
nil
cons
cons
nil
cons
899
def
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
72
ref
234
ref
312
remove
appTerm
appTerm
900
def
refl
867
remove
assume
appThm
trans
trans
appThm
833
ref
324
ref
subst
190
ref
667
ref
51
ref
appTerm
betaConv
appThm
866
ref
refl
appThm
trans
appThm
nil
271
ref
900
remove
866
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
740
ref
subst
trans
sym
31
ref
eqMp
eqMp
nil
132
ref
875
remove
cons
133
ref
876
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
33
ref
72
ref
864
remove
appTerm
874
remove
appTerm
nil
cons
cons
35
ref
858
ref
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
189
ref
190
ref
855
ref
18
ref
appTerm
betaConv
appThm
191
ref
40
ref
192
ref
44
ref
189
ref
855
ref
46
ref
appTerm
betaConv
appThm
855
ref
52
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
192
ref
182
ref
855
ref
183
ref
appTerm
901
def
betaConv
902
def
absThm
appThm
appThm
nil
195
ref
855
remove
nil
cons
903
def
cons
nil
cons
nil
cons
cons
202
ref
subst
eqMp
eqMp
904
def
eqMp
absThm
eqMp
905
def
eqMp
nil
33
ref
224
ref
852
ref
appTerm
nil
cons
cons
35
ref
853
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
227
ref
228
ref
852
remove
nil
cons
cons
231
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
851
remove
nil
cons
cons
35
ref
850
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
109
ref
108
ref
849
remove
nil
cons
cons
425
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
appThm
nil
23
ref
835
ref
nil
cons
906
def
cons
nil
cons
nil
cons
cons
907
def
687
ref
subst
trans
appThm
835
ref
refl
appThm
nil
271
ref
906
remove
cons
nil
cons
nil
cons
cons
740
ref
subst
trans
absThm
appThm
435
ref
trans
absThm
appThm
282
ref
830
remove
286
remove
subst
subst
908
def
trans
sym
31
ref
eqMp
909
def
eqMp
nil
33
ref
224
ref
844
ref
appTerm
nil
cons
cons
35
ref
845
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
227
ref
228
ref
844
remove
nil
cons
cons
231
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
843
remove
nil
cons
cons
35
ref
842
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
109
ref
108
ref
841
remove
nil
cons
cons
425
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
662
ref
206
ref
refl
910
def
99
ref
662
ref
667
ref
152
ref
appTerm
betaConv
911
def
appThm
276
ref
687
ref
subst
912
def
trans
absThm
appThm
183
ref
refl
913
def
appThm
appThm
trans
appThm
sym
832
remove
662
ref
910
remove
147
remove
"B"
6
ref
cons
nil
cons
cons
"t"
37
ref
var
230
remove
cons
nil
cons
nil
cons
cons
"t"
0
ref
2
ref
"B"
varType
914
def
nil
cons
915
def
cons
opType
916
def
var
917
def
10
remove
0
ref
916
ref
0
ref
916
ref
6
ref
cons
opType
918
def
nil
cons
cons
opType
constTerm
99
ref
917
remove
varTerm
919
def
152
ref
appTerm
absTerm
appTerm
919
ref
appTerm
absTerm
920
def
919
ref
appTerm
921
def
betaConv
nil
36
ref
0
ref
918
ref
6
ref
cons
opType
constTerm
920
ref
appTerm
922
def
axiom
nil
33
ref
922
remove
nil
cons
cons
35
ref
921
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
"A"
916
ref
nil
cons
cons
nil
cons
"P"
918
remove
var
920
remove
nil
cons
cons
"x"
916
remove
var
919
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
appThm
913
remove
appThm
appThm
appThm
sym
821
ref
refl
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
923
def
nil
224
ref
829
remove
appTerm
thm
905
remove
nil
224
ref
857
remove
appTerm
thm
909
remove
nil
224
ref
97
ref
43
ref
182
ref
846
remove
absTerm
appTerm
absTerm
appTerm
thm
674
ref
97
ref
192
ref
182
ref
60
ref
662
ref
182
ref
27
ref
825
ref
appTerm
821
remove
appTerm
924
def
absTerm
925
def
183
ref
appTerm
926
def
betaConv
97
ref
43
ref
925
ref
appTerm
927
def
absTerm
928
def
98
ref
appTerm
929
def
betaConv
674
ref
97
ref
192
ref
182
ref
924
remove
assume
sym
826
remove
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
923
remove
eqMp
nil
33
ref
224
ref
928
ref
appTerm
nil
cons
cons
35
ref
929
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
227
ref
228
ref
928
remove
nil
cons
cons
231
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
927
remove
nil
cons
cons
35
ref
926
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
109
ref
108
ref
925
remove
nil
cons
cons
425
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
appThm
nil
23
ref
208
ref
nil
cons
930
def
cons
nil
cons
nil
cons
cons
687
remove
subst
trans
appThm
208
ref
refl
appThm
nil
271
ref
930
remove
cons
nil
cons
nil
cons
cons
740
ref
subst
trans
absThm
appThm
435
ref
trans
absThm
appThm
908
ref
trans
sym
31
ref
eqMp
nil
224
ref
97
ref
43
ref
182
ref
27
ref
234
ref
825
remove
appTerm
appTerm
208
ref
appTerm
absTerm
appTerm
absTerm
appTerm
thm
nil
178
remove
163
ref
484
remove
39
ref
99
ref
27
ref
779
remove
745
ref
appTerm
appTerm
330
ref
appTerm
absTerm
appTerm
931
def
appTerm
932
def
absTerm
933
def
nil
cons
cons
nil
cons
nil
cons
cons
749
remove
subst
163
remove
nil
23
ref
932
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
751
remove
35
ref
931
remove
nil
cons
934
def
cons
nil
cons
cons
nil
cons
cons
935
def
121
ref
subst
935
remove
93
ref
subst
191
ref
99
ref
60
ref
nil
182
ref
745
remove
nil
cons
cons
nil
cons
nil
cons
cons
812
ref
152
ref
appTerm
936
def
betaConv
818
remove
820
remove
nil
33
ref
816
remove
cons
35
ref
817
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
109
ref
108
ref
819
remove
cons
425
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
813
remove
nil
cons
cons
35
ref
936
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
148
ref
94
ref
812
remove
nil
cons
cons
181
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
937
def
subst
233
remove
772
remove
appThm
trans
appThm
330
ref
refl
appThm
nil
271
ref
330
remove
nil
cons
cons
nil
cons
nil
cons
cons
740
ref
subst
trans
absThm
appThm
287
ref
trans
sym
31
ref
eqMp
eqMp
nil
773
remove
133
ref
934
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
175
remove
933
remove
appTerm
thm
674
ref
97
ref
192
ref
182
ref
60
ref
191
ref
99
ref
189
ref
937
ref
appThm
274
ref
appThm
absThm
appThm
appThm
426
ref
appThm
nil
271
ref
217
ref
nil
cons
938
def
cons
nil
cons
nil
cons
cons
740
ref
subst
trans
absThm
appThm
435
ref
trans
absThm
appThm
908
ref
trans
sym
31
ref
eqMp
nil
224
ref
97
ref
43
ref
182
ref
27
ref
39
ref
99
ref
45
ref
811
ref
appTerm
214
ref
appTerm
absTerm
appTerm
appTerm
208
ref
appTerm
absTerm
appTerm
absTerm
appTerm
thm
674
ref
97
ref
192
ref
182
ref
60
ref
665
ref
99
ref
190
ref
937
remove
appThm
274
ref
appThm
939
def
absThm
appThm
appThm
60
ref
907
remove
23
ref
29
remove
681
remove
appTerm
940
def
absTerm
941
def
28
ref
appTerm
942
def
betaConv
267
ref
refl
23
ref
940
remove
assume
sym
682
remove
assume
sym
deductAntisym
absThm
appThm
686
remove
eqMp
nil
33
ref
267
ref
941
ref
appTerm
nil
cons
cons
35
ref
942
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
941
remove
nil
cons
cons
281
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
appThm
572
ref
99
ref
72
ref
212
ref
appTerm
943
def
214
ref
appTerm
944
def
absTerm
945
def
appTerm
946
def
refl
947
def
appThm
sym
60
ref
662
ref
902
remove
904
remove
nil
33
ref
858
remove
cons
35
ref
901
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
109
remove
108
ref
903
remove
cons
425
remove
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
appThm
appThm
947
remove
appThm
sym
662
ref
833
remove
426
ref
subst
191
ref
99
ref
427
ref
911
remove
appThm
absThm
appThm
trans
appThm
60
ref
662
ref
191
ref
99
ref
99
ref
213
ref
666
ref
appTerm
absTerm
948
def
152
ref
appTerm
betaConv
949
def
absThm
appThm
appThm
appThm
665
ref
99
ref
662
remove
949
remove
appThm
absThm
appThm
appThm
nil
97
ref
948
remove
nil
cons
cons
nil
cons
nil
cons
cons
97
ref
27
ref
234
ref
39
ref
669
remove
appTerm
appTerm
appTerm
572
ref
667
remove
appTerm
appTerm
absTerm
950
def
98
remove
appTerm
951
def
betaConv
nil
224
ref
950
ref
appTerm
952
def
axiom
nil
33
ref
952
remove
nil
cons
cons
35
ref
951
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
227
ref
228
ref
950
remove
nil
cons
cons
231
remove
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
eqMp
665
ref
99
ref
nil
887
ref
666
remove
nil
cons
cons
888
ref
428
ref
cons
nil
cons
cons
nil
cons
cons
887
remove
27
ref
234
remove
45
ref
889
ref
appTerm
890
ref
appTerm
appTerm
appTerm
72
ref
889
ref
appTerm
891
remove
appTerm
appTerm
absTerm
953
def
890
remove
appTerm
954
def
betaConv
888
remove
267
ref
953
ref
appTerm
955
def
absTerm
956
def
889
remove
appTerm
957
def
betaConv
nil
267
ref
956
ref
appTerm
958
def
axiom
nil
33
ref
958
remove
nil
cons
cons
35
ref
957
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
956
remove
nil
cons
cons
898
remove
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
955
remove
nil
cons
cons
35
ref
954
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
953
remove
nil
cons
cons
899
remove
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
943
ref
refl
912
remove
appThm
trans
absThm
appThm
trans
trans
eqMp
eqMp
959
def
appThm
nil
271
ref
946
ref
nil
cons
960
def
cons
nil
cons
nil
cons
cons
740
remove
subst
trans
absThm
appThm
435
remove
trans
absThm
appThm
908
remove
trans
sym
31
ref
eqMp
nil
224
ref
97
ref
43
ref
182
ref
27
ref
572
ref
99
ref
72
ref
811
remove
appTerm
214
ref
appTerm
961
def
absTerm
appTerm
appTerm
835
ref
appTerm
absTerm
appTerm
absTerm
appTerm
thm
nil
228
ref
97
ref
421
remove
absTerm
962
def
nil
cons
cons
nil
cons
nil
cons
cons
831
ref
subst
97
ref
nil
23
ref
422
remove
cons
nil
cons
nil
cons
cons
32
ref
subst
424
remove
eqMp
absThm
eqMp
nil
224
ref
962
remove
appTerm
thm
nil
228
ref
97
ref
43
ref
182
ref
836
remove
946
ref
appTerm
963
def
absTerm
964
def
appTerm
965
def
absTerm
966
def
nil
cons
cons
nil
cons
nil
cons
cons
831
ref
subst
97
ref
nil
23
ref
965
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
108
ref
964
remove
nil
cons
cons
nil
cons
nil
cons
cons
112
ref
subst
182
ref
nil
23
ref
963
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
959
ref
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
224
ref
966
remove
appTerm
thm
nil
"P"
0
ref
0
ref
2
remove
0
ref
914
ref
6
ref
cons
opType
967
def
nil
cons
cons
opType
968
def
6
ref
cons
opType
969
def
var
970
def
"p"
968
ref
var
971
def
36
ref
0
ref
0
ref
14
remove
915
ref
opType
972
def
6
ref
cons
opType
973
def
6
ref
cons
opType
constTerm
974
def
"l"
972
ref
var
975
def
27
ref
39
ref
99
ref
204
remove
0
ref
967
ref
973
ref
nil
cons
cons
opType
976
def
constTerm
977
def
971
ref
varTerm
978
def
152
ref
appTerm
979
def
appTerm
975
ref
varTerm
980
def
appTerm
absTerm
appTerm
appTerm
977
remove
"y"
914
ref
var
981
def
39
ref
99
ref
979
ref
981
ref
varTerm
appTerm
982
def
absTerm
983
def
appTerm
absTerm
984
def
appTerm
980
ref
appTerm
appTerm
985
def
absTerm
986
def
appTerm
987
def
absTerm
988
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
968
ref
nil
cons
cons
nil
cons
989
def
110
ref
cons
107
ref
subst
990
def
subst
971
ref
nil
23
ref
987
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
"P"
973
remove
var
991
def
986
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
972
ref
nil
cons
cons
nil
cons
110
ref
cons
107
ref
subst
992
def
subst
975
ref
nil
23
ref
985
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
60
ref
191
ref
99
ref
nil
"p"
967
ref
var
993
def
979
ref
nil
cons
cons
nil
cons
nil
cons
cons
994
def
"A"
915
ref
cons
nil
cons
110
remove
cons
995
def
426
ref
subst
996
def
subst
absThm
appThm
appThm
nil
993
ref
984
ref
nil
cons
cons
nil
cons
nil
cons
cons
996
remove
subst
36
ref
0
ref
967
remove
6
ref
cons
opType
997
def
constTerm
998
def
refl
999
def
"x"
914
ref
var
1000
def
45
ref
209
remove
0
ref
914
remove
0
ref
1
remove
915
remove
opType
1001
def
6
ref
cons
opType
nil
cons
cons
opType
constTerm
1000
ref
varTerm
1002
def
appTerm
13
remove
0
ref
972
remove
1001
remove
nil
cons
cons
opType
constTerm
980
ref
appTerm
appTerm
1003
def
appTerm
1004
def
refl
1005
def
984
ref
1002
ref
appTerm
betaConv
appThm
60
ref
1005
ref
191
ref
99
ref
99
ref
979
ref
1002
ref
appTerm
1006
def
absTerm
1007
def
152
ref
appTerm
betaConv
1008
def
absThm
1009
def
appThm
appThm
appThm
191
ref
99
ref
1005
remove
1008
ref
appThm
absThm
appThm
appThm
nil
"q"
37
ref
var
1010
def
1007
remove
nil
cons
cons
33
ref
1003
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
1011
def
1010
ref
27
ref
116
ref
39
ref
99
ref
1010
ref
varTerm
1012
def
152
ref
appTerm
1013
def
absTerm
1014
def
appTerm
appTerm
appTerm
39
ref
99
ref
116
ref
1013
ref
appTerm
absTerm
appTerm
appTerm
absTerm
1015
def
1012
ref
appTerm
1016
def
betaConv
33
ref
224
ref
1015
ref
appTerm
1017
def
absTerm
1018
def
63
ref
appTerm
1019
def
betaConv
nil
267
ref
1018
ref
appTerm
1020
def
axiom
nil
33
ref
1020
remove
nil
cons
cons
35
ref
1019
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
1018
remove
nil
cons
cons
271
ref
88
remove
cons
nil
cons
1021
def
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
1017
remove
nil
cons
cons
35
ref
1016
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
227
ref
228
ref
1015
remove
nil
cons
cons
229
remove
1012
ref
nil
cons
1022
def
cons
nil
cons
1023
def
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
eqMp
trans
absThm
appThm
trans
appThm
sym
60
ref
191
ref
99
ref
999
ref
1000
ref
99
ref
1000
ref
1004
remove
1006
ref
appTerm
absTerm
1024
def
absTerm
1025
def
152
ref
appTerm
betaConv
1002
ref
refl
1026
def
appThm
1024
remove
1002
ref
appTerm
betaConv
trans
1027
def
absThm
appThm
absThm
appThm
appThm
999
remove
1000
ref
191
ref
99
ref
1027
remove
absThm
appThm
absThm
appThm
appThm
nil
971
ref
1025
remove
nil
cons
cons
nil
cons
nil
cons
cons
971
ref
27
ref
39
ref
99
ref
998
ref
981
ref
982
remove
absTerm
1028
def
appTerm
absTerm
appTerm
appTerm
998
remove
984
remove
appTerm
appTerm
absTerm
1029
def
978
ref
appTerm
1030
def
betaConv
nil
36
remove
0
remove
969
remove
6
remove
cons
opType
constTerm
1031
def
1029
ref
appTerm
1032
def
axiom
nil
33
ref
1032
remove
nil
cons
cons
35
ref
1030
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
989
ref
970
ref
1029
remove
nil
cons
cons
"x"
968
remove
var
978
ref
nil
cons
cons
nil
cons
1033
def
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
1031
ref
988
remove
appTerm
thm
nil
970
ref
971
ref
974
remove
975
ref
27
ref
572
ref
99
ref
823
remove
976
remove
constTerm
1034
def
979
remove
appTerm
980
ref
appTerm
absTerm
appTerm
appTerm
1034
remove
981
remove
572
ref
983
remove
appTerm
absTerm
1035
def
appTerm
980
remove
appTerm
appTerm
1036
def
absTerm
1037
def
appTerm
1038
def
absTerm
1039
def
nil
cons
cons
nil
cons
nil
cons
cons
990
remove
subst
971
ref
nil
23
ref
1038
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
991
remove
1037
remove
nil
cons
cons
nil
cons
nil
cons
cons
992
remove
subst
975
remove
nil
23
ref
1036
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
60
ref
665
ref
99
ref
994
remove
995
remove
959
ref
subst
1040
def
subst
absThm
appThm
appThm
nil
993
remove
1035
ref
nil
cons
cons
nil
cons
nil
cons
cons
1040
remove
subst
571
remove
997
remove
constTerm
1041
def
refl
1042
def
1000
ref
72
ref
1003
remove
appTerm
1043
def
refl
1044
def
1035
ref
1002
ref
appTerm
betaConv
appThm
60
ref
1044
ref
665
ref
1009
remove
appThm
appThm
appThm
665
ref
99
ref
1044
remove
1008
remove
appThm
absThm
appThm
appThm
1011
remove
1010
ref
27
ref
73
ref
572
ref
1014
remove
appTerm
appTerm
appTerm
572
ref
99
ref
73
remove
1013
ref
appTerm
absTerm
appTerm
appTerm
absTerm
1045
def
1012
ref
appTerm
1046
def
betaConv
33
ref
224
ref
1045
ref
appTerm
1047
def
absTerm
1048
def
63
ref
appTerm
1049
def
betaConv
nil
267
ref
1048
ref
appTerm
1050
def
axiom
nil
33
ref
1050
remove
nil
cons
cons
35
ref
1049
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
1048
remove
nil
cons
cons
1021
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
1047
remove
nil
cons
cons
35
ref
1046
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
227
remove
228
ref
1045
remove
nil
cons
cons
1023
remove
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
eqMp
trans
absThm
appThm
trans
appThm
sym
60
ref
665
ref
99
ref
1042
ref
1000
ref
99
ref
1000
ref
1043
remove
1006
remove
appTerm
absTerm
1051
def
absTerm
1052
def
152
ref
appTerm
betaConv
1026
remove
appThm
1051
remove
1002
remove
appTerm
betaConv
trans
1053
def
absThm
appThm
absThm
appThm
appThm
1042
remove
1000
remove
665
remove
99
ref
1053
remove
absThm
appThm
absThm
appThm
appThm
nil
971
ref
1052
remove
nil
cons
cons
nil
cons
nil
cons
cons
971
remove
27
ref
572
ref
99
ref
1041
ref
1028
remove
appTerm
absTerm
appTerm
appTerm
1041
remove
1035
remove
appTerm
appTerm
absTerm
1054
def
978
remove
appTerm
1055
def
betaConv
nil
1031
ref
1054
ref
appTerm
1056
def
axiom
nil
33
ref
1056
remove
nil
cons
cons
35
ref
1055
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
989
remove
970
remove
1054
remove
nil
cons
cons
1033
remove
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
1031
remove
1039
remove
appTerm
thm
nil
228
ref
97
ref
224
ref
1010
ref
43
ref
182
ref
27
ref
206
ref
99
ref
72
ref
214
ref
appTerm
1013
ref
appTerm
1057
def
absTerm
1058
def
appTerm
183
ref
appTerm
appTerm
72
ref
208
ref
appTerm
1059
def
206
ref
1012
ref
appTerm
1060
def
183
ref
appTerm
1061
def
appTerm
appTerm
1062
def
absTerm
1063
def
appTerm
1064
def
absTerm
1065
def
appTerm
1066
def
absTerm
1067
def
nil
cons
cons
nil
cons
nil
cons
cons
831
ref
subst
97
ref
nil
23
ref
1066
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
228
ref
1065
remove
nil
cons
cons
nil
cons
nil
cons
cons
831
ref
subst
1010
ref
nil
23
ref
1064
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
108
ref
1063
remove
nil
cons
cons
nil
cons
nil
cons
cons
112
ref
subst
182
ref
nil
23
ref
1062
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
60
ref
nil
97
ref
1058
ref
nil
cons
cons
nil
cons
nil
cons
cons
426
ref
subst
191
ref
99
ref
427
ref
1058
remove
152
ref
appTerm
betaConv
appThm
absThm
appThm
trans
appThm
190
ref
426
ref
appThm
nil
97
ref
1022
remove
cons
nil
cons
nil
cons
cons
1068
def
426
ref
subst
1069
def
appThm
appThm
sym
nil
33
ref
39
ref
99
ref
213
ref
1057
ref
appTerm
1070
def
absTerm
1071
def
appTerm
1072
def
nil
cons
1073
def
cons
1074
def
35
ref
72
ref
217
ref
appTerm
39
ref
99
ref
213
remove
1013
ref
appTerm
1075
def
absTerm
1076
def
appTerm
1077
def
appTerm
1078
def
nil
cons
1079
def
cons
nil
cons
cons
nil
cons
cons
1080
def
259
remove
subst
1080
ref
121
ref
subst
1080
remove
93
ref
subst
nil
94
ref
216
ref
nil
cons
cons
1081
def
nil
cons
nil
cons
cons
107
ref
subst
99
ref
nil
23
ref
215
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
33
ref
428
ref
cons
1082
def
362
ref
cons
nil
cons
cons
1083
def
121
ref
subst
190
ref
429
remove
32
ref
subst
212
remove
assume
eqMp
1084
def
appThm
274
ref
appThm
276
remove
23
ref
27
ref
72
ref
30
remove
appTerm
28
ref
appTerm
appTerm
28
ref
appTerm
absTerm
1085
def
28
remove
appTerm
1086
def
betaConv
nil
267
ref
1085
ref
appTerm
1087
def
axiom
nil
33
ref
1087
remove
nil
cons
cons
35
ref
1086
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
1085
remove
nil
cons
cons
281
remove
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
1088
def
subst
trans
sym
1089
def
1071
ref
152
ref
appTerm
1090
def
betaConv
nil
1074
remove
35
ref
1090
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
148
ref
94
ref
1071
remove
nil
cons
cons
1091
def
181
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
1092
def
nil
33
ref
1070
remove
nil
cons
1093
def
cons
1094
def
362
ref
cons
nil
cons
cons
146
ref
subst
proveHyp
189
ref
189
ref
1084
remove
appThm
1057
ref
refl
appThm
nil
23
ref
1057
remove
nil
cons
1095
def
cons
nil
cons
nil
cons
cons
505
remove
subst
trans
appThm
1096
def
274
remove
appThm
sym
nil
33
ref
1095
ref
cons
1097
def
362
remove
cons
nil
cons
cons
1098
def
121
ref
subst
1098
remove
93
ref
subst
nil
132
ref
275
ref
cons
133
ref
1013
ref
nil
cons
1099
def
cons
nil
cons
1100
def
cons
nil
cons
cons
1101
def
145
ref
subst
eqMp
nil
132
ref
1095
ref
cons
1102
def
369
ref
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
132
ref
428
remove
cons
1103
def
369
remove
cons
nil
cons
cons
1104
def
145
ref
subst
1105
def
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
33
ref
938
ref
cons
1106
def
35
ref
1077
ref
nil
cons
1107
def
cons
nil
cons
1108
def
cons
nil
cons
cons
93
ref
subst
proveHyp
nil
94
ref
1076
ref
nil
cons
cons
1109
def
nil
cons
nil
cons
cons
107
ref
subst
1110
def
99
ref
nil
23
ref
1075
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
1111
def
nil
1082
ref
35
ref
1099
ref
cons
nil
cons
1112
def
cons
nil
cons
cons
1113
def
121
ref
subst
1114
def
1113
ref
93
ref
subst
1115
def
1092
remove
nil
1094
remove
1112
ref
cons
nil
cons
cons
146
ref
subst
proveHyp
1096
remove
1013
ref
refl
1116
def
appThm
sym
nil
1097
remove
1112
ref
cons
nil
cons
cons
1117
def
121
ref
subst
1117
remove
93
ref
subst
1101
remove
258
ref
subst
eqMp
nil
1102
remove
1100
ref
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
1103
ref
1100
remove
cons
nil
cons
cons
145
ref
subst
1118
def
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
eqMp
nil
132
ref
1073
ref
cons
133
ref
1079
ref
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
nil
33
ref
45
ref
1072
ref
appTerm
1078
ref
appTerm
nil
cons
cons
35
ref
45
ref
1078
remove
appTerm
1072
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
93
ref
subst
proveHyp
nil
33
ref
1079
ref
cons
35
ref
1073
ref
cons
nil
cons
cons
nil
cons
cons
1119
def
121
ref
subst
1119
remove
93
ref
subst
nil
132
ref
938
ref
cons
133
ref
1107
ref
cons
nil
cons
1120
def
cons
nil
cons
cons
1121
def
145
ref
subst
1121
remove
258
ref
subst
nil
1091
remove
nil
cons
nil
cons
cons
107
ref
subst
99
ref
nil
23
ref
1093
remove
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
1082
ref
35
ref
1095
ref
cons
nil
cons
cons
nil
cons
cons
1122
def
121
ref
subst
1122
remove
93
ref
subst
1083
remove
146
ref
subst
216
remove
152
ref
appTerm
1123
def
betaConv
nil
1106
remove
35
ref
1123
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
148
ref
1081
remove
181
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
eqMp
1124
def
nil
33
ref
275
remove
cons
1112
ref
cons
nil
cons
cons
93
ref
subst
proveHyp
1113
remove
146
ref
subst
1076
remove
152
ref
appTerm
1125
def
betaConv
nil
33
ref
1107
remove
cons
35
ref
1125
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
148
ref
1109
remove
181
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
eqMp
eqMp
eqMp
nil
1103
remove
133
ref
1095
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
proveHyp
proveHyp
eqMp
nil
132
ref
1079
remove
cons
133
ref
1073
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
224
ref
1067
remove
appTerm
thm
674
ref
97
ref
674
remove
1010
ref
192
ref
182
ref
189
ref
190
ref
nil
97
ref
99
ref
575
ref
1013
ref
appTerm
absTerm
1126
def
nil
cons
cons
nil
cons
nil
cons
cons
426
ref
subst
191
ref
99
ref
427
remove
1126
ref
152
ref
appTerm
betaConv
appThm
nil
377
ref
1099
remove
cons
361
remove
1082
remove
nil
cons
cons
cons
nil
cons
cons
377
remove
27
ref
116
remove
384
remove
appTerm
appTerm
45
ref
74
remove
appTerm
378
ref
appTerm
appTerm
absTerm
1127
def
378
ref
appTerm
1128
def
betaConv
35
ref
267
ref
1127
ref
appTerm
1129
def
absTerm
1130
def
64
remove
appTerm
1131
def
betaConv
33
ref
267
ref
1130
ref
appTerm
1132
def
absTerm
1133
def
63
remove
appTerm
1134
def
betaConv
nil
267
remove
1133
ref
appTerm
1135
def
axiom
nil
33
ref
1135
remove
nil
cons
cons
35
ref
1134
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
1133
remove
nil
cons
cons
1021
remove
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
1132
remove
nil
cons
cons
35
ref
1131
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
ref
270
ref
1130
remove
nil
cons
cons
271
ref
90
remove
cons
nil
cons
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
nil
33
ref
1129
remove
nil
cons
cons
35
ref
1128
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
269
remove
270
remove
1127
remove
nil
cons
cons
271
remove
378
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
subst
trans
absThm
appThm
trans
appThm
426
ref
appThm
appThm
1069
ref
appThm
absThm
appThm
absThm
appThm
absThm
appThm
sym
nil
228
ref
97
ref
224
ref
1010
ref
43
ref
182
ref
45
ref
72
ref
39
ref
99
ref
45
ref
944
ref
appTerm
1013
ref
appTerm
absTerm
1136
def
appTerm
1137
def
appTerm
1138
def
217
remove
appTerm
1139
def
appTerm
1077
remove
appTerm
1140
def
absTerm
1141
def
appTerm
1142
def
absTerm
1143
def
appTerm
1144
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
831
ref
subst
97
ref
nil
23
ref
1144
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
228
ref
1143
remove
nil
cons
cons
nil
cons
nil
cons
cons
831
ref
subst
1010
ref
nil
23
ref
1142
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
108
ref
1141
remove
nil
cons
cons
nil
cons
nil
cons
cons
112
ref
subst
182
ref
nil
23
ref
1140
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
33
ref
1139
remove
nil
cons
1145
def
cons
1108
remove
cons
nil
cons
cons
1146
def
121
ref
subst
1146
remove
93
ref
subst
nil
132
ref
1137
remove
nil
cons
1147
def
cons
1148
def
133
ref
938
remove
cons
nil
cons
cons
nil
cons
cons
1149
def
145
ref
subst
1149
remove
258
ref
subst
1110
remove
99
ref
1111
remove
1114
remove
1115
ref
1089
ref
1124
remove
eqMp
nil
33
ref
944
remove
nil
cons
1150
def
cons
1151
def
1112
remove
cons
nil
cons
cons
146
ref
subst
1152
def
proveHyp
1136
ref
152
ref
appTerm
1153
def
betaConv
nil
33
ref
1147
remove
cons
35
ref
1153
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
148
ref
94
ref
1136
remove
nil
cons
cons
181
ref
cons
nil
cons
cons
158
ref
subst
eqMp
eqMp
1154
def
eqMp
eqMp
1118
remove
deductAntisym
eqMp
eqMp
absThm
eqMp
proveHyp
proveHyp
eqMp
nil
132
ref
1145
remove
cons
1120
remove
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
1155
def
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
224
ref
97
ref
224
ref
1010
ref
43
ref
182
ref
45
ref
72
ref
206
ref
1126
remove
appTerm
183
ref
appTerm
appTerm
208
ref
appTerm
appTerm
1061
ref
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
thm
nil
228
ref
97
ref
224
ref
1010
ref
43
ref
182
ref
45
ref
72
ref
39
ref
99
ref
45
ref
961
remove
appTerm
1013
ref
appTerm
absTerm
appTerm
appTerm
1156
def
208
remove
appTerm
appTerm
1061
ref
appTerm
1157
def
absTerm
1158
def
appTerm
1159
def
absTerm
1160
def
appTerm
1161
def
absTerm
1162
def
nil
cons
cons
nil
cons
nil
cons
cons
831
ref
subst
97
ref
nil
23
ref
1161
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
228
ref
1160
remove
nil
cons
cons
nil
cons
nil
cons
cons
831
ref
subst
1010
ref
nil
23
ref
1159
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
108
ref
1158
remove
nil
cons
cons
nil
cons
nil
cons
cons
112
ref
subst
182
ref
nil
23
ref
1157
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
189
ref
190
ref
191
ref
99
ref
189
ref
939
remove
appThm
1116
remove
appThm
absThm
appThm
appThm
1163
def
426
remove
appThm
appThm
1069
remove
appThm
sym
1155
remove
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
224
ref
1162
remove
appTerm
thm
nil
228
ref
97
ref
224
ref
1010
ref
43
ref
182
ref
45
ref
1156
remove
835
remove
appTerm
appTerm
824
remove
1012
ref
appTerm
183
ref
appTerm
appTerm
1164
def
absTerm
1165
def
appTerm
1166
def
absTerm
1167
def
appTerm
1168
def
absTerm
1169
def
nil
cons
cons
nil
cons
nil
cons
cons
831
ref
subst
97
ref
nil
23
ref
1168
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
228
ref
1167
remove
nil
cons
cons
nil
cons
nil
cons
cons
831
ref
subst
1010
ref
nil
23
ref
1166
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
108
ref
1165
remove
nil
cons
cons
nil
cons
nil
cons
cons
112
ref
subst
182
ref
nil
23
ref
1164
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
189
ref
1163
remove
959
ref
appThm
appThm
1068
ref
959
remove
subst
appThm
sym
nil
33
ref
1138
remove
946
ref
appTerm
nil
cons
1170
def
cons
35
ref
572
remove
99
ref
943
remove
1013
ref
appTerm
absTerm
1171
def
appTerm
1172
def
nil
cons
1173
def
cons
nil
cons
1174
def
cons
nil
cons
cons
1175
def
121
ref
subst
1175
remove
93
ref
subst
nil
1148
remove
133
ref
960
ref
cons
nil
cons
cons
nil
cons
cons
1176
def
145
ref
subst
1176
remove
258
ref
subst
nil
33
ref
960
remove
cons
1174
ref
cons
nil
cons
cons
146
ref
subst
nil
94
ref
99
ref
45
ref
945
ref
152
ref
appTerm
1177
def
appTerm
1172
ref
appTerm
1178
def
absTerm
1179
def
nil
cons
cons
nil
cons
nil
cons
cons
107
ref
subst
99
ref
nil
23
ref
1178
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
33
ref
1177
ref
nil
cons
1180
def
cons
1174
ref
cons
nil
cons
cons
1181
def
121
ref
subst
1181
remove
93
ref
subst
1177
ref
betaConv
1177
remove
assume
eqMp
nil
1151
remove
1174
remove
cons
nil
cons
cons
1182
def
146
ref
subst
proveHyp
1182
ref
121
ref
subst
1182
remove
93
ref
subst
1105
remove
1104
remove
258
ref
subst
1171
ref
152
ref
appTerm
betaConv
sym
1115
remove
1089
remove
214
remove
assume
eqMp
1152
remove
proveHyp
1154
remove
eqMp
eqMp
eqMp
148
ref
94
ref
1171
remove
nil
cons
cons
181
ref
cons
nil
cons
cons
589
remove
subst
proveHyp
proveHyp
proveHyp
eqMp
nil
132
ref
1150
remove
cons
133
ref
1173
remove
cons
nil
cons
1183
def
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
132
ref
1180
remove
cons
1183
ref
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
33
ref
39
ref
1179
remove
appTerm
nil
cons
cons
35
ref
45
ref
946
remove
appTerm
1172
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
148
ref
94
ref
945
remove
nil
cons
cons
1183
ref
cons
nil
cons
cons
654
remove
subst
eqMp
eqMp
proveHyp
proveHyp
eqMp
nil
132
ref
1170
remove
cons
1183
remove
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
224
ref
1169
remove
appTerm
thm
nil
228
ref
97
ref
224
ref
1010
ref
224
ref
"r"
37
remove
var
1184
def
43
ref
182
ref
45
ref
1059
remove
39
ref
99
ref
575
remove
27
ref
1013
remove
appTerm
1184
ref
varTerm
1185
def
152
ref
appTerm
appTerm
appTerm
1186
def
absTerm
1187
def
appTerm
1188
def
appTerm
appTerm
27
ref
1061
remove
appTerm
206
remove
1185
ref
appTerm
1189
def
183
ref
appTerm
appTerm
appTerm
absTerm
1190
def
appTerm
1191
def
absTerm
1192
def
appTerm
1193
def
absTerm
1194
def
appTerm
1195
def
absTerm
1196
def
nil
cons
cons
nil
cons
nil
cons
cons
831
ref
subst
97
ref
nil
23
ref
1195
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
228
ref
1194
remove
nil
cons
cons
nil
cons
nil
cons
cons
831
ref
subst
1010
remove
nil
23
ref
1193
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
228
remove
1192
remove
nil
cons
cons
nil
cons
nil
cons
cons
831
remove
subst
1184
remove
nil
23
ref
1191
remove
nil
cons
1197
def
cons
nil
cons
nil
cons
cons
32
ref
subst
189
ref
190
ref
232
ref
appThm
1188
ref
refl
1198
def
appThm
nil
23
ref
1188
ref
nil
cons
1199
def
cons
nil
cons
nil
cons
cons
1200
def
1088
ref
subst
trans
appThm
60
ref
1068
ref
232
ref
subst
appThm
nil
97
remove
1185
ref
nil
cons
cons
nil
cons
nil
cons
cons
1201
def
232
remove
subst
appThm
291
remove
trans
appThm
1200
remove
434
remove
subst
trans
sym
31
ref
eqMp
nil
33
ref
45
ref
72
ref
221
remove
appTerm
1188
ref
appTerm
appTerm
27
ref
1060
ref
18
ref
appTerm
appTerm
1189
ref
18
ref
appTerm
appTerm
appTerm
1202
def
nil
cons
cons
35
ref
39
remove
40
ref
43
remove
44
ref
45
ref
45
ref
72
ref
294
ref
appTerm
1188
ref
appTerm
1203
def
appTerm
27
ref
1060
ref
46
ref
appTerm
1204
def
appTerm
1189
ref
46
ref
appTerm
1205
def
appTerm
1206
def
appTerm
1207
def
appTerm
45
remove
72
ref
300
remove
appTerm
1188
ref
appTerm
appTerm
27
ref
1060
remove
52
ref
appTerm
appTerm
1189
remove
52
ref
appTerm
appTerm
appTerm
1208
def
appTerm
1209
def
absTerm
1210
def
appTerm
1211
def
absTerm
1212
def
appTerm
1213
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
93
ref
subst
proveHyp
nil
94
ref
1212
remove
nil
cons
cons
nil
cons
nil
cons
cons
107
remove
subst
40
ref
nil
23
ref
1211
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
108
remove
1210
remove
nil
cons
cons
nil
cons
nil
cons
cons
112
remove
subst
44
ref
nil
23
ref
1209
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
ref
subst
nil
33
ref
1207
ref
nil
cons
1214
def
cons
35
ref
1208
remove
nil
cons
1215
def
cons
nil
cons
cons
nil
cons
cons
1216
def
121
ref
subst
1216
remove
93
ref
subst
189
ref
190
ref
324
ref
appThm
1198
remove
appThm
appThm
60
remove
1068
remove
324
ref
subst
appThm
1201
remove
324
remove
subst
appThm
appThm
sym
nil
33
ref
72
ref
314
ref
appTerm
1188
remove
appTerm
nil
cons
1217
def
cons
35
ref
27
ref
72
ref
1012
remove
51
ref
appTerm
1218
def
appTerm
1204
remove
appTerm
appTerm
72
ref
1185
remove
51
remove
appTerm
1219
def
appTerm
1205
remove
appTerm
appTerm
nil
cons
1220
def
cons
nil
cons
cons
nil
cons
cons
1221
def
121
remove
subst
1221
remove
93
remove
subst
nil
132
ref
314
remove
nil
cons
cons
133
ref
1199
ref
cons
nil
cons
cons
nil
cons
cons
1222
def
145
ref
subst
1222
remove
258
ref
subst
nil
356
remove
133
ref
294
ref
nil
cons
1223
def
cons
nil
cons
cons
nil
cons
cons
1224
def
145
ref
subst
1224
remove
258
remove
subst
190
ref
nil
418
remove
35
ref
27
remove
1218
remove
appTerm
1219
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
415
remove
1187
ref
152
remove
appTerm
1225
def
betaConv
nil
33
ref
1199
remove
cons
35
ref
1225
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
148
remove
94
remove
1187
remove
nil
cons
cons
181
remove
cons
nil
cons
cons
158
remove
subst
eqMp
eqMp
1226
def
subst
eqMp
appThm
190
ref
nil
23
ref
1223
remove
cons
nil
cons
nil
cons
cons
32
ref
subst
294
remove
assume
eqMp
appThm
191
ref
99
remove
nil
23
remove
1186
remove
nil
cons
cons
nil
cons
nil
cons
cons
32
remove
subst
1226
remove
eqMp
absThm
appThm
287
remove
trans
appThm
282
remove
1088
remove
subst
trans
sym
31
remove
eqMp
nil
33
ref
1203
remove
nil
cons
cons
35
ref
1206
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
146
ref
subst
proveHyp
1207
remove
assume
eqMp
appThm
proveHyp
proveHyp
proveHyp
proveHyp
eqMp
nil
132
ref
1217
remove
cons
133
ref
1220
remove
cons
nil
cons
cons
nil
cons
cons
145
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
132
remove
1214
remove
cons
133
remove
1215
remove
cons
nil
cons
cons
nil
cons
cons
145
remove
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
33
remove
72
remove
1202
remove
appTerm
1213
remove
appTerm
nil
cons
cons
35
remove
1197
remove
cons
nil
cons
cons
nil
cons
cons
146
remove
subst
proveHyp
189
ref
190
remove
1190
ref
18
remove
appTerm
betaConv
appThm
191
remove
40
remove
192
ref
44
remove
189
remove
1190
ref
46
remove
appTerm
betaConv
appThm
1190
ref
52
remove
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
192
remove
182
remove
1190
ref
183
remove
appTerm
betaConv
absThm
appThm
appThm
nil
195
remove
1190
remove
nil
cons
cons
nil
cons
nil
cons
cons
202
remove
subst
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
224
remove
1196
remove
appTerm
thm