6
version
nil
"P"
"->"
typeOp
0
def
"Set.set"
"Set.fromPredicate"
"HOLLight.dest_set"
"A"
nil
cons
"A"
0
ref
"A"
varType
1
def
"bool"
typeOp
nil
opType
2
def
nil
cons
3
def
cons
opType
4
def
nil
cons
5
def
cons
nil
cons
6
def
nil
nil
cons
7
def
cons
8
def
nil
"="
const
9
def
0
ref
0
ref
4
ref
3
ref
cons
opType
10
def
0
ref
10
ref
3
ref
cons
opType
11
def
nil
cons
cons
opType
constTerm
12
def
"Data.Bool.?"
const
13
def
10
ref
constTerm
14
def
appTerm
15
def
"p"
4
ref
var
16
def
16
ref
varTerm
17
def
"select"
const
18
def
0
ref
4
ref
1
ref
nil
cons
19
def
cons
opType
constTerm
20
def
17
ref
appTerm
appTerm
absTerm
21
def
appTerm
axiom
22
def
subst
16
ref
"x"
4
ref
var
23
def
"Data.Bool.T"
const
2
ref
constTerm
24
def
absTerm
25
def
17
ref
appTerm
26
def
absTerm
27
def
refl
appThm
"p"
10
ref
var
28
def
28
remove
varTerm
29
def
18
remove
0
ref
10
ref
5
ref
cons
opType
constTerm
29
remove
appTerm
appTerm
absTerm
27
ref
appTerm
betaConv
trans
27
ref
17
ref
appTerm
betaConv
sym
26
remove
betaConv
sym
nil
24
ref
axiom
30
def
eqMp
eqMp
6
ref
"P"
10
ref
var
31
def
27
ref
nil
cons
cons
23
ref
17
ref
nil
cons
32
def
cons
nil
cons
33
def
cons
nil
cons
cons
9
ref
0
ref
2
ref
0
ref
2
ref
3
ref
cons
opType
34
def
nil
cons
cons
opType
35
def
constTerm
36
def
14
ref
"P"
4
ref
var
37
def
varTerm
38
def
appTerm
appTerm
refl
16
ref
"Data.Bool.!"
const
39
def
0
ref
34
ref
3
ref
cons
opType
40
def
constTerm
41
def
"q"
2
ref
var
42
def
"Data.Bool.==>"
const
35
ref
constTerm
43
def
39
ref
10
ref
constTerm
44
def
"x"
1
ref
var
45
def
43
ref
17
ref
45
ref
varTerm
46
def
appTerm
47
def
appTerm
42
ref
varTerm
48
def
appTerm
absTerm
appTerm
appTerm
48
ref
appTerm
absTerm
appTerm
absTerm
49
def
38
ref
appTerm
betaConv
appThm
nil
15
remove
49
remove
appTerm
axiom
38
ref
refl
50
def
appThm
eqMp
sym
nil
"P"
34
ref
var
51
def
"Q"
2
ref
var
52
def
43
ref
44
ref
45
ref
43
ref
38
ref
46
ref
appTerm
53
def
appTerm
52
ref
varTerm
54
def
appTerm
absTerm
55
def
appTerm
56
def
appTerm
54
ref
appTerm
57
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
3
ref
cons
nil
cons
58
def
7
ref
cons
59
def
36
ref
44
ref
38
ref
appTerm
60
def
appTerm
refl
16
ref
9
ref
0
ref
4
ref
10
remove
nil
cons
cons
opType
constTerm
61
def
17
ref
appTerm
45
ref
24
ref
absTerm
62
def
appTerm
absTerm
63
def
38
remove
appTerm
betaConv
64
def
appThm
nil
12
remove
44
ref
appTerm
63
remove
appTerm
axiom
50
remove
appThm
65
def
eqMp
sym
66
def
subst
subst
52
ref
nil
"t"
2
ref
var
67
def
57
remove
nil
cons
cons
nil
cons
nil
cons
cons
36
ref
67
ref
varTerm
68
def
appTerm
69
def
24
ref
appTerm
assume
sym
30
ref
eqMp
68
ref
assume
30
ref
deductAntisym
deductAntisym
70
def
subst
nil
"p"
2
ref
var
71
def
56
remove
nil
cons
72
def
cons
73
def
42
ref
54
ref
nil
cons
74
def
cons
nil
cons
75
def
cons
nil
cons
cons
76
def
36
ref
43
ref
71
ref
varTerm
77
def
appTerm
48
ref
appTerm
78
def
appTerm
refl
71
ref
42
ref
36
ref
"Data.Bool./\\"
const
35
ref
constTerm
79
def
77
ref
appTerm
80
def
48
ref
appTerm
81
def
appTerm
82
def
77
ref
appTerm
absTerm
83
def
absTerm
84
def
77
ref
appTerm
betaConv
48
ref
refl
85
def
appThm
83
remove
48
ref
appTerm
betaConv
trans
appThm
nil
9
ref
0
ref
35
ref
0
ref
35
ref
3
ref
cons
opType
86
def
nil
cons
cons
opType
constTerm
87
def
43
ref
appTerm
84
remove
appTerm
axiom
77
ref
refl
88
def
appThm
85
ref
appThm
eqMp
89
def
sym
90
def
subst
76
remove
36
ref
refl
91
def
"f"
35
ref
var
92
def
92
ref
varTerm
93
def
77
ref
appTerm
48
ref
appTerm
absTerm
94
def
71
ref
42
ref
48
ref
absTerm
95
def
absTerm
96
def
appTerm
betaConv
96
ref
77
ref
appTerm
betaConv
85
ref
appThm
95
ref
48
ref
appTerm
betaConv
trans
trans
appThm
92
ref
93
ref
24
ref
appTerm
24
ref
appTerm
absTerm
97
def
96
ref
appTerm
betaConv
96
ref
24
ref
appTerm
betaConv
24
ref
refl
98
def
appThm
95
ref
24
ref
appTerm
betaConv
trans
trans
99
def
appThm
82
remove
refl
42
ref
9
ref
0
ref
86
ref
0
ref
86
remove
3
ref
cons
opType
nil
cons
cons
opType
constTerm
100
def
94
remove
appTerm
97
ref
appTerm
absTerm
101
def
48
ref
appTerm
betaConv
appThm
9
ref
0
ref
34
ref
40
remove
nil
cons
cons
opType
constTerm
102
def
80
remove
appTerm
refl
71
ref
101
remove
absTerm
103
def
77
ref
appTerm
betaConv
appThm
nil
87
remove
79
ref
appTerm
103
ref
appTerm
axiom
104
def
88
remove
appThm
eqMp
85
remove
appThm
eqMp
105
def
81
remove
assume
eqMp
96
ref
refl
106
def
appThm
eqMp
sym
30
ref
eqMp
107
def
105
remove
sym
92
ref
93
ref
refl
nil
67
ref
77
ref
nil
cons
108
def
cons
nil
cons
nil
cons
cons
70
ref
subst
77
ref
assume
109
def
eqMp
appThm
nil
67
ref
48
ref
nil
cons
110
def
cons
nil
cons
nil
cons
cons
70
ref
subst
48
ref
assume
eqMp
appThm
absThm
eqMp
111
def
deductAntisym
112
def
subst
nil
71
ref
53
ref
nil
cons
113
def
cons
75
remove
cons
nil
cons
cons
90
ref
111
remove
nil
"P"
2
ref
var
114
def
108
remove
cons
52
ref
110
remove
cons
nil
cons
cons
nil
cons
cons
91
ref
92
ref
93
remove
114
ref
varTerm
115
def
appTerm
116
def
54
ref
appTerm
absTerm
117
def
71
ref
42
ref
77
remove
absTerm
absTerm
118
def
appTerm
betaConv
118
ref
115
ref
appTerm
betaConv
54
ref
refl
119
def
appThm
42
ref
115
ref
absTerm
54
ref
appTerm
betaConv
trans
trans
appThm
97
ref
118
ref
appTerm
betaConv
118
ref
24
ref
appTerm
betaConv
98
remove
appThm
42
ref
24
ref
absTerm
24
ref
appTerm
betaConv
trans
trans
appThm
36
ref
79
ref
115
ref
appTerm
120
def
54
ref
appTerm
121
def
appTerm
refl
42
ref
100
remove
92
remove
116
remove
48
remove
appTerm
absTerm
appTerm
97
remove
appTerm
absTerm
54
ref
appTerm
betaConv
appThm
102
remove
120
remove
appTerm
refl
103
remove
115
ref
appTerm
betaConv
appThm
104
remove
115
ref
refl
appThm
eqMp
119
ref
appThm
eqMp
121
remove
assume
eqMp
122
def
118
remove
refl
appThm
eqMp
sym
30
ref
eqMp
123
def
subst
deductAntisym
eqMp
89
remove
78
remove
assume
eqMp
sym
109
remove
eqMp
107
remove
proveHyp
deductAntisym
124
def
subst
55
ref
46
ref
appTerm
125
def
betaConv
nil
73
remove
42
ref
125
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
"A"
19
ref
cons
126
def
nil
cons
127
def
37
ref
55
remove
nil
cons
cons
45
ref
46
ref
nil
cons
128
def
cons
nil
cons
cons
nil
cons
cons
nil
71
ref
60
ref
nil
cons
129
def
cons
42
ref
113
ref
cons
nil
cons
cons
nil
cons
cons
130
def
90
ref
subst
130
remove
112
ref
subst
36
ref
53
remove
appTerm
refl
62
remove
46
ref
appTerm
betaConv
appThm
64
remove
65
remove
60
remove
assume
eqMp
eqMp
46
ref
refl
131
def
appThm
eqMp
sym
30
ref
eqMp
eqMp
nil
114
ref
129
remove
cons
52
ref
113
remove
cons
nil
cons
cons
nil
cons
cons
123
ref
subst
deductAntisym
eqMp
132
def
subst
eqMp
eqMp
eqMp
eqMp
nil
114
ref
72
remove
cons
52
ref
74
remove
cons
nil
cons
cons
nil
cons
cons
123
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
subst
proveHyp
eqMp
defineTypeOp
133
def
pop
134
def
pop
135
def
pop
136
def
pop
137
def
19
ref
opType
138
def
3
ref
cons
opType
139
def
var
140
def
"s"
138
ref
var
141
def
9
ref
0
ref
138
ref
139
ref
nil
cons
142
def
cons
opType
143
def
constTerm
144
def
"Set.rest"
"_9596"
138
ref
var
145
def
"Set.delete"
"_9490"
138
ref
var
146
def
"_9491"
1
ref
var
147
def
136
ref
0
ref
4
ref
138
ref
nil
cons
148
def
cons
opType
constTerm
149
def
"v"
1
ref
var
150
def
14
ref
"y"
1
ref
var
151
def
79
ref
9
ref
0
ref
1
ref
5
ref
cons
opType
constTerm
152
def
150
ref
varTerm
appTerm
153
def
151
ref
varTerm
154
def
appTerm
appTerm
155
def
79
ref
"Set.member"
"_9420"
1
ref
var
156
def
"_9421"
138
ref
var
157
def
135
remove
0
ref
138
ref
5
remove
cons
opType
constTerm
158
def
157
ref
varTerm
159
def
appTerm
156
ref
varTerm
160
def
appTerm
absTerm
161
def
absTerm
162
def
defineConst
163
def
pop
164
def
0
ref
1
ref
142
remove
cons
opType
constTerm
165
def
154
ref
appTerm
166
def
146
ref
varTerm
167
def
appTerm
appTerm
"Data.Bool.~"
const
34
remove
constTerm
168
def
152
ref
154
ref
appTerm
169
def
147
ref
varTerm
170
def
appTerm
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
171
def
absTerm
172
def
absTerm
173
def
defineConst
174
def
pop
0
ref
138
ref
0
ref
1
ref
148
ref
cons
opType
nil
cons
cons
opType
constTerm
175
def
145
ref
varTerm
176
def
appTerm
"Set.choice"
"_9591"
138
ref
var
177
def
20
ref
45
ref
165
ref
46
ref
appTerm
178
def
177
ref
varTerm
179
def
appTerm
absTerm
appTerm
absTerm
180
def
defineConst
181
def
pop
0
ref
138
ref
19
remove
cons
opType
constTerm
182
def
176
ref
appTerm
appTerm
183
def
absTerm
184
def
defineConst
185
def
pop
0
ref
138
ref
148
ref
cons
opType
186
def
constTerm
187
def
141
ref
varTerm
188
def
appTerm
appTerm
175
ref
188
ref
appTerm
189
def
182
remove
188
ref
appTerm
190
def
appTerm
appTerm
absTerm
191
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
148
ref
cons
nil
cons
192
def
7
ref
cons
66
ref
subst
193
def
subst
145
remove
nil
67
ref
144
ref
187
remove
176
ref
appTerm
appTerm
183
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
185
remove
176
ref
refl
appThm
184
remove
176
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
39
ref
0
ref
139
ref
3
ref
cons
opType
194
def
constTerm
195
def
191
remove
appTerm
thm
39
ref
11
remove
constTerm
196
def
refl
197
def
16
ref
44
ref
refl
198
def
45
ref
91
ref
nil
"p"
138
ref
var
199
def
149
ref
17
ref
appTerm
200
def
nil
cons
cons
nil
cons
nil
cons
cons
nil
156
remove
128
remove
cons
157
remove
199
ref
varTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
163
remove
160
ref
refl
appThm
162
remove
160
remove
appTerm
betaConv
trans
159
ref
refl
appThm
161
remove
159
remove
appTerm
betaConv
trans
subst
201
def
subst
nil
"r"
4
ref
var
202
def
32
remove
cons
nil
cons
nil
cons
cons
202
ref
61
ref
158
ref
149
ref
202
ref
varTerm
203
def
appTerm
appTerm
appTerm
203
ref
appTerm
204
def
absTerm
205
def
203
ref
appTerm
206
def
betaConv
207
def
79
ref
195
ref
"a"
138
ref
var
208
def
144
ref
149
ref
158
ref
208
ref
varTerm
209
def
appTerm
appTerm
210
def
appTerm
209
ref
appTerm
211
def
absTerm
212
def
appTerm
213
def
appTerm
refl
197
ref
202
ref
91
ref
25
ref
203
ref
appTerm
214
def
betaConv
appThm
204
ref
refl
215
def
appThm
nil
67
ref
204
ref
nil
cons
cons
nil
cons
nil
cons
cons
67
ref
36
ref
36
ref
24
ref
appTerm
68
ref
appTerm
appTerm
68
ref
appTerm
absTerm
216
def
68
ref
appTerm
217
def
betaConv
nil
41
ref
216
ref
appTerm
218
def
axiom
nil
71
ref
218
remove
nil
cons
cons
42
ref
217
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
58
ref
51
ref
216
remove
nil
cons
cons
"x"
2
ref
var
219
def
68
ref
nil
cons
cons
nil
cons
220
def
cons
nil
cons
cons
132
ref
subst
eqMp
eqMp
subst
trans
absThm
appThm
appThm
nil
140
ref
212
remove
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
208
ref
nil
67
ref
211
ref
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
144
ref
refl
221
def
208
ref
210
ref
absTerm
209
ref
appTerm
betaConv
appThm
208
ref
209
ref
absTerm
209
ref
appTerm
betaConv
appThm
134
remove
209
ref
refl
appThm
eqMp
eqMp
absThm
eqMp
222
def
nil
71
ref
213
remove
nil
cons
223
def
cons
42
ref
196
ref
202
ref
36
ref
214
remove
appTerm
204
remove
appTerm
224
def
absTerm
225
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
112
ref
subst
proveHyp
nil
31
ref
225
remove
nil
cons
cons
nil
cons
nil
cons
cons
8
ref
66
ref
subst
subst
202
ref
nil
67
ref
224
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
91
ref
23
ref
25
remove
23
ref
varTerm
appTerm
betaConv
absThm
203
ref
refl
226
def
appThm
appThm
215
remove
appThm
91
ref
207
remove
appThm
202
remove
27
remove
203
ref
appTerm
absTerm
203
ref
appTerm
betaConv
appThm
133
remove
226
remove
appThm
eqMp
sym
eqMp
eqMp
absThm
eqMp
eqMp
eqMp
nil
114
ref
223
remove
cons
52
ref
196
ref
205
ref
appTerm
nil
cons
227
def
cons
nil
cons
cons
nil
cons
cons
91
ref
117
remove
96
ref
appTerm
betaConv
96
remove
115
remove
appTerm
betaConv
119
remove
appThm
95
remove
54
remove
appTerm
betaConv
trans
trans
appThm
99
remove
appThm
122
remove
106
remove
appThm
eqMp
sym
30
ref
eqMp
subst
proveHyp
nil
71
ref
227
remove
cons
42
ref
206
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
6
ref
31
ref
205
remove
nil
cons
cons
23
remove
203
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
132
ref
subst
eqMp
eqMp
subst
131
ref
appThm
trans
228
def
appThm
47
ref
refl
appThm
nil
219
ref
47
ref
nil
cons
cons
nil
cons
nil
cons
cons
59
remove
nil
67
ref
152
remove
46
ref
appTerm
229
def
46
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
131
remove
eqMp
subst
subst
trans
absThm
appThm
nil
67
ref
24
ref
nil
cons
cons
nil
cons
nil
cons
cons
230
def
67
ref
36
ref
44
ref
45
ref
68
ref
absTerm
231
def
appTerm
appTerm
68
ref
appTerm
absTerm
232
def
68
ref
appTerm
233
def
betaConv
nil
41
ref
232
ref
appTerm
234
def
axiom
nil
71
ref
234
remove
nil
cons
cons
42
ref
233
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
58
ref
51
ref
232
remove
nil
cons
cons
220
ref
cons
nil
cons
cons
132
ref
subst
eqMp
eqMp
235
def
subst
trans
absThm
appThm
230
remove
8
remove
235
remove
subst
subst
trans
sym
30
remove
eqMp
nil
196
ref
16
ref
44
ref
45
ref
36
ref
178
ref
200
remove
appTerm
appTerm
47
ref
appTerm
absTerm
appTerm
absTerm
appTerm
thm
"Set.{}"
149
ref
150
ref
14
ref
45
ref
79
ref
153
remove
46
ref
appTerm
236
def
appTerm
237
def
"Data.Bool.F"
const
2
ref
constTerm
238
def
appTerm
absTerm
appTerm
absTerm
appTerm
239
def
defineConst
240
def
pop
241
def
pop
240
ref
nil
144
ref
241
remove
138
ref
constTerm
242
def
appTerm
239
remove
appTerm
thm
"Set.universe"
149
ref
150
ref
14
ref
45
ref
237
ref
24
remove
appTerm
absTerm
appTerm
absTerm
appTerm
243
def
defineConst
244
def
pop
245
def
pop
244
remove
nil
144
ref
245
remove
138
ref
constTerm
appTerm
243
remove
appTerm
thm
nil
140
ref
141
ref
43
ref
168
ref
144
ref
188
ref
appTerm
246
def
242
ref
appTerm
247
def
appTerm
248
def
appTerm
165
ref
190
remove
appTerm
188
ref
appTerm
249
def
appTerm
250
def
absTerm
251
def
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
141
ref
nil
67
ref
250
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
nil
"t1"
2
ref
var
252
def
249
remove
nil
cons
cons
"t2"
2
remove
var
253
def
248
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
253
ref
36
ref
43
ref
253
ref
varTerm
254
def
appTerm
252
ref
varTerm
255
def
appTerm
256
def
appTerm
43
ref
168
ref
255
ref
appTerm
appTerm
168
ref
254
ref
appTerm
appTerm
257
def
appTerm
258
def
absTerm
259
def
254
ref
appTerm
260
def
betaConv
252
ref
41
ref
259
ref
appTerm
261
def
absTerm
262
def
255
ref
appTerm
263
def
betaConv
41
ref
refl
264
def
252
ref
264
remove
253
ref
258
remove
assume
sym
36
ref
257
remove
appTerm
256
remove
appTerm
265
def
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
nil
41
ref
252
remove
41
ref
253
remove
265
remove
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
71
ref
41
ref
262
ref
appTerm
nil
cons
cons
42
ref
263
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
58
ref
51
ref
262
remove
nil
cons
cons
219
ref
255
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
132
ref
subst
eqMp
eqMp
nil
71
ref
261
remove
nil
cons
cons
42
ref
260
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
58
ref
51
ref
259
remove
nil
cons
cons
219
remove
254
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
132
ref
subst
eqMp
eqMp
subst
sym
43
ref
refl
266
def
168
ref
refl
267
def
165
ref
refl
nil
177
remove
188
ref
nil
cons
268
def
cons
nil
cons
nil
cons
cons
181
remove
179
ref
refl
appThm
180
remove
179
remove
appTerm
betaConv
trans
subst
appThm
188
ref
refl
appThm
appThm
appThm
nil
67
ref
247
remove
nil
cons
269
def
cons
nil
cons
nil
cons
cons
67
ref
36
ref
168
ref
168
ref
68
ref
appTerm
270
def
appTerm
appTerm
68
ref
appTerm
absTerm
271
def
68
ref
appTerm
272
def
betaConv
nil
41
ref
271
ref
appTerm
273
def
axiom
nil
71
ref
273
remove
nil
cons
cons
42
ref
272
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
58
ref
51
ref
271
remove
nil
cons
cons
220
ref
cons
nil
cons
cons
132
ref
subst
eqMp
eqMp
subst
appThm
sym
nil
71
ref
168
ref
165
remove
20
remove
45
ref
178
ref
188
ref
appTerm
274
def
absTerm
275
def
appTerm
276
def
appTerm
188
ref
appTerm
appTerm
277
def
nil
cons
278
def
cons
42
ref
269
ref
cons
nil
cons
279
def
cons
nil
cons
cons
280
def
90
ref
subst
280
remove
112
ref
subst
198
ref
45
ref
36
ref
274
ref
appTerm
281
def
refl
178
ref
refl
240
remove
149
ref
refl
282
def
150
ref
14
ref
refl
283
def
45
ref
nil
67
ref
236
remove
nil
cons
cons
nil
cons
nil
cons
cons
67
ref
36
ref
79
ref
68
ref
appTerm
238
ref
appTerm
appTerm
238
ref
appTerm
absTerm
284
def
68
ref
appTerm
285
def
betaConv
nil
41
ref
284
ref
appTerm
286
def
axiom
nil
71
ref
286
remove
nil
cons
cons
42
ref
285
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
58
ref
51
ref
284
remove
nil
cons
cons
220
ref
cons
nil
cons
cons
132
ref
subst
eqMp
eqMp
subst
absThm
appThm
nil
67
ref
238
ref
nil
cons
cons
nil
cons
nil
cons
cons
67
ref
36
ref
14
ref
231
remove
appTerm
appTerm
68
ref
appTerm
absTerm
287
def
68
ref
appTerm
288
def
betaConv
nil
41
ref
287
ref
appTerm
289
def
axiom
nil
71
ref
289
remove
nil
cons
cons
42
ref
288
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
58
ref
51
ref
287
remove
nil
cons
cons
220
ref
cons
nil
cons
cons
132
ref
subst
eqMp
eqMp
subst
trans
absThm
appThm
trans
appThm
nil
16
ref
150
ref
238
ref
absTerm
290
def
nil
cons
cons
nil
cons
nil
cons
cons
228
remove
subst
290
remove
46
ref
appTerm
betaConv
trans
trans
appThm
nil
67
ref
274
ref
nil
cons
cons
nil
cons
nil
cons
cons
67
ref
36
ref
69
remove
238
remove
appTerm
appTerm
270
remove
appTerm
absTerm
291
def
68
remove
appTerm
292
def
betaConv
nil
41
remove
291
ref
appTerm
293
def
axiom
nil
71
ref
293
remove
nil
cons
cons
42
ref
292
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
58
remove
51
remove
291
remove
nil
cons
cons
220
remove
cons
nil
cons
cons
132
ref
subst
eqMp
eqMp
subst
trans
absThm
appThm
sym
91
ref
198
ref
45
ref
267
ref
275
ref
46
ref
appTerm
betaConv
294
def
appThm
absThm
appThm
appThm
267
ref
283
remove
45
ref
294
ref
absThm
appThm
appThm
appThm
nil
16
ref
275
ref
nil
cons
295
def
cons
nil
cons
nil
cons
cons
16
ref
36
ref
44
ref
45
ref
168
ref
47
ref
appTerm
absTerm
appTerm
296
def
appTerm
168
ref
14
ref
45
ref
47
remove
absTerm
appTerm
appTerm
297
def
appTerm
298
def
absTerm
299
def
17
remove
appTerm
300
def
betaConv
197
remove
16
ref
298
remove
assume
sym
36
ref
297
remove
appTerm
296
remove
appTerm
301
def
assume
sym
deductAntisym
absThm
appThm
nil
196
ref
16
remove
301
remove
absTerm
appTerm
axiom
eqMp
nil
71
ref
196
remove
299
ref
appTerm
nil
cons
cons
42
ref
300
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
6
remove
31
remove
299
remove
nil
cons
cons
33
remove
cons
nil
cons
cons
132
ref
subst
eqMp
eqMp
subst
eqMp
267
remove
22
remove
275
ref
refl
appThm
21
remove
275
ref
appTerm
betaConv
275
ref
276
remove
appTerm
betaConv
trans
trans
appThm
trans
sym
277
remove
assume
eqMp
eqMp
nil
71
ref
44
ref
45
ref
281
ref
178
ref
242
ref
appTerm
appTerm
absTerm
appTerm
nil
cons
cons
279
remove
cons
nil
cons
cons
124
ref
subst
proveHyp
nil
"t"
138
ref
var
302
def
242
ref
nil
cons
cons
nil
cons
nil
cons
cons
302
ref
43
ref
44
ref
45
ref
281
remove
178
ref
302
ref
varTerm
303
def
appTerm
304
def
appTerm
absTerm
appTerm
appTerm
246
ref
303
ref
appTerm
305
def
appTerm
absTerm
306
def
303
ref
appTerm
307
def
betaConv
141
ref
195
ref
306
ref
appTerm
308
def
absTerm
309
def
188
ref
appTerm
310
def
betaConv
195
ref
refl
311
def
141
ref
311
ref
302
ref
266
ref
91
ref
198
remove
45
ref
91
remove
294
remove
appThm
45
ref
304
ref
absTerm
312
def
46
ref
appTerm
betaConv
appThm
absThm
appThm
appThm
61
ref
275
remove
appTerm
312
ref
appTerm
refl
appThm
nil
"f"
4
ref
var
295
remove
cons
"g"
4
ref
var
312
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
"B"
3
ref
cons
313
def
127
remove
cons
7
ref
cons
"g"
0
ref
1
ref
"B"
varType
314
def
nil
cons
315
def
cons
316
def
opType
317
def
var
318
def
36
ref
44
ref
45
ref
9
ref
0
ref
314
ref
0
ref
314
ref
3
ref
cons
opType
319
def
nil
cons
cons
opType
constTerm
320
def
"f"
317
ref
var
321
def
varTerm
322
def
46
ref
appTerm
323
def
appTerm
324
def
318
remove
varTerm
325
def
46
ref
appTerm
appTerm
absTerm
appTerm
appTerm
9
ref
0
ref
317
ref
0
ref
317
ref
3
ref
cons
opType
326
def
nil
cons
cons
opType
constTerm
327
def
322
ref
appTerm
325
ref
appTerm
appTerm
absTerm
328
def
325
ref
appTerm
329
def
betaConv
321
ref
39
ref
0
ref
326
ref
3
ref
cons
opType
330
def
constTerm
331
def
328
ref
appTerm
332
def
absTerm
333
def
322
ref
appTerm
334
def
betaConv
nil
331
ref
333
ref
appTerm
335
def
axiom
nil
71
ref
335
remove
nil
cons
cons
42
ref
334
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
"A"
317
ref
nil
cons
336
def
cons
nil
cons
337
def
"P"
326
ref
var
338
def
333
remove
nil
cons
cons
"x"
317
ref
var
339
def
322
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
132
ref
subst
eqMp
eqMp
nil
71
ref
332
remove
nil
cons
cons
42
ref
329
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
337
ref
338
ref
328
remove
nil
cons
cons
339
ref
325
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
132
ref
subst
eqMp
eqMp
subst
subst
eqMp
61
ref
refl
340
def
45
ref
nil
199
ref
268
ref
cons
nil
cons
nil
cons
cons
201
ref
subst
absThm
appThm
45
ref
nil
199
remove
303
ref
nil
cons
341
def
cons
nil
cons
nil
cons
cons
201
remove
subst
absThm
appThm
trans
appThm
305
ref
refl
342
def
appThm
absThm
appThm
absThm
appThm
sym
311
ref
141
ref
311
ref
302
ref
266
remove
340
remove
126
remove
313
remove
nil
cons
cons
343
def
"t"
4
remove
var
344
def
158
ref
188
ref
appTerm
345
def
nil
cons
cons
nil
cons
nil
cons
cons
"t"
317
ref
var
346
def
327
ref
45
ref
346
remove
varTerm
347
def
46
ref
appTerm
absTerm
appTerm
347
ref
appTerm
absTerm
348
def
347
ref
appTerm
349
def
betaConv
nil
331
ref
348
ref
appTerm
350
def
axiom
nil
71
ref
350
remove
nil
cons
cons
42
ref
349
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
337
ref
338
ref
348
remove
nil
cons
cons
339
remove
347
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
132
ref
subst
eqMp
eqMp
351
def
subst
appThm
343
remove
344
remove
158
remove
303
ref
appTerm
352
def
nil
cons
cons
nil
cons
nil
cons
cons
351
remove
subst
appThm
appThm
342
remove
appThm
absThm
appThm
absThm
appThm
sym
nil
140
ref
141
ref
195
ref
302
ref
43
ref
61
remove
345
remove
appTerm
352
remove
appTerm
353
def
appTerm
305
ref
appTerm
354
def
absTerm
355
def
appTerm
356
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
141
ref
nil
67
ref
356
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
nil
140
ref
355
remove
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
302
ref
nil
67
ref
354
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
nil
71
ref
353
ref
nil
cons
357
def
cons
42
ref
305
ref
nil
cons
358
def
cons
nil
cons
cons
nil
cons
cons
359
def
90
remove
subst
359
remove
112
remove
subst
221
remove
nil
208
ref
268
ref
cons
nil
cons
nil
cons
cons
208
ref
144
ref
209
ref
appTerm
210
remove
appTerm
360
def
absTerm
361
def
209
ref
appTerm
362
def
betaConv
311
remove
208
ref
360
remove
assume
sym
211
remove
assume
sym
deductAntisym
absThm
appThm
222
remove
eqMp
nil
71
ref
195
ref
361
ref
appTerm
nil
cons
cons
42
ref
362
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
192
ref
140
ref
361
remove
nil
cons
cons
"x"
138
ref
var
363
def
209
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
132
ref
subst
eqMp
eqMp
364
def
subst
appThm
nil
208
remove
341
ref
cons
nil
cons
nil
cons
cons
364
remove
subst
appThm
sym
282
remove
353
remove
assume
appThm
eqMp
eqMp
nil
114
ref
357
remove
cons
52
ref
358
remove
cons
nil
cons
cons
nil
cons
cons
123
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
eqMp
365
def
nil
71
ref
195
ref
309
ref
appTerm
366
def
nil
cons
cons
42
ref
310
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
192
ref
140
ref
309
remove
nil
cons
cons
363
ref
268
remove
cons
nil
cons
cons
nil
cons
cons
132
ref
subst
eqMp
eqMp
nil
71
remove
308
remove
nil
cons
cons
42
remove
307
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
remove
subst
proveHyp
192
remove
140
ref
306
remove
nil
cons
cons
363
remove
341
remove
cons
nil
cons
cons
nil
cons
cons
132
remove
subst
eqMp
eqMp
subst
eqMp
eqMp
nil
114
remove
278
remove
cons
52
remove
269
remove
cons
nil
cons
cons
nil
cons
cons
123
remove
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
absThm
eqMp
nil
195
ref
251
remove
appTerm
thm
nil
140
ref
141
ref
36
ref
"Set.singleton"
"_9538"
138
ref
var
367
def
14
ref
45
ref
144
ref
367
ref
varTerm
368
def
appTerm
"Set.insert"
"_9432"
1
ref
var
369
def
"_9433"
138
ref
var
370
def
149
ref
150
ref
14
ref
151
ref
155
ref
"Data.Bool.\\/"
const
35
remove
constTerm
371
def
169
ref
369
ref
varTerm
372
def
appTerm
appTerm
166
ref
370
ref
varTerm
373
def
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
374
def
absTerm
375
def
absTerm
376
def
defineConst
377
def
pop
0
ref
1
ref
186
remove
nil
cons
378
def
cons
opType
constTerm
379
def
46
ref
appTerm
380
def
242
ref
appTerm
381
def
appTerm
absTerm
appTerm
382
def
absTerm
383
def
defineConst
384
def
pop
139
remove
constTerm
385
def
188
ref
appTerm
appTerm
14
ref
45
ref
246
remove
381
remove
appTerm
absTerm
appTerm
appTerm
absTerm
386
def
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
367
remove
nil
67
ref
36
ref
385
remove
368
ref
appTerm
appTerm
382
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
384
remove
368
ref
refl
appThm
383
remove
368
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
195
ref
386
remove
appTerm
thm
nil
140
ref
141
ref
195
ref
302
ref
36
ref
"Set.disjoint"
"_9526"
138
ref
var
387
def
"_9527"
138
ref
var
388
def
144
ref
"Set.intersect"
"_9461"
138
ref
var
389
def
"_9462"
138
ref
var
390
def
149
ref
150
ref
14
ref
45
ref
237
ref
79
ref
178
ref
389
ref
varTerm
391
def
appTerm
appTerm
178
ref
390
ref
varTerm
392
def
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
393
def
absTerm
394
def
absTerm
395
def
defineConst
396
def
pop
397
def
0
ref
138
ref
378
remove
cons
opType
398
def
constTerm
399
def
387
ref
varTerm
400
def
appTerm
388
ref
varTerm
401
def
appTerm
appTerm
242
ref
appTerm
402
def
absTerm
403
def
absTerm
404
def
defineConst
405
def
pop
143
ref
constTerm
406
def
188
ref
appTerm
303
ref
appTerm
appTerm
144
ref
399
ref
188
ref
appTerm
303
ref
appTerm
appTerm
407
def
242
remove
appTerm
appTerm
absTerm
appTerm
absTerm
408
def
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
387
remove
nil
67
ref
195
ref
388
ref
36
ref
406
remove
400
ref
appTerm
401
ref
appTerm
appTerm
402
remove
appTerm
409
def
absTerm
410
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
nil
140
ref
410
remove
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
388
remove
nil
67
ref
409
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
405
remove
400
ref
refl
appThm
404
remove
400
remove
appTerm
betaConv
trans
401
ref
refl
appThm
403
remove
401
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
195
ref
408
remove
appTerm
thm
nil
140
ref
141
ref
39
ref
0
ref
0
ref
137
ref
315
remove
opType
411
def
3
ref
cons
opType
412
def
3
ref
cons
opType
constTerm
413
def
"t"
411
ref
var
414
def
9
ref
0
ref
137
ref
336
remove
opType
415
def
0
ref
415
ref
3
ref
cons
opType
nil
cons
cons
opType
constTerm
416
def
"Set.bijections"
"_9579"
138
ref
var
417
def
"_9580"
411
ref
var
418
def
397
remove
0
ref
415
ref
0
ref
415
ref
415
remove
nil
cons
419
def
cons
opType
nil
cons
cons
opType
constTerm
420
def
"Set.injections"
"_9555"
138
ref
var
421
def
"_9556"
411
ref
var
422
def
136
ref
0
ref
326
remove
419
ref
cons
opType
constTerm
423
def
"v"
317
ref
var
424
def
13
ref
330
remove
constTerm
425
def
321
ref
79
ref
327
remove
424
ref
varTerm
appTerm
322
ref
appTerm
appTerm
426
def
79
ref
44
ref
45
ref
43
ref
178
ref
421
ref
varTerm
427
def
appTerm
428
def
appTerm
164
ref
0
ref
314
ref
412
ref
nil
cons
429
def
cons
opType
constTerm
430
def
323
ref
appTerm
431
def
422
ref
varTerm
432
def
appTerm
appTerm
absTerm
appTerm
appTerm
44
ref
45
ref
44
ref
151
ref
43
ref
79
ref
428
remove
appTerm
79
ref
166
ref
427
ref
appTerm
appTerm
324
remove
322
ref
154
ref
appTerm
433
def
appTerm
434
def
appTerm
appTerm
appTerm
229
remove
154
remove
appTerm
435
def
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
436
def
absTerm
437
def
absTerm
438
def
defineConst
439
def
pop
0
ref
138
ref
0
ref
411
ref
419
remove
cons
opType
nil
cons
cons
opType
440
def
constTerm
441
def
417
ref
varTerm
442
def
appTerm
418
ref
varTerm
443
def
appTerm
appTerm
"Set.surjections"
"_9567"
138
ref
var
444
def
"_9568"
411
ref
var
445
def
423
ref
424
ref
425
ref
321
ref
426
ref
79
ref
44
ref
45
ref
43
ref
178
ref
444
ref
varTerm
446
def
appTerm
appTerm
431
ref
445
ref
varTerm
447
def
appTerm
appTerm
absTerm
appTerm
appTerm
39
ref
0
ref
319
ref
3
ref
cons
opType
448
def
constTerm
449
def
"x"
314
ref
var
450
def
43
ref
430
ref
450
ref
varTerm
451
def
appTerm
452
def
447
ref
appTerm
appTerm
14
ref
151
ref
79
ref
166
ref
446
ref
appTerm
appTerm
320
ref
433
remove
appTerm
451
remove
appTerm
453
def
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
454
def
absTerm
455
def
absTerm
456
def
defineConst
457
def
pop
440
ref
constTerm
458
def
442
ref
appTerm
443
ref
appTerm
appTerm
459
def
absTerm
460
def
absTerm
461
def
defineConst
462
def
pop
440
remove
constTerm
463
def
188
ref
appTerm
414
ref
varTerm
464
def
appTerm
appTerm
420
remove
441
ref
188
ref
appTerm
464
ref
appTerm
465
def
appTerm
458
ref
188
ref
appTerm
464
ref
appTerm
466
def
appTerm
appTerm
absTerm
appTerm
absTerm
467
def
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
417
remove
nil
67
ref
413
ref
418
ref
416
ref
463
remove
442
ref
appTerm
443
ref
appTerm
appTerm
459
remove
appTerm
468
def
absTerm
469
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
nil
"P"
412
remove
var
470
def
469
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
411
ref
nil
cons
471
def
cons
nil
cons
7
ref
cons
66
ref
subst
472
def
subst
418
remove
nil
67
ref
468
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
462
remove
442
ref
refl
appThm
461
remove
442
remove
appTerm
betaConv
trans
443
ref
refl
appThm
460
remove
443
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
195
ref
467
remove
appTerm
thm
nil
140
ref
141
ref
195
ref
302
ref
36
ref
"Set.properSubset"
"_9514"
138
ref
var
473
def
"_9515"
138
ref
var
474
def
79
ref
"Set.subset"
"_9502"
138
ref
var
475
def
"_9503"
138
ref
var
476
def
44
ref
45
ref
43
ref
178
ref
475
ref
varTerm
477
def
appTerm
appTerm
178
ref
476
ref
varTerm
478
def
appTerm
appTerm
absTerm
appTerm
479
def
absTerm
480
def
absTerm
481
def
defineConst
482
def
pop
143
ref
constTerm
483
def
473
ref
varTerm
484
def
appTerm
474
ref
varTerm
485
def
appTerm
appTerm
168
ref
144
ref
484
ref
appTerm
485
ref
appTerm
appTerm
appTerm
486
def
absTerm
487
def
absTerm
488
def
defineConst
489
def
pop
143
remove
constTerm
490
def
188
ref
appTerm
303
ref
appTerm
appTerm
79
ref
483
ref
188
ref
appTerm
303
ref
appTerm
491
def
appTerm
168
ref
305
remove
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
492
def
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
473
remove
nil
67
ref
195
ref
474
ref
36
ref
490
remove
484
ref
appTerm
485
ref
appTerm
appTerm
486
remove
appTerm
493
def
absTerm
494
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
nil
140
ref
494
remove
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
474
remove
nil
67
ref
493
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
489
remove
484
ref
refl
appThm
488
remove
484
remove
appTerm
betaConv
trans
485
ref
refl
appThm
487
remove
485
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
195
ref
492
remove
appTerm
thm
nil
140
ref
141
ref
195
ref
302
ref
36
ref
491
remove
appTerm
44
ref
45
ref
43
ref
274
ref
appTerm
495
def
304
ref
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
496
def
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
475
remove
nil
67
ref
195
ref
476
ref
36
remove
483
remove
477
ref
appTerm
478
ref
appTerm
appTerm
479
remove
appTerm
497
def
absTerm
498
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
nil
140
ref
498
remove
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
476
remove
nil
67
ref
497
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
482
remove
477
ref
refl
appThm
481
remove
477
remove
appTerm
betaConv
trans
478
ref
refl
appThm
480
remove
478
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
195
ref
496
remove
appTerm
thm
365
remove
nil
366
remove
thm
nil
"P"
0
ref
137
ref
148
ref
opType
499
def
3
ref
cons
opType
500
def
var
501
def
"s"
499
ref
var
502
def
144
ref
"Set.bigIntersect"
"_9473"
499
ref
var
503
def
149
ref
150
ref
14
ref
45
ref
237
ref
195
ref
"u"
138
ref
var
504
def
43
ref
164
remove
0
ref
138
ref
500
ref
nil
cons
cons
opType
constTerm
504
ref
varTerm
505
def
appTerm
506
def
503
ref
varTerm
507
def
appTerm
appTerm
178
ref
505
remove
appTerm
508
def
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
509
def
absTerm
510
def
defineConst
511
def
pop
0
ref
499
ref
148
remove
cons
opType
512
def
constTerm
513
def
502
ref
varTerm
514
def
appTerm
appTerm
149
ref
150
ref
14
ref
45
ref
237
ref
195
ref
504
ref
43
ref
506
ref
514
ref
appTerm
515
def
appTerm
508
ref
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
516
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
499
ref
nil
cons
cons
nil
cons
7
ref
cons
66
ref
subst
517
def
subst
503
remove
nil
67
ref
144
ref
513
remove
507
ref
appTerm
appTerm
509
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
511
remove
507
ref
refl
appThm
510
remove
507
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
39
remove
0
ref
500
remove
3
ref
cons
opType
constTerm
518
def
516
remove
appTerm
thm
nil
501
remove
502
remove
144
ref
"Set.bigUnion"
"_9456"
499
remove
var
519
def
149
ref
150
ref
14
ref
45
ref
237
ref
13
ref
194
remove
constTerm
520
def
504
ref
79
ref
506
remove
519
ref
varTerm
521
def
appTerm
appTerm
508
ref
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
522
def
absTerm
523
def
defineConst
524
def
pop
512
remove
constTerm
525
def
514
remove
appTerm
appTerm
149
ref
150
ref
14
ref
45
ref
237
ref
520
remove
504
remove
79
ref
515
remove
appTerm
508
remove
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
526
def
nil
cons
cons
nil
cons
nil
cons
cons
517
remove
subst
519
remove
nil
67
ref
144
ref
525
remove
521
ref
appTerm
appTerm
522
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
524
remove
521
ref
refl
appThm
523
remove
521
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
518
remove
526
remove
appTerm
thm
nil
37
ref
45
ref
195
ref
141
ref
144
ref
380
remove
188
ref
appTerm
appTerm
149
ref
150
ref
14
ref
151
ref
155
ref
371
ref
169
remove
46
ref
appTerm
527
def
appTerm
166
remove
188
ref
appTerm
528
def
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
529
def
nil
cons
cons
nil
cons
nil
cons
cons
66
ref
subst
369
remove
nil
67
ref
195
ref
370
ref
144
ref
379
remove
372
ref
appTerm
373
ref
appTerm
appTerm
374
remove
appTerm
530
def
absTerm
531
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
nil
140
ref
531
remove
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
370
remove
nil
67
ref
530
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
377
remove
372
ref
refl
appThm
376
remove
372
remove
appTerm
betaConv
trans
373
ref
refl
appThm
375
remove
373
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
44
ref
529
remove
appTerm
thm
nil
140
ref
141
ref
195
ref
302
ref
407
remove
149
ref
150
ref
14
ref
45
ref
237
ref
79
ref
274
ref
appTerm
532
def
304
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
533
def
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
389
remove
nil
67
ref
195
ref
390
ref
144
ref
399
remove
391
ref
appTerm
392
ref
appTerm
appTerm
393
remove
appTerm
534
def
absTerm
535
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
nil
140
ref
535
remove
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
390
remove
nil
67
ref
534
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
396
remove
391
ref
refl
appThm
395
remove
391
remove
appTerm
betaConv
trans
392
ref
refl
appThm
394
remove
392
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
195
ref
533
remove
appTerm
thm
nil
140
ref
141
ref
195
ref
302
ref
144
ref
"Set.union"
"_9444"
138
ref
var
536
def
"_9445"
138
ref
var
537
def
149
ref
150
ref
14
ref
45
ref
237
ref
371
ref
178
ref
536
ref
varTerm
538
def
appTerm
appTerm
178
ref
537
ref
varTerm
539
def
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
540
def
absTerm
541
def
absTerm
542
def
defineConst
543
def
pop
398
ref
constTerm
544
def
188
ref
appTerm
303
ref
appTerm
appTerm
149
ref
150
ref
14
ref
45
ref
237
ref
371
remove
274
remove
appTerm
304
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
545
def
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
536
remove
nil
67
ref
195
ref
537
ref
144
ref
544
remove
538
ref
appTerm
539
ref
appTerm
appTerm
540
remove
appTerm
546
def
absTerm
547
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
nil
140
ref
547
remove
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
537
remove
nil
67
ref
546
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
543
remove
538
ref
refl
appThm
542
remove
538
remove
appTerm
betaConv
trans
539
ref
refl
appThm
541
remove
539
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
195
ref
545
remove
appTerm
thm
nil
140
ref
141
ref
44
ref
45
ref
144
ref
189
remove
46
ref
appTerm
appTerm
149
ref
150
ref
14
ref
151
ref
155
remove
79
ref
528
remove
appTerm
548
def
168
ref
527
remove
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
549
def
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
146
remove
nil
67
ref
44
ref
147
ref
144
ref
175
remove
167
ref
appTerm
170
ref
appTerm
appTerm
171
remove
appTerm
550
def
absTerm
551
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
nil
37
remove
551
remove
nil
cons
cons
nil
cons
nil
cons
cons
66
ref
subst
147
remove
nil
67
ref
550
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
174
remove
167
ref
refl
appThm
173
remove
167
remove
appTerm
betaConv
trans
170
ref
refl
appThm
172
remove
170
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
195
ref
549
remove
appTerm
thm
nil
140
ref
141
ref
195
ref
302
remove
144
ref
"Set.difference"
"_9478"
138
ref
var
552
def
"_9479"
138
ref
var
553
def
149
ref
150
ref
14
ref
45
ref
237
ref
79
ref
178
ref
552
ref
varTerm
554
def
appTerm
appTerm
168
ref
178
ref
553
ref
varTerm
555
def
appTerm
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
556
def
absTerm
557
def
absTerm
558
def
defineConst
559
def
pop
398
remove
constTerm
560
def
188
ref
appTerm
303
remove
appTerm
appTerm
149
remove
150
remove
14
ref
45
ref
237
remove
532
ref
168
remove
304
remove
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
561
def
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
552
remove
nil
67
ref
195
ref
553
ref
144
remove
560
remove
554
ref
appTerm
555
ref
appTerm
appTerm
556
remove
appTerm
562
def
absTerm
563
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
nil
140
ref
563
remove
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
553
remove
nil
67
ref
562
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
559
remove
554
ref
refl
appThm
558
remove
554
remove
appTerm
betaConv
trans
555
ref
refl
appThm
557
remove
555
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
195
ref
561
remove
appTerm
thm
nil
338
remove
321
ref
195
ref
141
ref
9
ref
0
ref
411
ref
429
remove
cons
opType
constTerm
564
def
"Set.image"
"_9543"
317
ref
var
565
def
"_9544"
138
ref
var
566
def
136
ref
0
ref
319
remove
471
ref
cons
opType
constTerm
567
def
"v"
314
ref
var
568
def
13
remove
448
remove
constTerm
569
def
"y"
314
ref
var
570
def
79
ref
320
ref
568
ref
varTerm
appTerm
570
ref
varTerm
571
def
appTerm
appTerm
572
def
14
ref
45
ref
79
ref
178
ref
566
ref
varTerm
573
def
appTerm
appTerm
320
remove
571
ref
appTerm
574
def
565
ref
varTerm
575
def
46
ref
appTerm
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
576
def
absTerm
577
def
absTerm
578
def
defineConst
579
def
pop
0
ref
317
remove
0
ref
138
ref
471
remove
cons
opType
nil
cons
cons
opType
constTerm
580
def
322
remove
appTerm
188
ref
appTerm
appTerm
567
remove
568
remove
569
ref
570
ref
572
remove
14
ref
45
ref
532
ref
574
remove
323
remove
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
581
def
nil
cons
cons
nil
cons
nil
cons
cons
337
remove
7
remove
cons
66
remove
subst
subst
565
remove
nil
67
ref
195
ref
566
ref
564
remove
580
remove
575
ref
appTerm
573
ref
appTerm
appTerm
576
remove
appTerm
582
def
absTerm
583
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
nil
140
ref
583
remove
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
566
remove
nil
67
ref
582
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
579
remove
575
ref
refl
appThm
578
remove
575
remove
appTerm
betaConv
trans
573
ref
refl
appThm
577
remove
573
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
331
remove
581
remove
appTerm
thm
nil
140
ref
141
ref
413
ref
414
ref
9
ref
0
ref
137
remove
"Data.Pair.*"
typeOp
316
remove
opType
584
def
nil
cons
585
def
opType
586
def
0
ref
586
ref
3
ref
cons
opType
nil
cons
cons
opType
constTerm
587
def
"Set.cross"
"_10443"
138
ref
var
588
def
"_10444"
411
ref
var
589
def
136
remove
0
ref
0
ref
584
ref
3
remove
cons
opType
590
def
586
remove
nil
cons
591
def
cons
opType
constTerm
592
def
"v"
584
ref
var
593
def
14
ref
45
ref
569
ref
570
ref
79
ref
9
remove
0
ref
584
remove
590
remove
nil
cons
cons
opType
constTerm
593
ref
varTerm
appTerm
"Data.Pair.,"
const
0
ref
1
remove
0
ref
314
remove
585
remove
cons
opType
nil
cons
cons
opType
constTerm
46
remove
appTerm
571
ref
appTerm
appTerm
appTerm
594
def
79
ref
178
remove
588
ref
varTerm
595
def
appTerm
appTerm
430
remove
571
remove
appTerm
596
def
589
ref
varTerm
597
def
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
598
def
absTerm
599
def
absTerm
600
def
defineConst
601
def
pop
0
ref
138
remove
0
remove
411
remove
591
remove
cons
opType
nil
cons
cons
opType
constTerm
602
def
188
remove
appTerm
464
ref
appTerm
appTerm
592
remove
593
remove
14
ref
45
ref
569
remove
570
remove
594
remove
532
ref
596
remove
464
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
603
def
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
588
remove
nil
67
ref
413
ref
589
ref
587
remove
602
remove
595
ref
appTerm
597
ref
appTerm
appTerm
598
remove
appTerm
604
def
absTerm
605
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
nil
470
ref
605
remove
nil
cons
cons
nil
cons
nil
cons
cons
472
ref
subst
589
remove
nil
67
ref
604
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
601
remove
595
ref
refl
appThm
600
remove
595
remove
appTerm
betaConv
trans
597
ref
refl
appThm
599
remove
597
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
195
ref
603
remove
appTerm
thm
nil
140
ref
141
ref
413
ref
414
ref
416
ref
466
remove
appTerm
423
ref
424
ref
425
ref
321
ref
426
ref
79
remove
44
ref
45
ref
495
remove
431
remove
464
ref
appTerm
appTerm
absTerm
appTerm
appTerm
606
def
449
remove
450
remove
43
ref
452
remove
464
remove
appTerm
appTerm
14
remove
151
ref
548
ref
453
remove
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
607
def
nil
cons
cons
nil
cons
nil
cons
cons
193
ref
subst
444
remove
nil
67
ref
413
ref
445
ref
416
ref
458
remove
446
ref
appTerm
447
ref
appTerm
appTerm
454
remove
appTerm
608
def
absTerm
609
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
nil
470
ref
609
remove
nil
cons
cons
nil
cons
nil
cons
cons
472
ref
subst
445
remove
nil
67
ref
608
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
457
remove
446
ref
refl
appThm
456
remove
446
remove
appTerm
betaConv
trans
447
ref
refl
appThm
455
remove
447
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
195
ref
607
remove
appTerm
thm
nil
140
remove
141
remove
413
ref
414
remove
416
ref
465
remove
appTerm
423
remove
424
remove
425
remove
321
remove
426
remove
606
remove
44
ref
45
remove
44
remove
151
remove
43
remove
532
remove
548
remove
434
remove
appTerm
appTerm
appTerm
435
remove
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
610
def
nil
cons
cons
nil
cons
nil
cons
cons
193
remove
subst
421
remove
nil
67
ref
413
remove
422
ref
416
remove
441
remove
427
ref
appTerm
432
ref
appTerm
appTerm
436
remove
appTerm
611
def
absTerm
612
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
70
ref
subst
nil
470
remove
612
remove
nil
cons
cons
nil
cons
nil
cons
cons
472
remove
subst
422
remove
nil
67
remove
611
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
remove
subst
439
remove
427
ref
refl
appThm
438
remove
427
remove
appTerm
betaConv
trans
432
ref
refl
appThm
437
remove
432
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
195
remove
610
remove
appTerm
thm