6
version
"Data.List.toSet"
"set_of_list"
"->"
typeOp
0
def
"Data.List.list"
typeOp
"A"
varType
1
def
nil
cons
2
def
opType
3
def
"Set.set"
typeOp
2
ref
opType
4
def
nil
cons
5
def
cons
opType
6
def
var
7
def
nil
cons
cons
nil
cons
7
ref
"Data.Bool./\\"
const
0
ref
"bool"
typeOp
nil
opType
8
def
0
ref
8
ref
8
ref
nil
cons
9
def
cons
opType
10
def
nil
cons
cons
opType
11
def
constTerm
12
def
"="
const
13
def
0
ref
4
ref
0
ref
4
ref
9
ref
cons
opType
14
def
nil
cons
15
def
cons
opType
constTerm
16
def
7
remove
varTerm
17
def
"Data.List.[]"
const
3
ref
constTerm
18
def
appTerm
appTerm
"Set.{}"
const
4
ref
constTerm
19
def
appTerm
appTerm
"Data.Bool.!"
const
20
def
0
ref
0
ref
1
ref
9
ref
cons
opType
21
def
9
ref
cons
opType
22
def
constTerm
23
def
"h"
1
ref
var
24
def
20
ref
0
ref
0
ref
3
ref
9
ref
cons
opType
25
def
9
ref
cons
opType
26
def
constTerm
27
def
"t"
3
ref
var
28
def
16
ref
17
ref
"Data.List.::"
const
0
ref
1
ref
0
ref
3
ref
3
ref
nil
cons
29
def
cons
opType
nil
cons
cons
opType
constTerm
30
def
24
ref
varTerm
31
def
appTerm
28
ref
varTerm
32
def
appTerm
33
def
appTerm
appTerm
"Set.insert"
const
0
ref
1
ref
0
ref
4
ref
5
ref
cons
opType
nil
cons
34
def
cons
opType
constTerm
35
def
31
ref
appTerm
36
def
17
ref
32
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
37
def
refl
38
def
13
ref
0
ref
6
ref
0
ref
6
ref
9
ref
cons
opType
39
def
nil
cons
cons
opType
constTerm
17
ref
appTerm
"select"
const
40
def
0
ref
39
ref
6
ref
nil
cons
41
def
cons
opType
constTerm
42
def
37
ref
appTerm
appTerm
assume
sym
appThm
37
ref
17
remove
appTerm
betaConv
trans
"A"
41
remove
cons
nil
cons
nil
nil
cons
43
def
cons
nil
13
ref
0
ref
22
ref
0
ref
22
ref
9
ref
cons
opType
44
def
nil
cons
cons
opType
constTerm
45
def
"Data.Bool.?"
const
46
def
22
ref
constTerm
47
def
appTerm
48
def
"p"
21
ref
var
49
def
49
ref
varTerm
50
def
40
ref
0
ref
21
ref
2
ref
cons
opType
constTerm
50
ref
appTerm
appTerm
51
def
absTerm
52
def
appTerm
axiom
53
def
subst
38
remove
appThm
"p"
39
ref
var
54
def
54
remove
varTerm
55
def
42
remove
55
remove
appTerm
appTerm
absTerm
37
remove
appTerm
betaConv
trans
46
ref
0
ref
39
remove
9
ref
cons
opType
constTerm
refl
"fn"
6
ref
var
56
def
12
ref
16
ref
56
remove
varTerm
57
def
18
ref
appTerm
appTerm
19
ref
appTerm
appTerm
refl
23
ref
refl
58
def
24
ref
27
ref
refl
59
def
28
ref
16
ref
57
ref
33
ref
appTerm
appTerm
refl
24
ref
28
ref
"_15999"
4
ref
var
60
def
36
ref
60
remove
varTerm
appTerm
absTerm
61
def
absTerm
62
def
absTerm
63
def
31
ref
appTerm
betaConv
32
ref
refl
64
def
appThm
62
remove
32
ref
appTerm
betaConv
trans
57
remove
32
ref
appTerm
65
def
refl
appThm
61
remove
65
remove
appTerm
betaConv
trans
appThm
absThm
appThm
absThm
appThm
appThm
absThm
appThm
nil
"f"
0
ref
1
ref
0
ref
3
ref
34
remove
cons
opType
nil
cons
cons
opType
var
63
remove
nil
cons
cons
"b"
4
ref
var
19
ref
nil
cons
66
def
cons
nil
cons
cons
nil
cons
cons
"A"
2
ref
cons
67
def
"B"
5
ref
cons
nil
cons
cons
43
ref
cons
"f"
0
ref
1
ref
0
ref
3
ref
0
ref
"B"
varType
68
def
68
ref
nil
cons
69
def
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
70
def
var
71
def
46
ref
0
ref
0
ref
0
ref
3
ref
69
ref
cons
opType
72
def
9
ref
cons
opType
9
ref
cons
opType
constTerm
"fn"
72
remove
var
73
def
12
ref
13
ref
0
ref
68
ref
0
ref
68
ref
9
ref
cons
opType
74
def
nil
cons
cons
opType
constTerm
75
def
73
remove
varTerm
76
def
18
ref
appTerm
appTerm
"b"
68
ref
var
77
def
varTerm
78
def
appTerm
appTerm
23
ref
24
ref
27
ref
28
ref
75
remove
76
ref
33
ref
appTerm
appTerm
71
remove
varTerm
79
def
31
ref
appTerm
32
ref
appTerm
76
remove
32
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
80
def
79
ref
appTerm
81
def
betaConv
77
remove
20
ref
0
ref
0
ref
70
ref
9
ref
cons
opType
82
def
9
ref
cons
opType
constTerm
80
ref
appTerm
83
def
absTerm
84
def
78
ref
appTerm
85
def
betaConv
nil
20
ref
0
ref
74
ref
9
ref
cons
opType
constTerm
84
ref
appTerm
86
def
axiom
nil
"p"
8
ref
var
87
def
86
remove
nil
cons
cons
"q"
8
ref
var
88
def
85
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
13
ref
11
ref
constTerm
89
def
"Data.Bool.==>"
const
11
ref
constTerm
90
def
87
ref
varTerm
91
def
appTerm
92
def
88
ref
varTerm
93
def
appTerm
94
def
appTerm
refl
87
ref
88
ref
89
ref
12
ref
91
ref
appTerm
95
def
93
ref
appTerm
96
def
appTerm
97
def
91
ref
appTerm
absTerm
98
def
absTerm
99
def
91
ref
appTerm
betaConv
93
ref
refl
100
def
appThm
98
remove
93
ref
appTerm
betaConv
trans
appThm
nil
13
ref
0
ref
11
ref
0
ref
11
ref
9
ref
cons
opType
101
def
nil
cons
cons
opType
constTerm
102
def
90
ref
appTerm
99
remove
appTerm
axiom
91
ref
refl
103
def
appThm
100
ref
appThm
eqMp
104
def
sym
105
def
97
remove
refl
88
ref
13
ref
0
ref
101
ref
0
ref
101
remove
9
ref
cons
opType
nil
cons
cons
opType
constTerm
106
def
"f"
11
ref
var
107
def
107
ref
varTerm
108
def
91
ref
appTerm
93
ref
appTerm
absTerm
109
def
appTerm
107
ref
108
ref
"Data.Bool.T"
const
8
ref
constTerm
110
def
appTerm
110
ref
appTerm
absTerm
111
def
appTerm
absTerm
112
def
93
ref
appTerm
betaConv
appThm
13
ref
0
ref
10
ref
0
ref
10
ref
9
ref
cons
opType
113
def
nil
cons
cons
opType
constTerm
114
def
95
remove
appTerm
refl
87
ref
112
remove
absTerm
115
def
91
ref
appTerm
betaConv
appThm
nil
102
remove
12
ref
appTerm
115
ref
appTerm
axiom
116
def
103
remove
appThm
eqMp
100
ref
appThm
eqMp
117
def
sym
107
ref
108
ref
refl
nil
"t"
8
ref
var
118
def
91
ref
nil
cons
119
def
cons
nil
cons
nil
cons
cons
89
ref
118
ref
varTerm
120
def
appTerm
121
def
110
ref
appTerm
122
def
assume
sym
nil
110
ref
axiom
123
def
eqMp
120
ref
assume
123
ref
deductAntisym
deductAntisym
124
def
subst
91
ref
assume
125
def
eqMp
appThm
nil
118
ref
93
ref
nil
cons
126
def
cons
nil
cons
nil
cons
cons
124
ref
subst
93
ref
assume
127
def
eqMp
appThm
absThm
eqMp
128
def
nil
"P"
8
ref
var
129
def
119
ref
cons
"Q"
8
ref
var
130
def
126
ref
cons
nil
cons
131
def
cons
nil
cons
cons
89
ref
refl
132
def
107
ref
108
remove
129
ref
varTerm
133
def
appTerm
134
def
130
ref
varTerm
135
def
appTerm
absTerm
136
def
87
ref
88
ref
91
ref
absTerm
absTerm
137
def
appTerm
betaConv
137
ref
133
ref
appTerm
betaConv
135
ref
refl
138
def
appThm
88
ref
133
ref
absTerm
135
ref
appTerm
betaConv
trans
trans
appThm
111
ref
137
ref
appTerm
betaConv
137
ref
110
ref
appTerm
betaConv
110
ref
refl
139
def
appThm
88
ref
110
ref
absTerm
110
ref
appTerm
betaConv
trans
trans
appThm
89
ref
12
ref
133
ref
appTerm
140
def
135
ref
appTerm
141
def
appTerm
refl
88
ref
106
remove
107
remove
134
remove
93
ref
appTerm
absTerm
appTerm
111
ref
appTerm
absTerm
135
ref
appTerm
betaConv
appThm
114
ref
140
remove
appTerm
refl
115
remove
133
ref
appTerm
betaConv
appThm
116
remove
133
ref
refl
142
def
appThm
eqMp
138
ref
appThm
eqMp
141
remove
assume
eqMp
143
def
137
remove
refl
appThm
eqMp
sym
123
ref
eqMp
144
def
subst
145
def
deductAntisym
eqMp
104
remove
94
ref
assume
eqMp
sym
125
ref
eqMp
132
ref
109
remove
87
ref
88
ref
93
ref
absTerm
146
def
absTerm
147
def
appTerm
betaConv
147
ref
91
ref
appTerm
betaConv
100
remove
appThm
146
ref
93
ref
appTerm
betaConv
trans
trans
appThm
111
remove
147
ref
appTerm
betaConv
147
ref
110
ref
appTerm
betaConv
139
ref
appThm
146
ref
110
ref
appTerm
betaConv
trans
trans
148
def
appThm
117
remove
96
remove
assume
eqMp
147
ref
refl
149
def
appThm
eqMp
sym
123
ref
eqMp
150
def
proveHyp
deductAntisym
151
def
subst
proveHyp
"A"
69
remove
cons
nil
cons
"P"
74
remove
var
84
remove
nil
cons
cons
"x"
68
remove
var
78
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
87
ref
23
ref
"P"
21
ref
var
152
def
varTerm
153
def
appTerm
154
def
nil
cons
155
def
cons
88
ref
153
ref
"x"
1
ref
var
156
def
varTerm
157
def
appTerm
158
def
nil
cons
159
def
cons
nil
cons
cons
nil
cons
cons
160
def
105
ref
subst
160
remove
150
remove
128
remove
deductAntisym
161
def
subst
89
ref
158
ref
appTerm
refl
156
ref
110
ref
absTerm
162
def
157
ref
appTerm
betaConv
appThm
49
ref
13
ref
0
ref
21
ref
22
ref
nil
cons
163
def
cons
opType
constTerm
164
def
50
ref
appTerm
162
remove
appTerm
absTerm
165
def
153
ref
appTerm
betaConv
166
def
nil
45
ref
23
ref
appTerm
165
remove
appTerm
axiom
153
ref
refl
167
def
appThm
168
def
154
ref
assume
eqMp
eqMp
157
ref
refl
169
def
appThm
eqMp
sym
123
ref
eqMp
eqMp
nil
129
ref
155
remove
cons
130
ref
159
ref
cons
nil
cons
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
170
def
subst
eqMp
eqMp
nil
87
ref
83
remove
nil
cons
cons
88
ref
81
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
"A"
70
ref
nil
cons
cons
nil
cons
"P"
82
remove
var
80
remove
nil
cons
cons
"x"
70
remove
var
79
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
171
def
subst
subst
eqMp
eqMp
eqMp
defineConstList
172
def
pop
173
def
pop
172
ref
nil
129
ref
16
ref
173
remove
hdTl
pop
6
remove
constTerm
174
def
18
ref
appTerm
appTerm
19
ref
appTerm
175
def
nil
cons
cons
130
ref
23
ref
24
ref
27
ref
28
ref
16
ref
174
ref
33
ref
appTerm
appTerm
36
remove
174
ref
32
ref
appTerm
appTerm
appTerm
absTerm
176
def
appTerm
177
def
absTerm
178
def
appTerm
179
def
nil
cons
180
def
cons
nil
cons
cons
nil
cons
cons
181
def
132
ref
136
remove
147
ref
appTerm
betaConv
147
remove
133
ref
appTerm
betaConv
138
remove
appThm
146
remove
135
ref
appTerm
betaConv
trans
trans
appThm
148
remove
appThm
143
remove
149
remove
appThm
eqMp
sym
123
ref
eqMp
182
def
subst
proveHyp
183
def
nil
179
remove
thm
172
remove
181
remove
144
ref
subst
proveHyp
184
def
nil
175
remove
thm
12
ref
refl
185
def
20
ref
44
remove
constTerm
186
def
refl
187
def
49
ref
nil
118
ref
"Data.List.all"
"ALL"
0
ref
21
ref
25
ref
nil
cons
188
def
cons
opType
189
def
var
190
def
nil
cons
cons
nil
cons
190
ref
12
ref
186
ref
49
ref
89
ref
190
ref
varTerm
191
def
50
ref
appTerm
192
def
18
ref
appTerm
appTerm
110
ref
appTerm
absTerm
appTerm
appTerm
186
ref
49
ref
23
ref
24
ref
27
ref
28
ref
89
ref
192
ref
33
ref
appTerm
appTerm
12
ref
50
ref
31
ref
appTerm
193
def
appTerm
194
def
192
remove
32
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
195
def
refl
196
def
13
ref
0
ref
189
ref
0
ref
189
ref
9
ref
cons
opType
197
def
nil
cons
cons
opType
constTerm
198
def
191
ref
appTerm
199
def
40
ref
0
ref
197
ref
189
ref
nil
cons
200
def
cons
opType
constTerm
201
def
195
ref
appTerm
appTerm
assume
sym
appThm
195
ref
191
ref
appTerm
betaConv
202
def
trans
"A"
200
remove
cons
nil
cons
203
def
43
ref
cons
53
ref
subst
204
def
196
remove
appThm
"p"
197
ref
var
205
def
205
remove
varTerm
206
def
201
ref
206
remove
appTerm
appTerm
absTerm
207
def
195
ref
appTerm
betaConv
trans
46
ref
0
ref
0
ref
0
ref
3
ref
163
ref
cons
opType
208
def
9
ref
cons
opType
209
def
9
ref
cons
opType
210
def
constTerm
211
def
refl
212
def
"fn"
208
ref
var
213
def
12
ref
45
ref
213
ref
varTerm
214
def
18
ref
appTerm
appTerm
215
def
49
ref
110
ref
absTerm
216
def
appTerm
appTerm
refl
58
ref
24
ref
59
ref
28
ref
45
ref
214
ref
33
ref
appTerm
appTerm
refl
217
def
24
ref
28
ref
"_16010"
22
ref
var
218
def
49
ref
194
ref
218
remove
varTerm
50
ref
appTerm
appTerm
absTerm
absTerm
219
def
absTerm
220
def
absTerm
221
def
31
ref
appTerm
betaConv
64
ref
appThm
220
remove
32
ref
appTerm
betaConv
trans
214
remove
32
ref
appTerm
222
def
refl
223
def
appThm
219
remove
222
ref
appTerm
betaConv
trans
appThm
absThm
appThm
absThm
appThm
appThm
absThm
appThm
nil
"f"
0
ref
1
ref
0
ref
3
ref
0
ref
22
ref
163
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
var
224
def
221
remove
nil
cons
cons
"b"
22
ref
var
225
def
216
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
67
ref
"B"
163
remove
cons
nil
cons
cons
43
ref
cons
171
ref
subst
226
def
subst
eqMp
nil
87
ref
211
ref
"_16009"
208
ref
var
227
def
12
ref
45
ref
227
ref
varTerm
228
def
18
ref
appTerm
229
def
appTerm
216
ref
appTerm
230
def
appTerm
23
ref
24
ref
27
ref
28
ref
45
ref
228
ref
33
ref
appTerm
231
def
appTerm
49
ref
194
ref
228
ref
32
ref
appTerm
50
ref
appTerm
appTerm
232
def
absTerm
233
def
appTerm
absTerm
234
def
appTerm
235
def
absTerm
236
def
appTerm
237
def
appTerm
238
def
absTerm
239
def
appTerm
240
def
nil
cons
cons
88
ref
211
ref
227
ref
12
ref
186
ref
49
ref
89
ref
229
remove
50
ref
appTerm
appTerm
241
def
110
ref
appTerm
242
def
absTerm
243
def
appTerm
244
def
appTerm
186
ref
49
ref
23
ref
24
ref
27
ref
28
ref
89
ref
231
remove
50
ref
appTerm
appTerm
245
def
232
remove
appTerm
246
def
absTerm
247
def
appTerm
248
def
absTerm
249
def
appTerm
250
def
absTerm
251
def
appTerm
252
def
appTerm
253
def
absTerm
254
def
appTerm
255
def
nil
cons
256
def
cons
nil
cons
257
def
cons
nil
cons
cons
151
ref
subst
nil
"P"
209
remove
var
258
def
227
ref
90
ref
239
ref
228
ref
appTerm
259
def
appTerm
255
ref
appTerm
260
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
208
ref
nil
cons
cons
nil
cons
261
def
43
ref
cons
89
ref
154
remove
appTerm
refl
166
remove
appThm
168
remove
eqMp
sym
262
def
subst
263
def
subst
227
ref
nil
118
ref
260
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
nil
87
ref
259
ref
nil
cons
264
def
cons
257
ref
cons
nil
cons
cons
265
def
105
ref
subst
265
remove
161
ref
subst
259
ref
betaConv
259
remove
assume
eqMp
nil
87
ref
238
remove
nil
cons
266
def
cons
257
remove
cons
nil
cons
cons
267
def
151
ref
subst
proveHyp
267
ref
105
ref
subst
267
remove
161
ref
subst
254
ref
228
ref
appTerm
268
def
betaConv
269
def
sym
nil
129
ref
230
ref
nil
cons
cons
130
ref
237
remove
nil
cons
270
def
cons
nil
cons
cons
nil
cons
cons
271
def
144
ref
subst
nil
"P"
22
ref
var
272
def
243
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
21
ref
nil
cons
273
def
cons
nil
cons
43
ref
cons
262
ref
subst
274
def
subst
49
ref
nil
118
ref
242
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
241
remove
refl
216
remove
50
ref
appTerm
betaConv
appThm
230
remove
assume
50
ref
refl
275
def
appThm
eqMp
eqMp
absThm
eqMp
proveHyp
nil
87
ref
244
remove
nil
cons
cons
88
ref
252
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
161
ref
subst
proveHyp
271
remove
182
ref
subst
nil
272
ref
251
remove
nil
cons
cons
nil
cons
nil
cons
cons
274
ref
subst
49
ref
nil
118
ref
250
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
nil
152
ref
249
remove
nil
cons
cons
nil
cons
nil
cons
cons
262
ref
subst
24
ref
nil
118
ref
248
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
nil
"P"
25
ref
var
276
def
247
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
29
ref
cons
nil
cons
277
def
43
ref
cons
262
ref
subst
278
def
subst
28
ref
nil
118
ref
246
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
245
remove
refl
233
remove
50
ref
appTerm
betaConv
appThm
234
ref
32
ref
appTerm
279
def
betaConv
236
ref
31
ref
appTerm
280
def
betaConv
nil
87
ref
270
remove
cons
88
ref
280
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
67
ref
nil
cons
281
def
152
ref
236
remove
nil
cons
cons
156
ref
31
ref
nil
cons
cons
nil
cons
282
def
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
nil
87
ref
235
remove
nil
cons
cons
88
ref
279
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
277
ref
276
ref
234
remove
nil
cons
cons
"x"
3
ref
var
283
def
32
ref
nil
cons
cons
nil
cons
284
def
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
275
ref
appThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
proveHyp
eqMp
eqMp
261
ref
258
ref
254
ref
nil
cons
cons
285
def
"x"
208
ref
var
286
def
228
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
89
ref
47
remove
153
ref
appTerm
287
def
appTerm
288
def
refl
49
ref
20
ref
113
remove
constTerm
289
def
88
ref
90
ref
23
ref
156
ref
90
ref
50
ref
157
ref
appTerm
appTerm
93
ref
appTerm
absTerm
appTerm
appTerm
93
ref
appTerm
absTerm
appTerm
absTerm
290
def
153
remove
appTerm
betaConv
appThm
nil
48
remove
290
remove
appTerm
axiom
167
remove
appThm
eqMp
291
def
sym
nil
"P"
10
ref
var
292
def
130
ref
90
ref
23
ref
156
ref
90
ref
158
remove
appTerm
293
def
135
ref
appTerm
absTerm
294
def
appTerm
295
def
appTerm
135
ref
appTerm
296
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
9
ref
cons
nil
cons
297
def
43
ref
cons
298
def
262
ref
subst
subst
130
ref
nil
118
ref
296
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
nil
87
ref
295
remove
nil
cons
299
def
cons
300
def
88
ref
135
ref
nil
cons
301
def
cons
nil
cons
302
def
cons
nil
cons
cons
303
def
105
ref
subst
303
ref
161
ref
subst
nil
87
ref
159
remove
cons
302
ref
cons
nil
cons
cons
151
ref
subst
294
ref
157
ref
appTerm
304
def
betaConv
nil
300
ref
88
ref
304
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
281
ref
152
ref
294
remove
nil
cons
cons
156
ref
157
ref
nil
cons
305
def
cons
nil
cons
306
def
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
129
ref
299
remove
cons
307
def
130
ref
301
ref
cons
nil
cons
308
def
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
309
def
subst
proveHyp
eqMp
nil
129
ref
266
remove
cons
130
ref
256
ref
cons
nil
cons
310
def
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
129
ref
264
remove
cons
310
ref
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
87
ref
20
ref
210
remove
constTerm
311
def
286
ref
90
ref
239
ref
286
ref
varTerm
312
def
appTerm
appTerm
255
ref
appTerm
absTerm
appTerm
nil
cons
cons
88
ref
90
ref
240
remove
appTerm
255
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
261
ref
258
ref
239
remove
nil
cons
cons
310
remove
cons
nil
cons
cons
nil
300
remove
88
ref
90
ref
287
ref
appTerm
313
def
135
ref
appTerm
nil
cons
314
def
cons
nil
cons
cons
nil
cons
cons
315
def
105
ref
subst
315
remove
161
ref
subst
nil
87
ref
287
remove
nil
cons
316
def
cons
317
def
302
remove
cons
nil
cons
cons
318
def
105
ref
subst
318
remove
161
ref
subst
303
remove
151
ref
subst
88
ref
90
ref
23
ref
156
ref
293
remove
93
ref
appTerm
absTerm
appTerm
appTerm
93
ref
appTerm
absTerm
319
def
135
remove
appTerm
320
def
betaConv
nil
317
remove
88
ref
289
ref
319
ref
appTerm
321
def
nil
cons
322
def
cons
nil
cons
cons
nil
cons
cons
323
def
151
ref
subst
291
remove
nil
87
ref
288
remove
321
ref
appTerm
nil
cons
cons
88
ref
313
remove
321
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
323
remove
nil
87
ref
89
ref
91
ref
appTerm
93
ref
appTerm
324
def
nil
cons
325
def
cons
88
ref
94
remove
nil
cons
326
def
cons
nil
cons
cons
nil
cons
cons
327
def
105
ref
subst
327
remove
161
ref
subst
105
ref
161
ref
324
remove
assume
328
def
125
remove
eqMp
eqMp
145
remove
deductAntisym
eqMp
329
def
eqMp
nil
129
ref
325
remove
cons
130
ref
326
ref
cons
nil
cons
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
87
ref
322
remove
cons
88
ref
320
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
297
ref
292
ref
319
remove
nil
cons
cons
"x"
8
ref
var
330
def
301
remove
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
129
ref
316
remove
cons
308
remove
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
nil
307
remove
130
ref
314
remove
cons
nil
cons
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
331
def
subst
eqMp
eqMp
proveHyp
nil
87
ref
256
remove
cons
88
ref
46
ref
0
ref
197
ref
9
ref
cons
opType
constTerm
332
def
195
ref
appTerm
333
def
nil
cons
334
def
cons
nil
cons
335
def
cons
nil
cons
cons
151
ref
subst
nil
258
ref
227
ref
90
ref
268
ref
appTerm
333
ref
appTerm
336
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
263
ref
subst
227
remove
nil
118
ref
336
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
nil
87
ref
268
ref
nil
cons
337
def
cons
335
ref
cons
nil
cons
cons
338
def
105
ref
subst
338
remove
161
ref
subst
269
remove
268
remove
assume
eqMp
nil
87
ref
253
ref
nil
cons
339
def
cons
335
ref
cons
nil
cons
cons
340
def
151
ref
subst
proveHyp
340
ref
105
ref
subst
340
remove
161
ref
subst
"_16007"
21
ref
var
341
def
"_16008"
3
ref
var
342
def
228
remove
342
ref
varTerm
appTerm
343
def
341
remove
varTerm
appTerm
absTerm
absTerm
344
def
refl
nil
87
ref
198
ref
344
ref
appTerm
344
ref
appTerm
nil
cons
cons
335
ref
cons
nil
cons
cons
151
ref
subst
proveHyp
nil
190
remove
344
ref
nil
cons
cons
nil
cons
nil
cons
cons
nil
87
ref
199
remove
344
ref
appTerm
345
def
nil
cons
346
def
cons
335
remove
cons
nil
cons
cons
347
def
105
ref
subst
347
remove
161
ref
subst
202
remove
sym
185
ref
187
ref
49
ref
132
ref
345
remove
assume
275
ref
appThm
344
remove
50
ref
appTerm
betaConv
trans
348
def
18
ref
refl
349
def
appThm
342
remove
343
remove
50
ref
appTerm
absTerm
350
def
18
ref
appTerm
betaConv
trans
appThm
139
remove
appThm
absThm
appThm
appThm
187
ref
49
ref
58
ref
24
ref
59
ref
28
ref
132
ref
348
ref
33
ref
refl
351
def
appThm
350
ref
33
ref
appTerm
betaConv
trans
appThm
194
ref
refl
348
remove
64
ref
appThm
350
remove
32
ref
appTerm
betaConv
trans
appThm
appThm
absThm
appThm
absThm
appThm
absThm
appThm
appThm
sym
253
remove
assume
eqMp
eqMp
203
ref
"P"
197
remove
var
352
def
195
remove
nil
cons
cons
"x"
189
ref
var
353
def
191
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
309
ref
subst
proveHyp
eqMp
nil
129
ref
346
remove
cons
130
ref
334
remove
cons
nil
cons
354
def
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
129
ref
339
remove
cons
354
ref
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
129
ref
337
remove
cons
354
ref
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
87
ref
311
ref
286
ref
90
ref
254
remove
312
ref
appTerm
appTerm
333
ref
appTerm
absTerm
appTerm
nil
cons
cons
88
ref
90
ref
255
remove
appTerm
333
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
261
ref
285
remove
354
remove
cons
nil
cons
cons
331
ref
subst
eqMp
eqMp
proveHyp
eqMp
eqMp
defineConstList
355
def
pop
hdTl
pop
189
ref
constTerm
50
ref
appTerm
356
def
18
ref
appTerm
357
def
nil
cons
cons
nil
cons
nil
cons
cons
118
ref
89
ref
122
remove
appTerm
120
ref
appTerm
absTerm
358
def
120
ref
appTerm
359
def
betaConv
nil
289
ref
358
ref
appTerm
360
def
axiom
nil
87
ref
360
remove
nil
cons
cons
88
ref
359
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
297
ref
292
ref
358
remove
nil
cons
cons
330
ref
120
ref
nil
cons
cons
nil
cons
361
def
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
subst
absThm
appThm
appThm
186
ref
49
ref
23
ref
24
ref
27
ref
28
ref
89
ref
356
ref
33
ref
appTerm
appTerm
194
remove
356
remove
32
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
362
def
refl
appThm
355
remove
eqMp
363
def
nil
129
ref
186
ref
49
ref
357
remove
absTerm
appTerm
364
def
nil
cons
cons
130
ref
362
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
365
def
144
ref
subst
proveHyp
nil
364
remove
thm
363
remove
365
remove
182
ref
subst
proveHyp
nil
362
remove
thm
185
ref
187
ref
49
ref
nil
118
ref
"Data.List.any"
"EX"
189
ref
var
366
def
nil
cons
cons
nil
cons
366
ref
12
ref
186
ref
49
ref
89
ref
366
ref
varTerm
367
def
50
ref
appTerm
368
def
18
ref
appTerm
appTerm
"Data.Bool.F"
const
8
ref
constTerm
369
def
appTerm
absTerm
appTerm
appTerm
186
ref
49
ref
23
ref
24
ref
27
ref
28
ref
89
ref
368
ref
33
ref
appTerm
appTerm
"Data.Bool.\\/"
const
11
remove
constTerm
370
def
193
remove
appTerm
371
def
368
remove
32
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
372
def
refl
373
def
198
ref
367
ref
appTerm
374
def
201
remove
372
ref
appTerm
appTerm
assume
sym
appThm
372
ref
367
ref
appTerm
betaConv
375
def
trans
204
remove
373
remove
appThm
207
remove
372
ref
appTerm
betaConv
trans
212
remove
213
remove
12
ref
215
remove
49
ref
369
ref
absTerm
376
def
appTerm
appTerm
refl
58
ref
24
ref
59
ref
28
ref
217
remove
24
ref
28
ref
"_16016"
22
remove
var
377
def
49
ref
371
ref
377
remove
varTerm
50
ref
appTerm
appTerm
absTerm
absTerm
378
def
absTerm
379
def
absTerm
380
def
31
ref
appTerm
betaConv
64
ref
appThm
379
remove
32
ref
appTerm
betaConv
trans
223
remove
appThm
378
remove
222
remove
appTerm
betaConv
trans
appThm
absThm
appThm
absThm
appThm
appThm
absThm
appThm
nil
224
remove
380
remove
nil
cons
cons
225
remove
376
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
226
remove
subst
eqMp
nil
87
ref
211
ref
"_16015"
208
remove
var
381
def
12
ref
45
ref
381
ref
varTerm
382
def
18
ref
appTerm
383
def
appTerm
376
ref
appTerm
384
def
appTerm
23
ref
24
ref
27
ref
28
ref
45
remove
382
ref
33
ref
appTerm
385
def
appTerm
49
ref
371
ref
382
ref
32
ref
appTerm
50
ref
appTerm
appTerm
386
def
absTerm
387
def
appTerm
absTerm
388
def
appTerm
389
def
absTerm
390
def
appTerm
391
def
appTerm
392
def
absTerm
393
def
appTerm
394
def
nil
cons
cons
88
ref
211
remove
381
ref
12
ref
186
ref
49
ref
89
ref
383
remove
50
ref
appTerm
appTerm
395
def
369
ref
appTerm
396
def
absTerm
397
def
appTerm
398
def
appTerm
186
ref
49
ref
23
ref
24
ref
27
ref
28
ref
89
ref
385
remove
50
ref
appTerm
appTerm
399
def
386
remove
appTerm
400
def
absTerm
401
def
appTerm
402
def
absTerm
403
def
appTerm
404
def
absTerm
405
def
appTerm
406
def
appTerm
407
def
absTerm
408
def
appTerm
409
def
nil
cons
410
def
cons
nil
cons
411
def
cons
nil
cons
cons
151
ref
subst
nil
258
ref
381
ref
90
ref
393
ref
382
ref
appTerm
412
def
appTerm
409
ref
appTerm
413
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
263
ref
subst
381
ref
nil
118
ref
413
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
nil
87
ref
412
ref
nil
cons
414
def
cons
411
ref
cons
nil
cons
cons
415
def
105
ref
subst
415
remove
161
ref
subst
412
ref
betaConv
412
remove
assume
eqMp
nil
87
ref
392
remove
nil
cons
416
def
cons
411
remove
cons
nil
cons
cons
417
def
151
ref
subst
proveHyp
417
ref
105
ref
subst
417
remove
161
ref
subst
408
ref
382
ref
appTerm
418
def
betaConv
419
def
sym
nil
129
ref
384
ref
nil
cons
cons
130
ref
391
remove
nil
cons
420
def
cons
nil
cons
cons
nil
cons
cons
421
def
144
ref
subst
nil
272
ref
397
remove
nil
cons
cons
nil
cons
nil
cons
cons
274
ref
subst
49
ref
nil
118
ref
396
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
395
remove
refl
376
remove
50
ref
appTerm
betaConv
appThm
384
remove
assume
275
ref
appThm
eqMp
eqMp
absThm
eqMp
proveHyp
nil
87
ref
398
remove
nil
cons
cons
88
ref
406
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
161
ref
subst
proveHyp
421
remove
182
ref
subst
nil
272
remove
405
remove
nil
cons
cons
nil
cons
nil
cons
cons
274
remove
subst
49
ref
nil
118
ref
404
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
nil
152
ref
403
remove
nil
cons
cons
nil
cons
nil
cons
cons
262
ref
subst
24
ref
nil
118
ref
402
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
nil
276
ref
401
remove
nil
cons
cons
nil
cons
nil
cons
cons
278
ref
subst
28
ref
nil
118
ref
400
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
399
remove
refl
387
remove
50
ref
appTerm
betaConv
appThm
388
ref
32
ref
appTerm
422
def
betaConv
390
ref
31
ref
appTerm
423
def
betaConv
nil
87
ref
420
remove
cons
88
ref
423
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
281
ref
152
ref
390
remove
nil
cons
cons
282
ref
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
nil
87
ref
389
remove
nil
cons
cons
88
ref
422
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
277
ref
276
ref
388
remove
nil
cons
cons
284
ref
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
275
ref
appThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
proveHyp
eqMp
eqMp
261
ref
258
ref
408
ref
nil
cons
cons
424
def
286
ref
382
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
309
ref
subst
proveHyp
eqMp
nil
129
ref
416
remove
cons
130
ref
410
ref
cons
nil
cons
425
def
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
129
ref
414
remove
cons
425
ref
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
87
ref
311
ref
286
ref
90
ref
393
ref
312
ref
appTerm
appTerm
409
ref
appTerm
absTerm
appTerm
nil
cons
cons
88
ref
90
ref
394
remove
appTerm
409
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
261
ref
258
ref
393
remove
nil
cons
cons
425
remove
cons
nil
cons
cons
331
ref
subst
eqMp
eqMp
proveHyp
nil
87
ref
410
remove
cons
88
ref
332
remove
372
ref
appTerm
426
def
nil
cons
427
def
cons
nil
cons
428
def
cons
nil
cons
cons
151
ref
subst
nil
258
remove
381
ref
90
ref
418
ref
appTerm
426
ref
appTerm
429
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
263
remove
subst
381
remove
nil
118
ref
429
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
nil
87
ref
418
ref
nil
cons
430
def
cons
428
ref
cons
nil
cons
cons
431
def
105
ref
subst
431
remove
161
ref
subst
419
remove
418
remove
assume
eqMp
nil
87
ref
407
ref
nil
cons
432
def
cons
428
ref
cons
nil
cons
cons
433
def
151
ref
subst
proveHyp
433
ref
105
ref
subst
433
remove
161
ref
subst
"_16013"
21
ref
var
434
def
"_16014"
3
ref
var
435
def
382
remove
435
ref
varTerm
appTerm
436
def
434
remove
varTerm
appTerm
absTerm
absTerm
437
def
refl
nil
87
ref
198
remove
437
ref
appTerm
437
ref
appTerm
nil
cons
cons
428
ref
cons
nil
cons
cons
151
ref
subst
proveHyp
nil
366
remove
437
ref
nil
cons
cons
nil
cons
nil
cons
cons
nil
87
ref
374
remove
437
ref
appTerm
438
def
nil
cons
439
def
cons
428
remove
cons
nil
cons
cons
440
def
105
ref
subst
440
remove
161
ref
subst
375
remove
sym
185
ref
187
ref
49
ref
132
ref
438
remove
assume
275
ref
appThm
437
remove
50
ref
appTerm
betaConv
trans
441
def
349
ref
appThm
435
remove
436
remove
50
ref
appTerm
absTerm
442
def
18
ref
appTerm
betaConv
trans
appThm
369
ref
refl
443
def
appThm
absThm
appThm
appThm
187
remove
49
ref
58
ref
24
ref
59
ref
28
ref
132
ref
441
ref
351
ref
appThm
442
ref
33
ref
appTerm
betaConv
trans
appThm
371
ref
refl
441
remove
64
ref
appThm
442
remove
32
ref
appTerm
betaConv
trans
appThm
appThm
absThm
appThm
absThm
appThm
absThm
appThm
appThm
sym
407
remove
assume
eqMp
eqMp
203
remove
352
remove
372
remove
nil
cons
cons
353
remove
367
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
309
ref
subst
proveHyp
eqMp
nil
129
ref
439
remove
cons
130
ref
427
remove
cons
nil
cons
444
def
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
129
ref
432
remove
cons
444
ref
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
129
ref
430
remove
cons
444
ref
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
87
ref
311
remove
286
remove
90
ref
408
remove
312
remove
appTerm
appTerm
426
ref
appTerm
absTerm
appTerm
nil
cons
cons
88
ref
90
ref
409
remove
appTerm
426
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
261
remove
424
remove
444
remove
cons
nil
cons
cons
331
ref
subst
eqMp
eqMp
proveHyp
eqMp
eqMp
defineConstList
445
def
pop
hdTl
pop
189
remove
constTerm
50
ref
appTerm
446
def
18
ref
appTerm
447
def
nil
cons
cons
nil
cons
nil
cons
cons
118
ref
89
ref
121
remove
369
ref
appTerm
appTerm
"Data.Bool.~"
const
10
remove
constTerm
448
def
120
ref
appTerm
appTerm
absTerm
449
def
120
ref
appTerm
450
def
betaConv
nil
289
ref
449
ref
appTerm
451
def
axiom
nil
87
ref
451
remove
nil
cons
cons
88
ref
450
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
297
ref
292
ref
449
remove
nil
cons
cons
361
ref
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
452
def
subst
absThm
appThm
appThm
186
ref
49
ref
23
ref
24
ref
27
ref
28
ref
89
ref
446
ref
33
ref
appTerm
appTerm
371
remove
446
remove
32
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
453
def
refl
appThm
445
remove
eqMp
454
def
nil
129
ref
186
remove
49
remove
448
ref
447
remove
appTerm
absTerm
appTerm
455
def
nil
cons
cons
130
ref
453
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
456
def
144
ref
subst
proveHyp
nil
455
remove
thm
454
remove
456
remove
182
ref
subst
proveHyp
nil
453
remove
thm
185
ref
58
ref
156
ref
nil
118
ref
"Data.List.member"
"MEM"
0
ref
1
ref
188
remove
cons
opType
457
def
var
458
def
nil
cons
cons
nil
cons
458
ref
12
ref
23
ref
156
ref
89
ref
458
ref
varTerm
459
def
157
ref
appTerm
460
def
18
ref
appTerm
appTerm
369
ref
appTerm
absTerm
appTerm
appTerm
23
ref
156
ref
23
ref
24
ref
27
ref
28
ref
89
ref
460
ref
33
ref
appTerm
appTerm
370
remove
13
ref
0
ref
1
ref
273
ref
cons
opType
constTerm
461
def
157
ref
appTerm
462
def
31
ref
appTerm
appTerm
463
def
460
remove
32
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
464
def
refl
465
def
13
ref
0
ref
457
ref
0
ref
457
ref
9
ref
cons
opType
466
def
nil
cons
cons
opType
constTerm
467
def
459
ref
appTerm
468
def
40
ref
0
ref
466
ref
457
ref
nil
cons
469
def
cons
opType
constTerm
470
def
464
ref
appTerm
appTerm
assume
sym
appThm
464
ref
459
ref
appTerm
betaConv
471
def
trans
"A"
469
remove
cons
nil
cons
472
def
43
ref
cons
53
ref
subst
465
remove
appThm
"p"
466
ref
var
473
def
473
remove
varTerm
474
def
470
remove
474
remove
appTerm
appTerm
absTerm
464
ref
appTerm
betaConv
trans
46
ref
0
ref
0
ref
0
ref
3
ref
273
ref
cons
opType
475
def
9
ref
cons
opType
476
def
9
ref
cons
opType
477
def
constTerm
478
def
refl
"fn"
475
ref
var
479
def
12
ref
164
ref
479
remove
varTerm
480
def
18
ref
appTerm
appTerm
156
ref
369
ref
absTerm
481
def
appTerm
appTerm
refl
58
ref
24
ref
59
ref
28
ref
164
ref
480
ref
33
ref
appTerm
appTerm
refl
24
ref
28
ref
"_16022"
21
ref
var
482
def
156
ref
463
ref
482
remove
varTerm
157
ref
appTerm
appTerm
absTerm
absTerm
483
def
absTerm
484
def
absTerm
485
def
31
ref
appTerm
betaConv
64
ref
appThm
484
remove
32
ref
appTerm
betaConv
trans
480
remove
32
ref
appTerm
486
def
refl
appThm
483
remove
486
remove
appTerm
betaConv
trans
appThm
absThm
appThm
absThm
appThm
appThm
absThm
appThm
nil
"f"
0
ref
1
ref
0
ref
3
ref
0
ref
21
ref
273
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
var
485
remove
nil
cons
cons
"b"
21
remove
var
481
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
67
remove
"B"
273
remove
cons
nil
cons
cons
43
ref
cons
171
remove
subst
subst
eqMp
nil
87
ref
478
ref
"_16021"
475
ref
var
487
def
12
ref
164
ref
487
ref
varTerm
488
def
18
ref
appTerm
489
def
appTerm
481
ref
appTerm
490
def
appTerm
23
ref
24
ref
27
ref
28
ref
164
remove
488
ref
33
ref
appTerm
491
def
appTerm
156
ref
463
ref
488
ref
32
ref
appTerm
157
ref
appTerm
appTerm
492
def
absTerm
493
def
appTerm
absTerm
494
def
appTerm
495
def
absTerm
496
def
appTerm
497
def
appTerm
498
def
absTerm
499
def
appTerm
500
def
nil
cons
cons
88
ref
478
remove
487
ref
12
ref
23
ref
156
ref
89
ref
489
remove
157
ref
appTerm
appTerm
501
def
369
ref
appTerm
502
def
absTerm
503
def
appTerm
504
def
appTerm
23
ref
156
ref
23
ref
24
ref
27
ref
28
ref
89
ref
491
remove
157
ref
appTerm
appTerm
505
def
492
remove
appTerm
506
def
absTerm
507
def
appTerm
508
def
absTerm
509
def
appTerm
510
def
absTerm
511
def
appTerm
512
def
appTerm
513
def
absTerm
514
def
appTerm
515
def
nil
cons
516
def
cons
nil
cons
517
def
cons
nil
cons
cons
151
ref
subst
nil
"P"
476
remove
var
518
def
487
ref
90
ref
499
ref
488
ref
appTerm
519
def
appTerm
515
ref
appTerm
520
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
475
ref
nil
cons
cons
nil
cons
521
def
43
ref
cons
262
ref
subst
522
def
subst
487
ref
nil
118
ref
520
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
nil
87
ref
519
ref
nil
cons
523
def
cons
517
ref
cons
nil
cons
cons
524
def
105
ref
subst
524
remove
161
ref
subst
519
ref
betaConv
519
remove
assume
eqMp
nil
87
ref
498
remove
nil
cons
525
def
cons
517
remove
cons
nil
cons
cons
526
def
151
ref
subst
proveHyp
526
ref
105
ref
subst
526
remove
161
ref
subst
514
ref
488
ref
appTerm
527
def
betaConv
528
def
sym
nil
129
ref
490
ref
nil
cons
cons
130
ref
497
remove
nil
cons
529
def
cons
nil
cons
cons
nil
cons
cons
530
def
144
ref
subst
nil
152
ref
503
remove
nil
cons
cons
nil
cons
nil
cons
cons
262
ref
subst
156
ref
nil
118
ref
502
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
501
remove
refl
481
remove
157
ref
appTerm
betaConv
appThm
490
remove
assume
169
ref
appThm
eqMp
eqMp
absThm
eqMp
proveHyp
nil
87
ref
504
remove
nil
cons
cons
88
ref
512
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
161
ref
subst
proveHyp
530
remove
182
ref
subst
nil
152
ref
511
remove
nil
cons
cons
nil
cons
nil
cons
cons
262
ref
subst
156
ref
nil
118
ref
510
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
nil
152
ref
509
remove
nil
cons
cons
nil
cons
nil
cons
cons
262
ref
subst
24
ref
nil
118
ref
508
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
nil
276
ref
507
remove
nil
cons
cons
nil
cons
nil
cons
cons
278
ref
subst
28
ref
nil
118
ref
506
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
505
remove
refl
493
remove
157
ref
appTerm
betaConv
appThm
494
ref
32
ref
appTerm
531
def
betaConv
496
ref
31
ref
appTerm
532
def
betaConv
nil
87
ref
529
remove
cons
88
ref
532
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
281
ref
152
ref
496
remove
nil
cons
cons
282
ref
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
nil
87
ref
495
remove
nil
cons
cons
88
ref
531
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
277
ref
276
ref
494
remove
nil
cons
cons
284
ref
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
169
ref
appThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
proveHyp
eqMp
eqMp
521
ref
518
ref
514
ref
nil
cons
cons
533
def
"x"
475
remove
var
534
def
488
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
309
ref
subst
proveHyp
eqMp
nil
129
ref
525
remove
cons
130
ref
516
ref
cons
nil
cons
535
def
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
129
ref
523
remove
cons
535
ref
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
87
ref
20
ref
477
remove
constTerm
536
def
534
ref
90
ref
499
ref
534
ref
varTerm
537
def
appTerm
appTerm
515
ref
appTerm
absTerm
appTerm
nil
cons
cons
88
ref
90
ref
500
remove
appTerm
515
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
521
ref
518
ref
499
remove
nil
cons
cons
535
remove
cons
nil
cons
cons
331
ref
subst
eqMp
eqMp
proveHyp
nil
87
ref
516
remove
cons
88
ref
46
ref
0
ref
466
ref
9
ref
cons
opType
constTerm
464
ref
appTerm
538
def
nil
cons
539
def
cons
nil
cons
540
def
cons
nil
cons
cons
151
ref
subst
nil
518
remove
487
ref
90
ref
527
ref
appTerm
538
ref
appTerm
541
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
522
remove
subst
487
remove
nil
118
ref
541
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
nil
87
ref
527
ref
nil
cons
542
def
cons
540
ref
cons
nil
cons
cons
543
def
105
ref
subst
543
remove
161
ref
subst
528
remove
527
remove
assume
eqMp
nil
87
ref
513
ref
nil
cons
544
def
cons
540
ref
cons
nil
cons
cons
545
def
151
ref
subst
proveHyp
545
ref
105
ref
subst
545
remove
161
ref
subst
"_16019"
1
ref
var
546
def
"_16020"
3
ref
var
547
def
488
remove
547
ref
varTerm
appTerm
548
def
546
remove
varTerm
appTerm
absTerm
absTerm
549
def
refl
nil
87
ref
467
remove
549
ref
appTerm
549
ref
appTerm
nil
cons
cons
540
ref
cons
nil
cons
cons
151
ref
subst
proveHyp
nil
458
remove
549
ref
nil
cons
cons
nil
cons
nil
cons
cons
nil
87
ref
468
remove
549
ref
appTerm
550
def
nil
cons
551
def
cons
540
remove
cons
nil
cons
cons
552
def
105
ref
subst
552
remove
161
ref
subst
471
remove
sym
185
ref
58
ref
156
ref
132
ref
550
remove
assume
169
ref
appThm
549
remove
157
ref
appTerm
betaConv
trans
553
def
349
remove
appThm
547
remove
548
remove
157
ref
appTerm
absTerm
554
def
18
ref
appTerm
betaConv
trans
appThm
443
remove
appThm
absThm
appThm
appThm
58
ref
156
ref
58
ref
24
ref
59
remove
28
ref
132
ref
553
ref
351
remove
appThm
554
ref
33
ref
appTerm
betaConv
trans
appThm
463
ref
refl
553
remove
64
remove
appThm
554
remove
32
ref
appTerm
betaConv
trans
appThm
appThm
absThm
appThm
absThm
appThm
absThm
appThm
appThm
sym
513
remove
assume
eqMp
eqMp
472
remove
"P"
466
remove
var
464
remove
nil
cons
cons
"x"
457
ref
var
459
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
309
ref
subst
proveHyp
eqMp
nil
129
ref
551
remove
cons
130
ref
539
remove
cons
nil
cons
555
def
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
129
ref
544
remove
cons
555
ref
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
129
ref
542
remove
cons
555
ref
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
87
ref
536
remove
534
remove
90
ref
514
remove
537
remove
appTerm
appTerm
538
ref
appTerm
absTerm
appTerm
nil
cons
cons
88
ref
90
ref
515
remove
appTerm
538
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
521
remove
533
remove
555
remove
cons
nil
cons
cons
331
ref
subst
eqMp
eqMp
proveHyp
eqMp
eqMp
defineConstList
556
def
pop
hdTl
pop
457
remove
constTerm
157
ref
appTerm
557
def
18
ref
appTerm
558
def
nil
cons
cons
nil
cons
nil
cons
cons
452
remove
subst
absThm
appThm
appThm
23
ref
156
ref
23
ref
24
ref
27
ref
28
ref
89
ref
557
ref
33
ref
appTerm
appTerm
463
remove
557
remove
32
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
559
def
refl
appThm
556
remove
eqMp
560
def
nil
129
ref
23
ref
156
ref
448
ref
558
remove
appTerm
absTerm
appTerm
561
def
nil
cons
cons
130
ref
559
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
562
def
144
ref
subst
proveHyp
nil
561
remove
thm
560
remove
562
remove
182
ref
subst
proveHyp
nil
559
remove
thm
20
ref
0
ref
14
ref
9
ref
cons
opType
563
def
constTerm
564
def
refl
565
def
"s"
4
ref
var
566
def
90
ref
"Set.finite"
const
14
ref
constTerm
566
ref
varTerm
567
def
appTerm
568
def
appTerm
569
def
refl
570
def
185
ref
16
ref
refl
571
def
174
ref
refl
nil
"_16002"
4
ref
var
572
def
567
ref
nil
cons
573
def
cons
nil
cons
nil
cons
cons
"Data.List.fromSet"
572
ref
40
remove
0
ref
25
ref
29
ref
cons
opType
constTerm
574
def
"l"
3
ref
var
575
def
12
ref
16
ref
174
ref
575
ref
varTerm
576
def
appTerm
appTerm
577
def
572
remove
varTerm
578
def
appTerm
appTerm
13
remove
0
ref
"Number.Natural.natural"
typeOp
nil
opType
579
def
0
ref
579
ref
9
ref
cons
opType
nil
cons
cons
opType
constTerm
580
def
"Data.List.length"
const
0
ref
3
remove
579
ref
nil
cons
581
def
cons
opType
constTerm
582
def
576
ref
appTerm
appTerm
583
def
"Set.size"
const
0
ref
4
ref
581
ref
cons
opType
constTerm
584
def
578
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
585
def
defineConst
586
def
pop
587
def
pop
586
remove
578
ref
refl
appThm
585
remove
578
remove
appTerm
betaConv
trans
subst
588
def
appThm
appThm
567
ref
refl
appThm
appThm
580
ref
refl
589
def
582
ref
refl
588
remove
appThm
appThm
584
ref
567
ref
appTerm
590
def
refl
591
def
appThm
appThm
appThm
absThm
appThm
sym
565
ref
566
ref
570
ref
132
remove
575
ref
12
ref
577
ref
567
ref
appTerm
592
def
appTerm
583
ref
590
ref
appTerm
593
def
appTerm
594
def
absTerm
595
def
574
remove
595
ref
appTerm
appTerm
betaConv
appThm
46
remove
26
remove
constTerm
596
def
595
ref
appTerm
597
def
refl
appThm
277
ref
"p"
25
remove
var
595
ref
nil
cons
598
def
cons
nil
cons
nil
cons
cons
89
ref
51
ref
appTerm
refl
53
remove
275
remove
appThm
52
remove
50
remove
appTerm
betaConv
trans
appThm
nil
330
ref
51
remove
nil
cons
cons
nil
cons
nil
cons
cons
298
remove
nil
118
ref
462
remove
157
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
169
remove
eqMp
599
def
subst
subst
trans
sym
123
ref
eqMp
subst
eqMp
appThm
absThm
appThm
sym
575
ref
12
ref
577
ref
19
ref
appTerm
appTerm
583
ref
584
ref
19
ref
appTerm
600
def
appTerm
appTerm
absTerm
601
def
18
ref
appTerm
betaConv
sym
185
ref
571
ref
184
remove
appThm
19
ref
refl
appThm
nil
"x"
4
ref
var
602
def
66
remove
cons
nil
cons
nil
cons
cons
"A"
5
remove
cons
nil
cons
603
def
43
ref
cons
604
def
599
ref
subst
605
def
subst
trans
appThm
589
ref
nil
580
ref
582
ref
18
ref
appTerm
appTerm
"Number.Natural.zero"
const
579
ref
constTerm
606
def
appTerm
axiom
appThm
nil
580
ref
600
remove
appTerm
606
ref
appTerm
axiom
appThm
nil
"x"
579
ref
var
606
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
581
ref
cons
nil
cons
43
remove
cons
607
def
599
remove
subst
subst
trans
appThm
nil
118
ref
110
ref
nil
cons
cons
nil
cons
nil
cons
cons
118
ref
89
ref
12
ref
110
ref
appTerm
120
ref
appTerm
appTerm
120
ref
appTerm
absTerm
608
def
120
ref
appTerm
609
def
betaConv
nil
289
ref
608
ref
appTerm
610
def
axiom
nil
87
ref
610
remove
nil
cons
cons
88
ref
609
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
297
ref
292
ref
608
remove
nil
cons
cons
361
ref
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
611
def
subst
trans
sym
123
remove
eqMp
eqMp
277
ref
276
ref
601
ref
nil
cons
cons
283
ref
18
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
309
ref
subst
proveHyp
nil
87
ref
596
ref
601
remove
appTerm
612
def
nil
cons
cons
88
ref
23
ref
156
ref
564
ref
566
ref
90
ref
12
ref
597
ref
appTerm
12
ref
448
ref
"Set.member"
const
0
ref
1
ref
15
ref
cons
opType
constTerm
157
ref
appTerm
567
ref
appTerm
613
def
appTerm
614
def
appTerm
568
ref
appTerm
615
def
appTerm
616
def
appTerm
596
remove
575
ref
12
ref
577
remove
35
remove
157
ref
appTerm
617
def
567
ref
appTerm
618
def
appTerm
appTerm
583
remove
584
remove
618
ref
appTerm
619
def
appTerm
appTerm
absTerm
620
def
appTerm
621
def
appTerm
622
def
absTerm
623
def
appTerm
624
def
absTerm
625
def
appTerm
626
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
161
ref
subst
proveHyp
nil
152
ref
625
remove
nil
cons
cons
nil
cons
nil
cons
cons
262
ref
subst
156
ref
nil
118
ref
624
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
nil
"P"
14
ref
var
627
def
623
remove
nil
cons
cons
nil
cons
nil
cons
cons
604
remove
262
remove
subst
subst
566
ref
nil
118
ref
622
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
nil
87
ref
616
remove
nil
cons
628
def
cons
88
ref
621
ref
nil
cons
629
def
cons
nil
cons
630
def
cons
nil
cons
cons
631
def
105
ref
subst
631
remove
161
ref
subst
nil
129
ref
597
ref
nil
cons
632
def
cons
130
ref
615
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
633
def
144
ref
subst
633
remove
182
ref
subst
nil
87
ref
632
remove
cons
630
ref
cons
nil
cons
cons
151
ref
subst
nil
276
ref
575
ref
90
ref
595
ref
576
ref
appTerm
634
def
appTerm
621
ref
appTerm
635
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
278
remove
subst
575
remove
nil
118
ref
635
remove
nil
cons
cons
nil
cons
nil
cons
cons
124
ref
subst
nil
87
ref
634
ref
nil
cons
636
def
cons
630
ref
cons
nil
cons
cons
637
def
105
ref
subst
637
remove
161
ref
subst
634
ref
betaConv
634
remove
assume
eqMp
nil
87
ref
594
remove
nil
cons
638
def
cons
630
remove
cons
nil
cons
cons
639
def
151
ref
subst
proveHyp
639
ref
105
ref
subst
639
remove
161
ref
subst
nil
129
ref
592
ref
nil
cons
cons
130
ref
593
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
640
def
144
ref
subst
640
remove
182
ref
subst
nil
129
ref
614
remove
nil
cons
641
def
cons
130
ref
568
ref
nil
cons
642
def
cons
nil
cons
cons
nil
cons
cons
643
def
144
ref
subst
643
remove
182
ref
subst
620
ref
30
remove
157
ref
appTerm
576
ref
appTerm
644
def
appTerm
betaConv
sym
185
ref
571
remove
nil
28
ref
576
remove
nil
cons
cons
24
ref
305
remove
cons
nil
cons
cons
nil
cons
cons
645
def
176
ref
32
ref
appTerm
646
def
betaConv
178
ref
31
ref
appTerm
647
def
betaConv
183
remove
nil
87
ref
180
remove
cons
88
ref
647
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
281
ref
152
ref
178
remove
nil
cons
cons
282
ref
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
nil
87
ref
177
remove
nil
cons
cons
88
ref
646
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
277
ref
276
ref
176
remove
nil
cons
cons
284
ref
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
subst
617
remove
refl
592
remove
assume
appThm
trans
appThm
618
ref
refl
appThm
nil
602
ref
618
ref
nil
cons
cons
nil
cons
nil
cons
cons
605
remove
subst
trans
appThm
589
remove
645
remove
28
remove
580
ref
582
ref
33
remove
appTerm
appTerm
"Number.Natural.suc"
const
0
ref
579
ref
581
remove
cons
opType
648
def
constTerm
649
def
582
ref
32
ref
appTerm
appTerm
appTerm
absTerm
650
def
32
remove
appTerm
651
def
betaConv
24
remove
27
ref
650
ref
appTerm
652
def
absTerm
653
def
31
remove
appTerm
654
def
betaConv
nil
23
ref
653
ref
appTerm
655
def
axiom
nil
87
ref
655
remove
nil
cons
cons
88
ref
654
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
281
ref
152
ref
653
remove
nil
cons
cons
282
remove
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
nil
87
ref
652
remove
nil
cons
cons
88
ref
651
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
277
ref
276
ref
650
remove
nil
cons
cons
284
remove
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
subst
649
ref
refl
593
remove
assume
appThm
trans
appThm
619
ref
refl
appThm
appThm
nil
118
ref
580
ref
649
remove
590
ref
appTerm
656
def
appTerm
619
ref
appTerm
657
def
nil
cons
658
def
cons
nil
cons
nil
cons
cons
611
remove
subst
trans
sym
566
ref
569
ref
580
ref
619
remove
appTerm
659
def
"Data.Bool.cond"
const
660
def
0
ref
8
ref
0
ref
579
ref
648
remove
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
661
def
613
ref
appTerm
590
ref
appTerm
656
ref
appTerm
appTerm
appTerm
662
def
absTerm
663
def
567
ref
appTerm
664
def
betaConv
156
ref
564
ref
663
ref
appTerm
665
def
absTerm
666
def
157
remove
appTerm
667
def
betaConv
nil
23
ref
666
ref
appTerm
668
def
axiom
nil
87
ref
668
remove
nil
cons
cons
88
ref
667
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
281
ref
152
ref
666
remove
nil
cons
cons
306
remove
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
nil
87
ref
665
remove
nil
cons
cons
88
ref
664
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
603
remove
627
remove
663
remove
nil
cons
cons
602
remove
573
remove
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
nil
87
ref
662
remove
nil
cons
cons
88
ref
658
ref
cons
nil
cons
669
def
cons
nil
cons
cons
151
ref
subst
proveHyp
90
ref
refl
670
def
670
ref
nil
118
ref
642
remove
cons
nil
cons
nil
cons
cons
124
remove
subst
568
remove
assume
eqMp
appThm
659
ref
refl
661
remove
refl
nil
87
ref
641
remove
cons
88
ref
89
ref
613
ref
appTerm
369
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
nil
129
ref
613
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
87
ref
448
ref
133
ref
appTerm
671
def
nil
cons
672
def
cons
88
ref
89
ref
133
ref
appTerm
369
ref
appTerm
nil
cons
673
def
cons
nil
cons
cons
nil
cons
cons
674
def
105
ref
subst
674
remove
161
ref
subst
nil
87
ref
133
ref
nil
cons
675
def
cons
88
ref
369
ref
nil
cons
676
def
cons
nil
cons
cons
nil
cons
cons
329
remove
nil
87
ref
326
ref
cons
88
ref
90
ref
93
remove
appTerm
677
def
91
ref
appTerm
nil
cons
678
def
cons
nil
cons
cons
nil
cons
cons
161
ref
subst
proveHyp
677
remove
refl
328
remove
appThm
sym
nil
87
ref
126
ref
cons
679
def
88
ref
126
ref
cons
nil
cons
cons
nil
cons
cons
680
def
105
ref
subst
680
remove
161
ref
subst
127
remove
eqMp
nil
129
ref
126
remove
cons
131
remove
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
679
remove
88
ref
119
remove
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
nil
129
ref
326
remove
cons
130
ref
678
remove
cons
nil
cons
cons
nil
cons
cons
681
def
182
remove
subst
eqMp
151
ref
681
remove
144
ref
subst
eqMp
deductAntisym
deductAntisym
subst
89
ref
671
ref
appTerm
refl
87
ref
92
remove
369
ref
appTerm
absTerm
682
def
133
ref
appTerm
betaConv
appThm
nil
114
remove
448
remove
appTerm
682
remove
appTerm
axiom
142
remove
appThm
eqMp
671
remove
assume
eqMp
nil
87
ref
90
ref
133
ref
appTerm
369
ref
appTerm
nil
cons
cons
88
ref
90
ref
369
ref
appTerm
133
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
161
ref
subst
proveHyp
nil
87
ref
676
ref
cons
88
ref
675
ref
cons
nil
cons
cons
nil
cons
cons
683
def
105
ref
subst
683
remove
161
ref
subst
87
ref
91
remove
absTerm
684
def
133
remove
appTerm
685
def
betaConv
nil
89
ref
369
ref
appTerm
289
ref
684
ref
appTerm
686
def
appTerm
axiom
369
ref
assume
eqMp
nil
87
ref
686
remove
nil
cons
cons
88
ref
685
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
297
ref
292
ref
684
remove
nil
cons
cons
330
remove
675
ref
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
eqMp
nil
129
ref
676
remove
cons
130
ref
675
remove
cons
nil
cons
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
129
ref
672
remove
cons
130
ref
673
remove
cons
nil
cons
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
subst
eqMp
appThm
591
remove
appThm
656
ref
refl
appThm
nil
"t2"
579
ref
var
656
ref
nil
cons
cons
"t1"
579
remove
var
590
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
607
remove
"t2"
1
ref
var
687
def
461
remove
660
remove
0
ref
8
remove
0
ref
1
ref
0
ref
1
ref
2
remove
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
369
remove
appTerm
"t1"
1
remove
var
688
def
varTerm
689
def
appTerm
687
remove
varTerm
690
def
appTerm
appTerm
690
ref
appTerm
absTerm
691
def
690
ref
appTerm
692
def
betaConv
688
remove
23
ref
691
ref
appTerm
693
def
absTerm
694
def
689
ref
appTerm
695
def
betaConv
nil
23
ref
694
ref
appTerm
696
def
axiom
nil
87
ref
696
remove
nil
cons
cons
88
ref
695
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
281
ref
152
ref
694
remove
nil
cons
cons
156
ref
689
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
nil
87
ref
693
remove
nil
cons
cons
88
ref
692
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
281
remove
152
remove
691
remove
nil
cons
cons
156
ref
690
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
subst
subst
trans
appThm
appThm
nil
118
ref
659
remove
656
remove
appTerm
697
def
nil
cons
698
def
cons
nil
cons
nil
cons
cons
118
remove
89
remove
90
ref
110
remove
appTerm
120
ref
appTerm
appTerm
120
ref
appTerm
absTerm
699
def
120
remove
appTerm
700
def
betaConv
nil
289
remove
699
ref
appTerm
701
def
axiom
nil
87
ref
701
remove
nil
cons
cons
88
ref
700
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
297
remove
292
remove
699
remove
nil
cons
cons
361
remove
cons
nil
cons
cons
170
ref
subst
eqMp
eqMp
subst
trans
appThm
657
remove
refl
appThm
sym
nil
87
ref
698
ref
cons
669
remove
cons
nil
cons
cons
702
def
105
remove
subst
702
remove
161
remove
subst
697
remove
assume
sym
eqMp
nil
129
ref
698
remove
cons
130
ref
658
remove
cons
nil
cons
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
277
ref
276
ref
620
remove
nil
cons
cons
283
ref
644
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
309
remove
subst
proveHyp
proveHyp
proveHyp
proveHyp
proveHyp
eqMp
nil
129
ref
638
remove
cons
130
remove
629
remove
cons
nil
cons
703
def
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
129
ref
636
remove
cons
703
ref
cons
nil
cons
cons
144
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
87
ref
27
remove
283
ref
90
ref
595
remove
283
remove
varTerm
appTerm
appTerm
621
ref
appTerm
absTerm
appTerm
nil
cons
cons
88
ref
90
ref
597
ref
appTerm
621
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
277
remove
276
remove
598
remove
cons
703
ref
cons
nil
cons
cons
331
remove
subst
eqMp
eqMp
proveHyp
proveHyp
eqMp
nil
129
remove
628
remove
cons
703
remove
cons
nil
cons
cons
144
remove
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
87
ref
12
ref
612
remove
appTerm
626
remove
appTerm
nil
cons
cons
88
ref
564
ref
566
ref
569
ref
597
ref
appTerm
absTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
ref
subst
proveHyp
670
ref
185
ref
566
ref
597
remove
absTerm
704
def
19
ref
appTerm
betaConv
appThm
58
remove
156
ref
565
ref
566
ref
670
remove
185
remove
704
ref
567
ref
appTerm
betaConv
705
def
appThm
615
ref
refl
appThm
appThm
704
ref
618
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
565
remove
566
ref
570
remove
705
remove
appThm
absThm
appThm
appThm
nil
"p"
14
ref
var
706
def
704
remove
nil
cons
cons
nil
cons
nil
cons
cons
706
ref
90
ref
12
ref
706
remove
varTerm
707
def
19
remove
appTerm
appTerm
23
remove
156
remove
564
ref
566
ref
90
remove
12
ref
707
ref
567
ref
appTerm
708
def
appTerm
615
remove
appTerm
appTerm
707
ref
618
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
564
ref
566
ref
569
ref
708
remove
appTerm
absTerm
appTerm
appTerm
absTerm
709
def
707
ref
appTerm
710
def
betaConv
nil
20
remove
0
ref
563
ref
9
remove
cons
opType
constTerm
709
ref
appTerm
711
def
axiom
nil
87
remove
711
remove
nil
cons
cons
88
remove
710
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
151
remove
subst
proveHyp
"A"
15
remove
cons
nil
cons
"P"
563
remove
var
709
remove
nil
cons
cons
"x"
14
remove
var
707
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
remove
subst
eqMp
eqMp
subst
eqMp
eqMp
eqMp
eqMp
nil
564
remove
566
remove
569
remove
12
remove
16
remove
174
remove
587
remove
0
remove
4
remove
29
remove
cons
opType
constTerm
567
ref
appTerm
712
def
appTerm
appTerm
567
remove
appTerm
appTerm
580
remove
582
remove
712
remove
appTerm
appTerm
590
remove
appTerm
appTerm
appTerm
absTerm
appTerm
thm