6
version
nil
"P"
"->"
typeOp
0
def
0
ref
"A"
varType
1
def
"bool"
typeOp
nil
opType
2
def
nil
cons
3
def
cons
opType
4
def
3
ref
cons
opType
5
def
var
6
def
"p"
4
ref
var
7
def
"Data.Bool.!"
const
8
def
0
ref
0
ref
"Data.List.list"
typeOp
9
def
1
ref
nil
cons
10
def
opType
11
def
3
ref
cons
opType
12
def
3
ref
cons
opType
13
def
constTerm
14
def
"l"
11
ref
var
15
def
"Number.Natural.<="
const
0
ref
"Number.Natural.natural"
typeOp
nil
opType
16
def
0
ref
16
ref
3
ref
cons
opType
17
def
nil
cons
cons
opType
18
def
constTerm
19
def
"Data.List.length"
const
0
ref
11
ref
16
ref
nil
cons
20
def
cons
opType
constTerm
21
def
"Data.List.filter"
const
22
def
0
ref
4
ref
0
ref
11
ref
11
ref
nil
cons
23
def
cons
opType
nil
cons
24
def
cons
opType
constTerm
25
def
7
ref
varTerm
26
def
appTerm
27
def
15
ref
varTerm
28
def
appTerm
29
def
appTerm
appTerm
21
ref
28
ref
appTerm
appTerm
absTerm
30
def
appTerm
31
def
absTerm
32
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
4
ref
nil
cons
33
def
cons
nil
cons
34
def
nil
nil
cons
35
def
cons
36
def
"="
const
37
def
0
ref
2
ref
0
ref
2
ref
3
ref
cons
opType
38
def
nil
cons
cons
opType
39
def
constTerm
40
def
8
ref
5
ref
constTerm
41
def
"P"
4
ref
var
42
def
varTerm
43
def
appTerm
44
def
appTerm
refl
7
ref
37
ref
0
ref
4
ref
5
ref
nil
cons
cons
opType
constTerm
26
ref
appTerm
"x"
1
ref
var
45
def
"Data.Bool.T"
const
2
ref
constTerm
46
def
absTerm
47
def
appTerm
absTerm
48
def
43
ref
appTerm
betaConv
49
def
appThm
nil
37
ref
0
ref
5
ref
0
ref
5
ref
3
ref
cons
opType
50
def
nil
cons
cons
opType
constTerm
51
def
41
ref
appTerm
48
remove
appTerm
axiom
43
ref
refl
52
def
appThm
53
def
eqMp
sym
54
def
subst
55
def
subst
7
ref
nil
"t"
2
ref
var
56
def
31
remove
nil
cons
57
def
cons
nil
cons
nil
cons
cons
40
ref
56
ref
varTerm
58
def
appTerm
59
def
46
ref
appTerm
60
def
assume
sym
nil
46
ref
axiom
61
def
eqMp
58
ref
assume
61
ref
deductAntisym
deductAntisym
62
def
subst
19
ref
refl
63
def
21
ref
refl
64
def
7
ref
37
ref
0
ref
11
ref
12
ref
nil
cons
65
def
cons
opType
constTerm
66
def
27
ref
"Data.List.[]"
const
67
def
11
ref
constTerm
68
def
appTerm
69
def
appTerm
68
ref
appTerm
absTerm
70
def
26
ref
appTerm
71
def
betaConv
nil
8
ref
50
remove
constTerm
72
def
70
ref
appTerm
73
def
axiom
nil
"p"
2
ref
var
74
def
73
remove
nil
cons
cons
"q"
2
ref
var
75
def
71
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
40
ref
"Data.Bool.==>"
const
39
ref
constTerm
76
def
74
ref
varTerm
77
def
appTerm
78
def
75
ref
varTerm
79
def
appTerm
80
def
appTerm
refl
74
ref
75
ref
40
ref
"Data.Bool./\\"
const
39
ref
constTerm
81
def
77
ref
appTerm
82
def
79
ref
appTerm
83
def
appTerm
84
def
77
ref
appTerm
absTerm
85
def
absTerm
86
def
77
ref
appTerm
betaConv
79
ref
refl
87
def
appThm
85
remove
79
ref
appTerm
betaConv
trans
appThm
nil
37
ref
0
ref
39
ref
0
ref
39
ref
3
ref
cons
opType
88
def
nil
cons
cons
opType
constTerm
89
def
76
ref
appTerm
86
remove
appTerm
axiom
77
ref
refl
90
def
appThm
87
ref
appThm
eqMp
91
def
sym
92
def
84
remove
refl
75
ref
37
ref
0
ref
88
ref
0
ref
88
remove
3
ref
cons
opType
nil
cons
cons
opType
constTerm
93
def
"f"
39
ref
var
94
def
94
ref
varTerm
95
def
77
ref
appTerm
79
ref
appTerm
absTerm
96
def
appTerm
94
ref
95
ref
46
ref
appTerm
46
ref
appTerm
absTerm
97
def
appTerm
absTerm
98
def
79
ref
appTerm
betaConv
appThm
37
ref
0
ref
38
ref
0
ref
38
ref
3
ref
cons
opType
99
def
nil
cons
cons
opType
constTerm
100
def
82
remove
appTerm
refl
74
ref
98
remove
absTerm
101
def
77
ref
appTerm
betaConv
appThm
nil
89
ref
81
ref
appTerm
101
ref
appTerm
axiom
102
def
90
remove
appThm
eqMp
87
ref
appThm
eqMp
103
def
sym
94
ref
95
ref
refl
nil
56
ref
77
ref
nil
cons
104
def
cons
nil
cons
nil
cons
cons
62
ref
subst
77
ref
assume
105
def
eqMp
appThm
nil
56
ref
79
ref
nil
cons
106
def
cons
nil
cons
nil
cons
cons
62
ref
subst
79
ref
assume
107
def
eqMp
appThm
absThm
eqMp
108
def
nil
"P"
2
ref
var
109
def
104
ref
cons
"Q"
2
ref
var
110
def
106
ref
cons
nil
cons
111
def
cons
nil
cons
cons
40
ref
refl
112
def
94
ref
95
remove
109
ref
varTerm
113
def
appTerm
114
def
110
ref
varTerm
115
def
appTerm
absTerm
116
def
74
ref
75
ref
77
ref
absTerm
absTerm
117
def
appTerm
betaConv
117
ref
113
ref
appTerm
betaConv
115
ref
refl
118
def
appThm
75
ref
113
ref
absTerm
115
ref
appTerm
betaConv
trans
trans
appThm
97
ref
117
ref
appTerm
betaConv
117
ref
46
ref
appTerm
betaConv
46
ref
refl
119
def
appThm
75
ref
46
ref
absTerm
46
ref
appTerm
betaConv
trans
trans
appThm
40
ref
81
ref
113
ref
appTerm
120
def
115
ref
appTerm
121
def
appTerm
refl
75
ref
93
remove
94
remove
114
remove
79
ref
appTerm
absTerm
appTerm
97
ref
appTerm
absTerm
115
ref
appTerm
betaConv
appThm
100
ref
120
remove
appTerm
refl
101
remove
113
ref
appTerm
betaConv
appThm
102
remove
113
ref
refl
122
def
appThm
eqMp
118
ref
appThm
eqMp
121
remove
assume
eqMp
123
def
117
remove
refl
appThm
eqMp
sym
61
ref
eqMp
124
def
subst
deductAntisym
eqMp
91
remove
80
ref
assume
eqMp
sym
105
remove
eqMp
112
ref
96
remove
74
ref
75
ref
79
ref
absTerm
125
def
absTerm
126
def
appTerm
betaConv
126
ref
77
ref
appTerm
betaConv
87
ref
appThm
125
ref
79
ref
appTerm
betaConv
trans
trans
appThm
97
remove
126
ref
appTerm
betaConv
126
ref
46
ref
appTerm
betaConv
119
remove
appThm
125
ref
46
ref
appTerm
betaConv
trans
trans
127
def
appThm
103
remove
83
ref
assume
eqMp
126
ref
refl
128
def
appThm
eqMp
sym
61
ref
eqMp
129
def
proveHyp
deductAntisym
130
def
subst
proveHyp
34
ref
6
ref
70
remove
nil
cons
cons
"x"
4
ref
var
26
ref
nil
cons
cons
nil
cons
131
def
cons
nil
cons
cons
nil
74
ref
44
ref
nil
cons
132
def
cons
75
ref
43
ref
45
ref
varTerm
133
def
appTerm
134
def
nil
cons
135
def
cons
nil
cons
cons
nil
cons
cons
136
def
92
ref
subst
136
remove
129
remove
108
remove
deductAntisym
137
def
subst
40
ref
134
ref
appTerm
refl
47
remove
133
ref
appTerm
betaConv
appThm
49
remove
53
remove
44
remove
assume
eqMp
eqMp
133
ref
refl
138
def
appThm
eqMp
sym
61
ref
eqMp
eqMp
nil
109
ref
132
remove
cons
110
ref
135
ref
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
139
def
subst
eqMp
eqMp
140
def
appThm
appThm
21
ref
68
ref
appTerm
141
def
refl
appThm
nil
"n"
16
ref
var
142
def
141
ref
nil
cons
cons
nil
cons
nil
cons
cons
nil
56
ref
19
ref
142
ref
varTerm
143
def
appTerm
144
def
143
ref
appTerm
145
def
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
142
ref
145
remove
absTerm
146
def
143
ref
appTerm
147
def
betaConv
nil
8
ref
0
ref
17
ref
3
ref
cons
opType
148
def
constTerm
149
def
146
ref
appTerm
150
def
axiom
nil
74
ref
150
remove
nil
cons
cons
75
ref
147
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
"A"
20
ref
cons
nil
cons
151
def
"P"
17
remove
var
152
def
146
remove
nil
cons
cons
"x"
16
ref
var
153
def
143
ref
nil
cons
cons
nil
cons
154
def
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
eqMp
155
def
subst
trans
sym
61
ref
eqMp
nil
74
ref
19
ref
21
ref
69
ref
appTerm
appTerm
141
remove
appTerm
156
def
nil
cons
cons
75
ref
41
ref
"h"
1
ref
var
157
def
14
ref
"t"
11
ref
var
158
def
76
ref
19
ref
21
ref
27
ref
158
ref
varTerm
159
def
appTerm
160
def
appTerm
161
def
appTerm
162
def
21
ref
159
ref
appTerm
163
def
appTerm
164
def
appTerm
19
ref
21
ref
27
ref
"Data.List.::"
const
165
def
0
ref
1
ref
24
ref
cons
opType
constTerm
157
ref
varTerm
166
def
appTerm
167
def
159
ref
appTerm
168
def
appTerm
169
def
appTerm
appTerm
21
ref
168
ref
appTerm
170
def
appTerm
171
def
appTerm
172
def
absTerm
173
def
appTerm
174
def
absTerm
175
def
appTerm
176
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
137
ref
subst
proveHyp
nil
42
ref
175
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
157
ref
nil
56
ref
174
remove
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
nil
"P"
12
ref
var
177
def
173
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
23
remove
cons
178
def
nil
cons
179
def
35
ref
cons
180
def
54
ref
subst
181
def
subst
158
ref
nil
56
ref
172
remove
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
nil
74
ref
164
ref
nil
cons
182
def
cons
75
ref
171
remove
nil
cons
183
def
cons
nil
cons
cons
nil
cons
cons
184
def
92
ref
subst
184
remove
137
ref
subst
63
ref
64
remove
158
ref
66
ref
169
ref
appTerm
"Data.Bool.cond"
const
185
def
0
ref
2
ref
0
ref
11
ref
24
remove
cons
opType
186
def
nil
cons
cons
opType
constTerm
187
def
26
ref
166
ref
appTerm
188
def
appTerm
189
def
167
ref
160
ref
appTerm
190
def
appTerm
160
ref
appTerm
191
def
appTerm
absTerm
192
def
159
ref
appTerm
193
def
betaConv
157
ref
14
ref
192
ref
appTerm
194
def
absTerm
195
def
166
ref
appTerm
196
def
betaConv
7
ref
41
ref
195
ref
appTerm
197
def
absTerm
198
def
26
ref
appTerm
199
def
betaConv
nil
72
ref
198
ref
appTerm
200
def
axiom
nil
74
ref
200
remove
nil
cons
cons
75
ref
199
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
34
ref
6
ref
198
remove
nil
cons
cons
131
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
197
remove
nil
cons
cons
75
ref
196
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
"A"
10
ref
cons
201
def
nil
cons
202
def
42
ref
195
remove
nil
cons
cons
45
ref
166
ref
nil
cons
cons
203
def
nil
cons
204
def
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
194
remove
nil
cons
cons
75
ref
193
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
179
ref
177
ref
192
remove
nil
cons
cons
"x"
11
ref
var
205
def
159
ref
nil
cons
cons
nil
cons
206
def
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
207
def
appThm
appThm
170
ref
refl
appThm
sym
142
ref
81
ref
19
ref
21
ref
191
ref
appTerm
208
def
appTerm
209
def
143
ref
appTerm
appTerm
144
ref
170
ref
appTerm
appTerm
absTerm
210
def
"Number.Natural.suc"
const
0
ref
16
ref
20
remove
cons
opType
constTerm
211
def
161
ref
appTerm
212
def
appTerm
betaConv
sym
112
ref
"_16094"
11
ref
var
213
def
19
ref
21
ref
213
remove
varTerm
appTerm
appTerm
212
ref
appTerm
absTerm
214
def
191
ref
appTerm
betaConv
appThm
81
ref
refl
215
def
76
ref
188
ref
appTerm
216
def
refl
217
def
214
ref
190
ref
appTerm
betaConv
appThm
appThm
76
ref
"Data.Bool.~"
const
38
ref
constTerm
218
def
188
ref
appTerm
219
def
appTerm
220
def
refl
221
def
214
ref
160
ref
appTerm
betaConv
appThm
appThm
appThm
nil
"_485"
11
ref
var
222
def
160
ref
nil
cons
223
def
cons
"_482"
11
ref
var
224
def
190
ref
nil
cons
225
def
cons
"_483"
2
ref
var
226
def
188
ref
nil
cons
227
def
cons
nil
cons
228
def
cons
cons
nil
cons
cons
nil
"_484"
12
ref
var
229
def
214
remove
nil
cons
cons
nil
cons
nil
cons
cons
180
ref
nil
45
ref
"_482"
1
ref
var
varTerm
nil
cons
cons
"c"
2
ref
var
230
def
226
ref
varTerm
nil
cons
cons
7
ref
"_484"
4
ref
var
varTerm
nil
cons
cons
"y"
1
ref
var
231
def
"_485"
1
ref
var
varTerm
nil
cons
cons
nil
cons
cons
cons
cons
nil
cons
cons
231
ref
40
ref
26
ref
185
ref
0
ref
2
ref
0
ref
1
ref
0
ref
1
ref
10
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
232
def
230
ref
varTerm
233
def
appTerm
133
ref
appTerm
231
ref
varTerm
234
def
appTerm
appTerm
appTerm
81
ref
76
ref
233
ref
appTerm
26
ref
133
ref
appTerm
235
def
appTerm
appTerm
76
ref
218
ref
233
ref
appTerm
appTerm
26
ref
234
ref
appTerm
236
def
appTerm
appTerm
appTerm
absTerm
237
def
234
ref
appTerm
238
def
betaConv
45
ref
41
ref
237
ref
appTerm
239
def
absTerm
240
def
133
ref
appTerm
241
def
betaConv
230
remove
41
ref
240
ref
appTerm
242
def
absTerm
243
def
233
ref
appTerm
244
def
betaConv
7
ref
8
ref
99
remove
constTerm
245
def
243
ref
appTerm
246
def
absTerm
247
def
26
ref
appTerm
248
def
betaConv
nil
72
ref
247
ref
appTerm
249
def
axiom
nil
74
ref
249
remove
nil
cons
cons
75
ref
248
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
34
ref
6
ref
247
remove
nil
cons
cons
131
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
246
remove
nil
cons
cons
75
ref
244
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
"A"
3
ref
cons
nil
cons
250
def
"P"
38
remove
var
251
def
243
remove
nil
cons
cons
"x"
2
ref
var
252
def
233
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
242
remove
nil
cons
cons
75
ref
241
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
202
ref
42
ref
240
remove
nil
cons
cons
45
ref
133
ref
nil
cons
cons
nil
cons
253
def
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
239
remove
nil
cons
cons
75
ref
238
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
202
ref
42
ref
237
remove
nil
cons
cons
45
ref
234
ref
nil
cons
cons
nil
cons
254
def
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
subst
255
def
subst
256
def
subst
subst
eqMp
sym
nil
74
ref
227
ref
cons
257
def
75
ref
19
ref
21
remove
190
ref
appTerm
appTerm
212
ref
appTerm
258
def
nil
cons
259
def
cons
nil
cons
cons
nil
cons
cons
260
def
92
ref
subst
260
remove
137
ref
subst
63
remove
nil
158
ref
223
ref
cons
nil
cons
261
def
nil
cons
cons
262
def
158
ref
37
ref
18
remove
constTerm
170
ref
appTerm
211
ref
163
ref
appTerm
appTerm
absTerm
263
def
159
ref
appTerm
264
def
betaConv
157
ref
14
ref
263
ref
appTerm
265
def
absTerm
266
def
166
ref
appTerm
267
def
betaConv
nil
41
ref
266
ref
appTerm
268
def
axiom
nil
74
ref
268
remove
nil
cons
cons
75
ref
267
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
202
ref
42
ref
266
remove
nil
cons
cons
204
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
265
remove
nil
cons
cons
75
ref
264
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
179
ref
177
ref
263
remove
nil
cons
cons
206
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
269
def
subst
appThm
212
ref
refl
appThm
nil
142
ref
212
ref
nil
cons
270
def
cons
nil
cons
nil
cons
cons
155
remove
subst
trans
sym
61
ref
eqMp
eqMp
nil
109
ref
227
ref
cons
271
def
110
ref
259
remove
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
nil
74
ref
216
ref
258
remove
appTerm
nil
cons
cons
75
ref
220
ref
162
remove
212
ref
appTerm
272
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
137
ref
subst
proveHyp
nil
74
ref
219
ref
nil
cons
273
def
cons
274
def
75
ref
272
remove
nil
cons
275
def
cons
nil
cons
cons
nil
cons
cons
276
def
92
ref
subst
276
remove
137
ref
subst
nil
142
ref
161
remove
nil
cons
277
def
cons
nil
cons
nil
cons
cons
142
ref
144
ref
211
ref
143
ref
appTerm
278
def
appTerm
absTerm
279
def
143
ref
appTerm
280
def
betaConv
nil
149
ref
279
ref
appTerm
281
def
axiom
nil
74
ref
281
remove
nil
cons
cons
75
ref
280
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
151
ref
152
ref
279
remove
nil
cons
cons
154
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
subst
eqMp
nil
109
ref
273
remove
cons
282
def
110
ref
275
remove
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
74
ref
209
ref
212
ref
appTerm
nil
cons
cons
75
ref
19
ref
212
remove
appTerm
283
def
170
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
137
ref
subst
proveHyp
283
remove
refl
269
remove
appThm
nil
142
ref
163
remove
nil
cons
cons
"m"
16
ref
var
284
def
277
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
40
ref
19
ref
211
remove
284
ref
varTerm
285
def
appTerm
appTerm
278
remove
appTerm
appTerm
19
remove
285
ref
appTerm
286
def
143
ref
appTerm
287
def
appTerm
absTerm
288
def
143
ref
appTerm
289
def
betaConv
284
ref
149
ref
288
ref
appTerm
290
def
absTerm
291
def
285
ref
appTerm
292
def
betaConv
nil
149
ref
291
ref
appTerm
293
def
axiom
nil
74
ref
293
remove
nil
cons
cons
75
ref
292
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
151
ref
152
ref
291
remove
nil
cons
cons
153
ref
285
ref
nil
cons
cons
nil
cons
294
def
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
290
remove
nil
cons
cons
75
ref
289
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
151
ref
152
ref
288
remove
nil
cons
cons
154
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
subst
nil
56
ref
182
ref
cons
nil
cons
nil
cons
cons
62
ref
subst
164
remove
assume
eqMp
trans
trans
sym
61
ref
eqMp
eqMp
eqMp
151
ref
152
ref
210
ref
nil
cons
cons
153
ref
270
remove
cons
nil
cons
cons
nil
cons
cons
40
ref
"Data.Bool.?"
const
295
def
5
remove
constTerm
296
def
43
ref
appTerm
297
def
appTerm
298
def
refl
7
ref
245
ref
75
ref
76
ref
41
ref
45
ref
76
ref
235
ref
appTerm
79
ref
appTerm
absTerm
appTerm
appTerm
79
ref
appTerm
absTerm
appTerm
absTerm
299
def
43
remove
appTerm
betaConv
appThm
nil
51
remove
296
ref
appTerm
299
remove
appTerm
axiom
52
remove
appThm
eqMp
300
def
sym
nil
251
ref
110
ref
76
ref
41
ref
45
ref
76
ref
134
remove
appTerm
301
def
115
ref
appTerm
absTerm
302
def
appTerm
303
def
appTerm
115
ref
appTerm
304
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
250
ref
35
ref
cons
305
def
54
ref
subst
subst
110
ref
nil
56
ref
304
remove
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
nil
74
ref
303
remove
nil
cons
306
def
cons
307
def
75
ref
115
ref
nil
cons
308
def
cons
nil
cons
309
def
cons
nil
cons
cons
310
def
92
ref
subst
310
ref
137
ref
subst
nil
74
ref
135
remove
cons
309
ref
cons
nil
cons
cons
130
ref
subst
302
ref
133
ref
appTerm
311
def
betaConv
nil
307
ref
75
ref
311
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
202
ref
42
ref
302
remove
nil
cons
cons
253
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
109
ref
306
remove
cons
312
def
110
ref
308
ref
cons
nil
cons
313
def
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
subst
proveHyp
nil
74
ref
295
remove
148
remove
constTerm
314
def
210
remove
appTerm
nil
cons
cons
75
ref
209
remove
170
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
nil
"p"
16
remove
var
315
def
170
remove
nil
cons
cons
284
ref
208
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
315
ref
76
ref
314
remove
142
ref
81
ref
287
remove
appTerm
144
remove
315
ref
varTerm
316
def
appTerm
appTerm
317
def
absTerm
318
def
appTerm
319
def
appTerm
320
def
286
remove
316
ref
appTerm
321
def
appTerm
322
def
absTerm
323
def
316
ref
appTerm
324
def
betaConv
284
ref
149
ref
323
ref
appTerm
325
def
absTerm
326
def
285
ref
appTerm
327
def
betaConv
nil
149
ref
284
ref
149
ref
142
ref
149
ref
315
ref
76
ref
317
ref
appTerm
321
ref
appTerm
absTerm
328
def
appTerm
329
def
absTerm
330
def
appTerm
331
def
absTerm
332
def
appTerm
333
def
axiom
nil
74
ref
333
ref
nil
cons
334
def
cons
335
def
75
ref
149
ref
326
ref
appTerm
nil
cons
336
def
cons
nil
cons
cons
nil
cons
cons
337
def
130
ref
subst
proveHyp
337
ref
92
ref
subst
337
remove
137
ref
subst
nil
152
ref
326
remove
nil
cons
cons
338
def
nil
cons
nil
cons
cons
151
ref
35
ref
cons
54
ref
subst
339
def
subst
284
remove
nil
56
ref
325
remove
nil
cons
340
def
cons
nil
cons
nil
cons
cons
62
ref
subst
nil
152
ref
323
remove
nil
cons
cons
341
def
nil
cons
nil
cons
cons
339
ref
subst
315
remove
nil
56
ref
322
remove
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
nil
74
ref
319
remove
nil
cons
342
def
cons
343
def
75
ref
321
ref
nil
cons
344
def
cons
nil
cons
345
def
cons
nil
cons
cons
346
def
92
ref
subst
346
remove
137
ref
subst
nil
335
ref
345
ref
cons
nil
cons
cons
347
def
130
ref
subst
nil
343
remove
75
ref
76
ref
333
remove
appTerm
321
remove
appTerm
348
def
nil
cons
349
def
cons
nil
cons
350
def
cons
nil
cons
cons
130
ref
subst
nil
152
ref
142
ref
76
ref
318
ref
143
ref
appTerm
351
def
appTerm
348
ref
appTerm
352
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
339
remove
subst
142
remove
nil
56
ref
352
remove
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
nil
74
ref
351
ref
nil
cons
353
def
cons
350
ref
cons
nil
cons
cons
354
def
92
ref
subst
354
remove
137
ref
subst
351
ref
betaConv
351
remove
assume
eqMp
nil
74
ref
317
remove
nil
cons
355
def
cons
356
def
350
remove
cons
nil
cons
cons
357
def
130
ref
subst
proveHyp
357
ref
92
ref
subst
357
remove
137
ref
subst
347
ref
92
ref
subst
347
remove
137
ref
subst
nil
356
remove
345
remove
cons
nil
cons
cons
130
ref
subst
328
ref
316
ref
appTerm
358
def
betaConv
330
ref
143
remove
appTerm
359
def
betaConv
332
ref
285
remove
appTerm
360
def
betaConv
nil
335
remove
75
ref
360
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
151
ref
152
ref
332
remove
nil
cons
cons
294
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
331
remove
nil
cons
cons
75
ref
359
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
151
ref
152
ref
330
remove
nil
cons
cons
154
remove
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
329
remove
nil
cons
cons
75
ref
358
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
151
ref
152
ref
328
remove
nil
cons
cons
153
ref
316
remove
nil
cons
cons
nil
cons
361
def
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
109
ref
334
remove
cons
362
def
110
ref
344
remove
cons
nil
cons
363
def
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
eqMp
nil
109
ref
355
remove
cons
110
ref
349
remove
cons
nil
cons
364
def
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
109
ref
353
remove
cons
364
ref
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
74
ref
149
remove
153
ref
76
ref
318
ref
153
remove
varTerm
appTerm
appTerm
348
ref
appTerm
absTerm
appTerm
nil
cons
cons
75
ref
320
remove
348
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
151
ref
152
remove
318
remove
nil
cons
cons
364
remove
cons
nil
cons
cons
nil
307
remove
75
ref
76
ref
297
ref
appTerm
365
def
115
ref
appTerm
nil
cons
366
def
cons
nil
cons
cons
nil
cons
cons
367
def
92
ref
subst
367
remove
137
ref
subst
nil
74
ref
297
remove
nil
cons
368
def
cons
369
def
309
remove
cons
nil
cons
cons
370
def
92
ref
subst
370
remove
137
ref
subst
310
remove
130
ref
subst
75
ref
76
ref
41
ref
45
ref
301
remove
79
ref
appTerm
absTerm
appTerm
appTerm
79
ref
appTerm
absTerm
371
def
115
ref
appTerm
372
def
betaConv
nil
369
remove
75
ref
245
ref
371
ref
appTerm
373
def
nil
cons
374
def
cons
nil
cons
cons
nil
cons
cons
375
def
130
ref
subst
300
remove
nil
74
ref
298
remove
373
ref
appTerm
nil
cons
cons
75
ref
365
remove
373
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
375
remove
nil
74
ref
40
ref
77
ref
appTerm
79
ref
appTerm
376
def
nil
cons
377
def
cons
75
ref
80
remove
nil
cons
378
def
cons
nil
cons
cons
nil
cons
cons
379
def
92
ref
subst
379
remove
137
ref
subst
76
ref
refl
380
def
376
remove
assume
381
def
appThm
87
remove
appThm
sym
nil
74
ref
106
ref
cons
382
def
75
ref
106
ref
cons
nil
cons
cons
nil
cons
cons
383
def
92
ref
subst
383
remove
137
ref
subst
107
remove
eqMp
nil
109
ref
106
ref
cons
111
remove
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
384
def
eqMp
385
def
eqMp
nil
109
ref
377
remove
cons
110
ref
378
ref
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
74
ref
374
remove
cons
75
ref
372
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
250
ref
251
ref
371
remove
nil
cons
cons
252
ref
308
remove
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
109
ref
368
remove
cons
313
remove
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
eqMp
nil
312
remove
110
ref
366
remove
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
eqMp
eqMp
nil
109
ref
342
remove
cons
363
remove
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
362
remove
110
ref
336
ref
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
eqMp
nil
74
ref
336
remove
cons
75
ref
327
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
151
ref
338
remove
294
remove
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
340
remove
cons
75
ref
324
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
151
remove
341
remove
361
remove
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
eqMp
nil
109
ref
182
remove
cons
110
ref
183
remove
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
74
ref
81
ref
156
remove
appTerm
176
remove
appTerm
nil
cons
cons
75
ref
57
remove
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
380
ref
215
ref
30
ref
68
ref
appTerm
betaConv
appThm
41
ref
refl
386
def
157
ref
14
ref
refl
387
def
158
ref
380
ref
30
ref
159
ref
appTerm
betaConv
appThm
30
ref
168
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
387
ref
15
ref
30
ref
28
ref
appTerm
betaConv
absThm
appThm
appThm
nil
"p"
12
ref
var
388
def
30
remove
nil
cons
cons
nil
cons
nil
cons
cons
388
ref
76
ref
81
ref
388
ref
varTerm
389
def
68
ref
appTerm
appTerm
41
ref
157
ref
14
ref
158
ref
76
ref
389
ref
159
ref
appTerm
appTerm
389
ref
168
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
14
ref
15
ref
389
ref
28
ref
appTerm
absTerm
appTerm
appTerm
absTerm
390
def
389
ref
appTerm
391
def
betaConv
nil
8
ref
0
ref
13
ref
3
ref
cons
opType
constTerm
390
ref
appTerm
392
def
axiom
nil
74
ref
392
remove
nil
cons
cons
75
ref
391
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
"A"
65
ref
cons
nil
cons
"P"
13
remove
var
390
remove
nil
cons
cons
"x"
12
remove
var
389
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
393
def
subst
eqMp
eqMp
eqMp
absThm
eqMp
nil
72
ref
32
remove
appTerm
thm
72
ref
refl
394
def
7
ref
387
ref
15
ref
386
ref
45
ref
112
ref
nil
15
ref
29
ref
nil
cons
cons
nil
cons
nil
cons
cons
45
ref
40
ref
"Data.List.member"
const
0
ref
1
ref
65
ref
cons
opType
constTerm
133
ref
appTerm
395
def
28
ref
appTerm
396
def
appTerm
"Set.member"
const
0
ref
1
ref
0
ref
"Set.set"
typeOp
10
remove
opType
397
def
3
ref
cons
opType
398
def
nil
cons
399
def
cons
opType
constTerm
400
def
133
ref
appTerm
401
def
"Data.List.toSet"
const
0
ref
11
ref
397
ref
nil
cons
402
def
cons
opType
403
def
constTerm
404
def
28
ref
appTerm
405
def
appTerm
406
def
appTerm
absTerm
407
def
133
ref
appTerm
408
def
betaConv
15
ref
41
ref
407
ref
appTerm
409
def
absTerm
410
def
28
ref
appTerm
411
def
betaConv
nil
14
ref
410
ref
appTerm
412
def
axiom
nil
74
ref
412
remove
nil
cons
cons
75
ref
411
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
179
ref
177
ref
410
remove
nil
cons
cons
205
ref
28
ref
nil
cons
cons
nil
cons
413
def
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
409
remove
nil
cons
cons
75
ref
408
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
202
ref
42
ref
407
remove
nil
cons
cons
253
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
414
def
subst
401
ref
refl
415
def
15
ref
37
ref
0
ref
397
ref
399
remove
cons
opType
constTerm
416
def
404
ref
29
ref
appTerm
appTerm
"Set.difference"
const
0
ref
397
ref
0
ref
397
ref
402
ref
cons
opType
nil
cons
417
def
cons
opType
418
def
constTerm
419
def
405
ref
appTerm
"Set.fromPredicate"
const
0
ref
4
ref
402
ref
cons
opType
constTerm
420
def
"v"
1
ref
var
421
def
296
ref
45
ref
81
ref
37
ref
0
ref
1
ref
33
ref
cons
opType
constTerm
422
def
421
ref
varTerm
appTerm
423
def
133
ref
appTerm
appTerm
424
def
218
ref
235
ref
appTerm
425
def
appTerm
absTerm
appTerm
absTerm
appTerm
426
def
appTerm
appTerm
absTerm
427
def
28
ref
appTerm
428
def
betaConv
429
def
416
ref
refl
430
def
404
ref
refl
431
def
140
ref
appThm
nil
416
ref
404
ref
68
ref
appTerm
432
def
appTerm
"Set.{}"
const
397
ref
constTerm
433
def
appTerm
axiom
434
def
trans
appThm
419
ref
refl
435
def
434
remove
appThm
426
ref
refl
436
def
appThm
nil
"s"
397
ref
var
437
def
426
ref
nil
cons
438
def
cons
nil
cons
nil
cons
cons
437
ref
416
ref
419
ref
433
ref
appTerm
437
ref
varTerm
439
def
appTerm
appTerm
433
ref
appTerm
absTerm
440
def
439
ref
appTerm
441
def
betaConv
nil
8
ref
0
ref
398
ref
3
ref
cons
opType
constTerm
442
def
440
ref
appTerm
443
def
axiom
nil
74
ref
443
remove
nil
cons
cons
75
ref
441
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
"A"
402
ref
cons
nil
cons
444
def
"P"
398
remove
var
445
def
440
remove
nil
cons
cons
"x"
397
ref
var
446
def
439
ref
nil
cons
cons
nil
cons
447
def
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
subst
trans
appThm
nil
446
ref
433
remove
nil
cons
cons
nil
cons
nil
cons
cons
444
ref
35
ref
cons
448
def
nil
56
ref
422
ref
133
ref
appTerm
133
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
138
remove
eqMp
449
def
subst
450
def
subst
trans
sym
61
ref
eqMp
nil
74
ref
416
ref
404
ref
69
ref
appTerm
appTerm
419
ref
432
remove
appTerm
426
ref
appTerm
appTerm
451
def
nil
cons
cons
75
ref
41
ref
157
ref
14
ref
158
ref
76
ref
416
ref
404
ref
160
ref
appTerm
appTerm
419
ref
404
ref
159
ref
appTerm
452
def
appTerm
426
ref
appTerm
453
def
appTerm
454
def
appTerm
416
ref
404
ref
169
ref
appTerm
appTerm
419
ref
404
ref
168
ref
appTerm
455
def
appTerm
426
remove
appTerm
456
def
appTerm
457
def
appTerm
458
def
absTerm
459
def
appTerm
460
def
absTerm
461
def
appTerm
462
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
137
ref
subst
proveHyp
nil
42
ref
461
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
157
ref
nil
56
ref
460
remove
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
nil
177
ref
459
remove
nil
cons
cons
nil
cons
nil
cons
cons
181
ref
subst
158
ref
nil
56
ref
458
remove
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
nil
74
ref
454
ref
nil
cons
463
def
cons
75
ref
457
remove
nil
cons
464
def
cons
nil
cons
cons
nil
cons
cons
465
def
92
ref
subst
465
remove
137
ref
subst
430
ref
431
remove
207
ref
appThm
appThm
456
remove
refl
466
def
appThm
sym
430
ref
nil
"f"
403
remove
var
404
remove
nil
cons
cons
"y"
11
ref
var
223
ref
cons
205
ref
225
ref
cons
"b"
2
ref
var
467
def
227
ref
cons
nil
cons
cons
cons
cons
nil
cons
cons
178
remove
"B"
402
remove
cons
nil
cons
cons
35
ref
cons
231
ref
37
ref
0
ref
"B"
varType
468
def
0
ref
468
ref
3
ref
cons
opType
469
def
nil
cons
470
def
cons
opType
constTerm
"f"
0
ref
1
ref
468
ref
nil
cons
471
def
cons
opType
472
def
var
473
def
varTerm
474
def
232
ref
467
ref
varTerm
475
def
appTerm
133
ref
appTerm
234
ref
appTerm
appTerm
appTerm
185
ref
0
ref
2
ref
0
ref
468
ref
0
ref
468
ref
471
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
475
ref
appTerm
474
ref
133
ref
appTerm
appTerm
474
ref
234
ref
appTerm
appTerm
appTerm
absTerm
476
def
234
ref
appTerm
477
def
betaConv
45
ref
41
ref
476
ref
appTerm
478
def
absTerm
479
def
133
ref
appTerm
480
def
betaConv
473
ref
41
ref
479
ref
appTerm
481
def
absTerm
482
def
474
ref
appTerm
483
def
betaConv
467
remove
8
ref
0
ref
0
ref
472
ref
3
ref
cons
opType
484
def
3
ref
cons
opType
constTerm
485
def
482
ref
appTerm
486
def
absTerm
487
def
475
ref
appTerm
488
def
betaConv
nil
245
ref
487
ref
appTerm
489
def
axiom
nil
74
ref
489
remove
nil
cons
cons
75
ref
488
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
250
ref
251
ref
487
remove
nil
cons
cons
252
ref
475
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
486
remove
nil
cons
cons
75
ref
483
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
"A"
472
ref
nil
cons
cons
nil
cons
490
def
"P"
484
remove
var
491
def
482
remove
nil
cons
cons
"x"
472
ref
var
492
def
474
ref
nil
cons
493
def
cons
nil
cons
494
def
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
481
remove
nil
cons
cons
75
ref
480
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
202
ref
42
ref
479
remove
nil
cons
cons
253
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
478
remove
nil
cons
cons
75
ref
477
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
202
ref
42
ref
476
remove
nil
cons
cons
254
remove
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
subst
subst
appThm
466
remove
appThm
sym
430
ref
185
ref
0
ref
2
ref
418
remove
nil
cons
cons
opType
constTerm
495
def
188
ref
appTerm
496
def
refl
262
remove
158
ref
416
ref
455
remove
appTerm
"Set.insert"
const
0
ref
1
ref
417
remove
cons
opType
constTerm
497
def
166
ref
appTerm
498
def
452
ref
appTerm
appTerm
absTerm
499
def
159
ref
appTerm
500
def
betaConv
157
ref
14
ref
499
ref
appTerm
501
def
absTerm
502
def
166
ref
appTerm
503
def
betaConv
nil
41
ref
502
ref
appTerm
504
def
axiom
nil
74
ref
504
remove
nil
cons
cons
75
ref
503
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
202
ref
42
ref
502
remove
nil
cons
cons
204
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
501
remove
nil
cons
cons
75
ref
500
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
179
ref
177
ref
499
remove
nil
cons
cons
206
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
505
def
subst
498
ref
refl
454
remove
assume
506
def
appThm
trans
appThm
506
remove
appThm
appThm
435
remove
505
remove
appThm
436
remove
appThm
nil
"t"
397
ref
var
507
def
438
remove
cons
508
def
437
ref
452
remove
nil
cons
cons
204
ref
cons
cons
nil
cons
cons
45
ref
416
ref
419
ref
497
remove
133
ref
appTerm
509
def
439
ref
appTerm
appTerm
507
ref
varTerm
510
def
appTerm
appTerm
495
ref
401
ref
510
ref
appTerm
511
def
appTerm
419
remove
439
ref
appTerm
510
ref
appTerm
512
def
appTerm
509
remove
512
ref
appTerm
appTerm
appTerm
absTerm
513
def
133
ref
appTerm
514
def
betaConv
507
ref
41
ref
513
ref
appTerm
515
def
absTerm
516
def
510
ref
appTerm
517
def
betaConv
437
ref
442
ref
516
ref
appTerm
518
def
absTerm
519
def
439
ref
appTerm
520
def
betaConv
nil
442
ref
519
ref
appTerm
521
def
axiom
nil
74
ref
521
remove
nil
cons
cons
75
ref
520
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
444
ref
445
ref
519
remove
nil
cons
cons
447
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
518
remove
nil
cons
cons
75
ref
517
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
444
ref
445
ref
516
remove
nil
cons
cons
446
ref
510
ref
nil
cons
cons
nil
cons
522
def
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
515
remove
nil
cons
cons
75
ref
514
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
202
ref
42
ref
513
remove
nil
cons
cons
253
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
subst
495
ref
refl
523
def
112
ref
400
remove
166
ref
appTerm
refl
420
ref
refl
524
def
421
ref
296
ref
refl
525
def
45
ref
424
ref
refl
526
def
45
ref
425
remove
absTerm
527
def
133
ref
appTerm
betaConv
528
def
appThm
absThm
appThm
absThm
appThm
529
def
appThm
appThm
527
ref
166
ref
appTerm
betaConv
appThm
nil
7
ref
527
remove
nil
cons
cons
530
def
204
ref
cons
nil
cons
cons
45
ref
40
ref
401
ref
420
ref
421
ref
296
ref
231
remove
81
ref
423
remove
234
remove
appTerm
appTerm
236
remove
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
235
ref
appTerm
absTerm
531
def
133
ref
appTerm
532
def
betaConv
7
ref
41
ref
531
ref
appTerm
533
def
absTerm
534
def
26
ref
appTerm
535
def
betaConv
nil
72
ref
534
ref
appTerm
536
def
axiom
nil
74
ref
536
remove
nil
cons
cons
75
ref
535
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
34
ref
6
ref
534
remove
nil
cons
cons
131
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
533
remove
nil
cons
cons
75
ref
532
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
202
ref
42
ref
531
remove
nil
cons
cons
253
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
537
def
subst
eqMp
appThm
453
ref
refl
538
def
appThm
498
remove
453
ref
appTerm
539
def
refl
540
def
appThm
trans
trans
appThm
sym
nil
74
ref
40
ref
188
ref
appTerm
541
def
"Data.Bool.F"
const
2
ref
constTerm
542
def
appTerm
543
def
nil
cons
544
def
cons
75
ref
416
ref
496
remove
539
ref
appTerm
453
ref
appTerm
appTerm
495
ref
219
remove
appTerm
453
ref
appTerm
539
ref
appTerm
appTerm
nil
cons
545
def
cons
nil
cons
546
def
cons
nil
cons
cons
547
def
92
ref
subst
547
remove
137
ref
subst
40
ref
"_16102"
2
ref
var
548
def
416
ref
495
ref
548
remove
varTerm
549
def
appTerm
539
ref
appTerm
453
ref
appTerm
appTerm
495
ref
218
ref
549
remove
appTerm
appTerm
453
ref
appTerm
539
ref
appTerm
appTerm
absTerm
550
def
188
ref
appTerm
551
def
appTerm
refl
552
def
550
ref
542
ref
appTerm
betaConv
appThm
112
ref
551
remove
betaConv
appThm
553
def
416
ref
495
ref
542
ref
appTerm
539
ref
appTerm
453
ref
appTerm
appTerm
495
ref
218
ref
542
ref
appTerm
554
def
appTerm
453
ref
appTerm
539
ref
appTerm
appTerm
refl
appThm
trans
550
remove
refl
555
def
543
remove
assume
appThm
eqMp
sym
430
ref
nil
"t2"
397
ref
var
556
def
453
ref
nil
cons
557
def
cons
"t1"
397
remove
var
558
def
539
ref
nil
cons
559
def
cons
nil
cons
cons
nil
cons
cons
560
def
448
ref
"t2"
1
ref
var
561
def
422
ref
232
ref
542
ref
appTerm
"t1"
1
ref
var
562
def
varTerm
563
def
appTerm
561
ref
varTerm
564
def
appTerm
appTerm
564
ref
appTerm
absTerm
565
def
564
ref
appTerm
566
def
betaConv
562
ref
41
ref
565
ref
appTerm
567
def
absTerm
568
def
563
ref
appTerm
569
def
betaConv
nil
41
ref
568
ref
appTerm
570
def
axiom
nil
74
ref
570
remove
nil
cons
cons
75
ref
569
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
202
ref
42
ref
568
remove
nil
cons
cons
45
ref
563
ref
nil
cons
cons
nil
cons
571
def
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
567
remove
nil
cons
cons
75
ref
566
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
202
ref
42
ref
565
remove
nil
cons
cons
45
ref
564
ref
nil
cons
cons
nil
cons
572
def
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
573
def
subst
574
def
subst
appThm
523
ref
nil
40
ref
554
remove
appTerm
46
ref
appTerm
axiom
appThm
538
ref
appThm
540
ref
appThm
nil
556
remove
559
ref
cons
558
remove
557
ref
cons
nil
cons
cons
nil
cons
cons
575
def
448
remove
561
remove
422
remove
232
remove
46
ref
appTerm
563
ref
appTerm
564
ref
appTerm
appTerm
563
ref
appTerm
absTerm
576
def
564
remove
appTerm
577
def
betaConv
562
remove
41
ref
576
ref
appTerm
578
def
absTerm
579
def
563
remove
appTerm
580
def
betaConv
nil
41
ref
579
ref
appTerm
581
def
axiom
nil
74
ref
581
remove
nil
cons
cons
75
ref
580
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
202
ref
42
ref
579
remove
nil
cons
cons
571
remove
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
578
remove
nil
cons
cons
75
ref
577
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
202
ref
42
ref
576
remove
nil
cons
cons
572
remove
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
582
def
subst
583
def
subst
trans
appThm
nil
446
ref
557
remove
cons
nil
cons
nil
cons
cons
450
ref
subst
trans
sym
61
ref
eqMp
eqMp
eqMp
nil
109
ref
544
ref
cons
110
ref
545
ref
cons
nil
cons
584
def
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
nil
74
ref
541
remove
46
ref
appTerm
585
def
nil
cons
586
def
cons
546
remove
cons
nil
cons
cons
587
def
92
ref
subst
587
remove
137
ref
subst
552
remove
"_16100"
2
ref
var
588
def
416
ref
495
ref
588
remove
varTerm
589
def
appTerm
539
ref
appTerm
453
ref
appTerm
appTerm
495
ref
218
ref
589
remove
appTerm
appTerm
453
ref
appTerm
539
ref
appTerm
appTerm
absTerm
46
ref
appTerm
betaConv
appThm
553
remove
416
remove
495
ref
46
ref
appTerm
539
ref
appTerm
453
ref
appTerm
appTerm
495
remove
218
ref
46
ref
appTerm
590
def
appTerm
453
remove
appTerm
539
remove
appTerm
appTerm
refl
appThm
trans
555
remove
585
remove
assume
appThm
eqMp
sym
430
remove
560
remove
583
remove
subst
appThm
523
remove
nil
40
ref
590
remove
appTerm
542
ref
appTerm
axiom
appThm
538
remove
appThm
540
remove
appThm
575
remove
574
remove
subst
trans
appThm
nil
446
remove
559
remove
cons
nil
cons
nil
cons
cons
450
remove
subst
trans
sym
61
ref
eqMp
eqMp
eqMp
nil
109
ref
586
remove
cons
591
def
584
remove
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
56
ref
"Data.Bool.\\/"
const
39
remove
constTerm
592
def
60
remove
appTerm
59
remove
542
ref
appTerm
appTerm
absTerm
593
def
188
ref
appTerm
594
def
betaConv
nil
245
ref
593
ref
appTerm
595
def
axiom
nil
74
ref
595
remove
nil
cons
cons
75
ref
594
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
250
ref
251
ref
593
remove
nil
cons
cons
252
ref
227
ref
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
591
remove
110
ref
544
ref
cons
"R"
2
ref
var
596
def
545
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
74
ref
76
ref
115
ref
appTerm
597
def
596
remove
varTerm
598
def
appTerm
599
def
nil
cons
cons
75
ref
598
ref
nil
cons
600
def
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
nil
74
ref
76
ref
113
ref
appTerm
601
def
598
ref
appTerm
nil
cons
cons
75
ref
76
ref
599
remove
appTerm
598
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
"r"
2
ref
var
602
def
76
ref
601
ref
602
ref
varTerm
603
def
appTerm
appTerm
604
def
76
ref
597
remove
603
ref
appTerm
appTerm
603
ref
appTerm
appTerm
absTerm
605
def
598
remove
appTerm
606
def
betaConv
40
ref
592
ref
113
ref
appTerm
607
def
115
ref
appTerm
608
def
appTerm
refl
75
ref
245
ref
602
ref
604
remove
76
ref
76
ref
79
ref
appTerm
609
def
603
ref
appTerm
610
def
appTerm
603
ref
appTerm
611
def
appTerm
absTerm
appTerm
absTerm
115
ref
appTerm
betaConv
appThm
100
ref
607
remove
appTerm
refl
74
ref
75
ref
245
ref
602
ref
76
ref
78
ref
603
ref
appTerm
appTerm
611
remove
appTerm
absTerm
appTerm
absTerm
absTerm
612
def
113
ref
appTerm
betaConv
appThm
nil
89
remove
592
remove
appTerm
612
remove
appTerm
axiom
122
ref
appThm
eqMp
118
ref
appThm
eqMp
608
remove
assume
eqMp
nil
74
ref
245
ref
605
ref
appTerm
nil
cons
cons
75
ref
606
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
250
ref
251
ref
605
remove
nil
cons
cons
252
ref
600
remove
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
eqMp
eqMp
subst
proveHyp
proveHyp
proveHyp
eqMp
eqMp
eqMp
eqMp
nil
109
ref
463
remove
cons
110
ref
464
remove
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
74
ref
81
ref
451
remove
appTerm
462
remove
appTerm
nil
cons
cons
75
ref
14
ref
427
ref
appTerm
613
def
nil
cons
614
def
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
380
ref
215
ref
427
ref
68
ref
appTerm
betaConv
appThm
386
ref
157
ref
387
ref
158
ref
380
ref
427
ref
159
ref
appTerm
betaConv
appThm
427
ref
168
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
387
ref
15
ref
429
remove
absThm
appThm
appThm
nil
388
ref
427
remove
nil
cons
615
def
cons
nil
cons
nil
cons
cons
393
ref
subst
eqMp
eqMp
616
def
nil
74
ref
614
ref
cons
75
ref
428
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
179
ref
177
ref
615
remove
cons
413
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
617
def
appThm
nil
508
remove
437
ref
405
remove
nil
cons
cons
nil
cons
618
def
cons
nil
cons
cons
45
ref
40
ref
401
ref
512
remove
appTerm
appTerm
81
ref
401
remove
439
ref
appTerm
appTerm
218
ref
511
remove
appTerm
appTerm
appTerm
absTerm
619
def
133
ref
appTerm
620
def
betaConv
507
ref
41
ref
619
ref
appTerm
621
def
absTerm
622
def
510
remove
appTerm
623
def
betaConv
437
remove
442
ref
622
ref
appTerm
624
def
absTerm
625
def
439
remove
appTerm
626
def
betaConv
nil
442
remove
625
ref
appTerm
627
def
axiom
nil
74
ref
627
remove
nil
cons
cons
75
ref
626
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
444
ref
445
ref
625
remove
nil
cons
cons
447
remove
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
624
remove
nil
cons
cons
75
ref
623
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
444
remove
445
remove
622
remove
nil
cons
cons
522
remove
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
621
remove
nil
cons
cons
75
ref
620
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
202
ref
42
ref
619
remove
nil
cons
cons
253
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
628
def
subst
81
ref
406
ref
appTerm
629
def
refl
630
def
218
ref
refl
631
def
112
ref
415
ref
529
remove
appThm
appThm
528
remove
appThm
nil
530
remove
nil
cons
nil
cons
cons
537
ref
subst
eqMp
appThm
nil
56
ref
235
ref
nil
cons
632
def
cons
nil
cons
nil
cons
cons
56
ref
40
ref
218
ref
218
ref
58
ref
appTerm
appTerm
appTerm
58
ref
appTerm
absTerm
633
def
58
ref
appTerm
634
def
betaConv
nil
245
ref
633
ref
appTerm
635
def
axiom
nil
74
ref
635
remove
nil
cons
cons
75
ref
634
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
250
ref
251
ref
633
remove
nil
cons
cons
252
ref
58
ref
nil
cons
cons
nil
cons
636
def
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
637
def
subst
trans
appThm
trans
trans
trans
appThm
215
ref
414
remove
appThm
235
ref
refl
638
def
appThm
appThm
nil
252
ref
629
ref
235
ref
appTerm
639
def
nil
cons
cons
nil
cons
nil
cons
cons
305
remove
449
ref
subst
640
def
subst
trans
absThm
appThm
nil
56
ref
46
ref
nil
cons
cons
nil
cons
nil
cons
cons
641
def
56
ref
40
ref
41
ref
45
ref
58
ref
absTerm
appTerm
appTerm
58
ref
appTerm
absTerm
642
def
58
remove
appTerm
643
def
betaConv
nil
245
ref
642
ref
appTerm
644
def
axiom
nil
74
ref
644
remove
nil
cons
cons
75
ref
643
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
250
ref
251
ref
642
remove
nil
cons
cons
636
remove
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
645
def
subst
trans
absThm
appThm
641
ref
180
ref
645
ref
subst
subst
646
def
trans
absThm
appThm
641
remove
36
remove
645
remove
subst
subst
647
def
trans
sym
61
ref
eqMp
nil
72
ref
7
ref
14
ref
15
ref
41
ref
45
ref
40
ref
395
remove
29
remove
appTerm
appTerm
81
ref
396
remove
appTerm
235
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
thm
nil
6
ref
7
ref
14
ref
"l1"
11
ref
var
648
def
14
ref
"l2"
11
ref
var
649
def
66
ref
27
ref
"Data.List.@"
const
186
remove
constTerm
650
def
648
ref
varTerm
651
def
appTerm
649
ref
varTerm
652
def
appTerm
appTerm
appTerm
650
ref
27
ref
651
ref
appTerm
appTerm
27
ref
652
ref
appTerm
653
def
appTerm
appTerm
absTerm
appTerm
absTerm
654
def
appTerm
655
def
absTerm
656
def
nil
cons
cons
nil
cons
nil
cons
cons
55
ref
subst
7
ref
nil
56
ref
655
remove
nil
cons
657
def
cons
nil
cons
nil
cons
cons
62
ref
subst
387
ref
649
ref
66
ref
refl
658
def
27
ref
refl
659
def
nil
15
ref
652
ref
nil
cons
660
def
cons
nil
cons
nil
cons
cons
661
def
15
ref
66
ref
650
ref
68
ref
appTerm
662
def
28
ref
appTerm
appTerm
28
ref
appTerm
absTerm
663
def
28
ref
appTerm
664
def
betaConv
nil
14
ref
663
ref
appTerm
665
def
axiom
nil
74
ref
665
remove
nil
cons
cons
75
ref
664
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
179
ref
177
ref
663
remove
nil
cons
cons
413
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
666
def
subst
appThm
appThm
650
ref
refl
667
def
140
ref
appThm
653
ref
refl
668
def
appThm
nil
15
ref
653
ref
nil
cons
669
def
cons
670
def
nil
cons
nil
cons
cons
666
remove
subst
trans
appThm
nil
205
ref
669
remove
cons
nil
cons
nil
cons
cons
180
ref
449
ref
subst
671
def
subst
trans
absThm
appThm
646
ref
trans
sym
61
ref
eqMp
nil
74
ref
14
ref
649
ref
66
ref
27
ref
662
remove
652
ref
appTerm
appTerm
appTerm
650
ref
69
remove
appTerm
653
ref
appTerm
appTerm
absTerm
appTerm
672
def
nil
cons
cons
75
ref
41
ref
157
ref
14
ref
158
ref
76
ref
14
ref
649
ref
66
ref
27
ref
650
ref
159
ref
appTerm
673
def
652
ref
appTerm
674
def
appTerm
appTerm
650
ref
160
ref
appTerm
653
ref
appTerm
675
def
appTerm
absTerm
676
def
appTerm
677
def
appTerm
14
ref
649
ref
66
ref
27
remove
650
ref
168
ref
appTerm
678
def
652
ref
appTerm
appTerm
appTerm
650
ref
169
remove
appTerm
653
ref
appTerm
appTerm
679
def
absTerm
680
def
appTerm
681
def
appTerm
682
def
absTerm
683
def
appTerm
684
def
absTerm
685
def
appTerm
686
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
137
ref
subst
proveHyp
nil
42
ref
685
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
157
ref
nil
56
ref
684
remove
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
nil
177
ref
683
remove
nil
cons
cons
nil
cons
nil
cons
cons
181
ref
subst
158
ref
nil
56
ref
682
remove
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
nil
74
ref
677
remove
nil
cons
687
def
cons
688
def
75
ref
681
remove
nil
cons
689
def
cons
nil
cons
cons
nil
cons
cons
690
def
92
ref
subst
690
remove
137
ref
subst
nil
177
ref
680
remove
nil
cons
cons
nil
cons
nil
cons
cons
181
ref
subst
649
remove
nil
56
ref
679
remove
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
658
remove
659
remove
661
remove
158
ref
66
ref
678
remove
28
ref
appTerm
appTerm
167
ref
673
remove
28
ref
appTerm
appTerm
appTerm
absTerm
691
def
159
ref
appTerm
692
def
betaConv
157
ref
14
ref
691
ref
appTerm
693
def
absTerm
694
def
166
ref
appTerm
695
def
betaConv
15
ref
41
ref
694
ref
appTerm
696
def
absTerm
697
def
28
ref
appTerm
698
def
betaConv
nil
14
ref
697
ref
appTerm
699
def
axiom
nil
74
ref
699
remove
nil
cons
cons
75
ref
698
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
179
ref
177
ref
697
remove
nil
cons
cons
413
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
696
remove
nil
cons
cons
75
ref
695
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
202
ref
42
ref
694
remove
nil
cons
cons
204
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
693
remove
nil
cons
cons
75
ref
692
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
179
ref
177
ref
691
remove
nil
cons
cons
206
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
700
def
subst
appThm
nil
158
ref
674
remove
nil
cons
cons
nil
cons
nil
cons
cons
207
ref
subst
189
ref
refl
167
ref
refl
676
ref
652
remove
appTerm
701
def
betaConv
nil
688
remove
75
ref
701
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
179
ref
177
ref
676
remove
nil
cons
cons
205
ref
660
remove
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
702
def
appThm
appThm
702
remove
appThm
trans
trans
appThm
667
ref
207
ref
appThm
668
ref
appThm
appThm
sym
112
ref
"_16082"
11
ref
var
703
def
66
ref
703
remove
varTerm
appTerm
650
ref
191
remove
appTerm
653
ref
appTerm
704
def
appTerm
absTerm
705
def
189
remove
167
ref
675
ref
appTerm
706
def
appTerm
675
ref
appTerm
appTerm
betaConv
appThm
215
ref
217
remove
705
ref
706
ref
appTerm
betaConv
appThm
appThm
221
remove
705
ref
675
ref
appTerm
betaConv
appThm
appThm
appThm
nil
222
remove
675
ref
nil
cons
707
def
cons
224
remove
706
ref
nil
cons
708
def
cons
228
remove
cons
cons
nil
cons
cons
nil
229
remove
705
remove
nil
cons
cons
nil
cons
nil
cons
cons
256
remove
subst
subst
eqMp
sym
nil
257
remove
75
ref
66
ref
706
remove
appTerm
709
def
704
ref
appTerm
710
def
nil
cons
711
def
cons
nil
cons
cons
nil
cons
cons
712
def
92
ref
subst
712
remove
137
ref
subst
40
ref
"_16084"
2
ref
var
713
def
709
ref
650
ref
187
ref
713
remove
varTerm
appTerm
190
ref
appTerm
160
ref
appTerm
appTerm
653
ref
appTerm
appTerm
absTerm
714
def
188
ref
appTerm
715
def
appTerm
refl
714
ref
46
ref
appTerm
betaConv
appThm
112
ref
715
remove
betaConv
appThm
709
ref
650
ref
187
ref
46
ref
appTerm
716
def
190
ref
appTerm
160
ref
appTerm
appTerm
653
ref
appTerm
appTerm
refl
appThm
trans
714
remove
refl
nil
56
ref
227
remove
cons
nil
cons
nil
cons
cons
62
ref
subst
188
ref
assume
eqMp
appThm
eqMp
sym
709
remove
refl
667
ref
nil
"t2"
11
ref
var
717
def
223
remove
cons
"t1"
11
ref
var
718
def
225
remove
cons
nil
cons
cons
nil
cons
cons
719
def
180
ref
582
remove
subst
720
def
subst
appThm
668
ref
appThm
nil
670
remove
261
remove
cons
nil
cons
cons
700
remove
subst
trans
appThm
nil
205
ref
708
remove
cons
nil
cons
nil
cons
cons
671
ref
subst
trans
sym
61
ref
eqMp
eqMp
eqMp
nil
271
ref
110
ref
711
remove
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
nil
74
ref
216
remove
710
remove
appTerm
nil
cons
cons
75
ref
220
remove
66
remove
675
remove
appTerm
721
def
704
remove
appTerm
722
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
137
ref
subst
proveHyp
nil
274
ref
75
ref
722
remove
nil
cons
723
def
cons
nil
cons
cons
nil
cons
cons
724
def
92
ref
subst
724
remove
137
ref
subst
40
ref
"_16086"
2
ref
var
725
def
721
ref
650
ref
187
ref
725
remove
varTerm
appTerm
190
ref
appTerm
160
ref
appTerm
appTerm
653
ref
appTerm
appTerm
absTerm
726
def
188
remove
appTerm
727
def
appTerm
refl
726
ref
542
ref
appTerm
betaConv
appThm
112
ref
727
remove
betaConv
appThm
721
ref
650
remove
187
ref
542
ref
appTerm
728
def
190
remove
appTerm
160
remove
appTerm
appTerm
653
remove
appTerm
appTerm
refl
appThm
trans
726
remove
refl
nil
274
remove
75
ref
544
remove
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
nil
271
remove
nil
cons
nil
cons
cons
nil
74
ref
218
ref
113
ref
appTerm
729
def
nil
cons
730
def
cons
75
ref
40
ref
113
ref
appTerm
542
ref
appTerm
nil
cons
731
def
cons
nil
cons
cons
nil
cons
cons
732
def
92
ref
subst
732
remove
137
ref
subst
nil
74
ref
113
ref
nil
cons
733
def
cons
75
ref
542
ref
nil
cons
734
def
cons
nil
cons
cons
nil
cons
cons
385
remove
nil
74
ref
378
ref
cons
75
ref
609
ref
77
ref
appTerm
nil
cons
735
def
cons
nil
cons
cons
nil
cons
cons
137
ref
subst
proveHyp
609
remove
refl
381
remove
appThm
sym
384
remove
eqMp
eqMp
nil
382
remove
75
ref
104
ref
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
nil
109
ref
378
remove
cons
110
ref
735
remove
cons
nil
cons
cons
nil
cons
cons
736
def
112
ref
116
remove
126
ref
appTerm
betaConv
126
remove
113
ref
appTerm
betaConv
118
remove
appThm
125
remove
115
remove
appTerm
betaConv
trans
trans
appThm
127
remove
appThm
123
remove
128
remove
appThm
eqMp
sym
61
ref
eqMp
subst
eqMp
130
ref
736
remove
124
ref
subst
eqMp
deductAntisym
deductAntisym
subst
40
ref
729
ref
appTerm
refl
74
ref
78
ref
542
ref
appTerm
absTerm
737
def
113
ref
appTerm
betaConv
appThm
nil
100
remove
218
ref
appTerm
737
remove
appTerm
axiom
122
remove
appThm
eqMp
729
remove
assume
eqMp
nil
74
ref
601
remove
542
ref
appTerm
nil
cons
cons
75
ref
76
ref
542
ref
appTerm
113
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
137
ref
subst
proveHyp
nil
74
ref
734
ref
cons
75
ref
733
ref
cons
nil
cons
cons
nil
cons
cons
738
def
92
ref
subst
738
remove
137
ref
subst
74
ref
77
ref
absTerm
739
def
113
remove
appTerm
740
def
betaConv
nil
40
ref
542
ref
appTerm
245
ref
739
ref
appTerm
741
def
appTerm
axiom
542
ref
assume
eqMp
nil
74
ref
741
remove
nil
cons
cons
75
ref
740
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
250
ref
251
ref
739
remove
nil
cons
cons
252
ref
733
ref
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
eqMp
nil
109
ref
734
remove
cons
110
ref
733
remove
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
109
ref
730
remove
cons
110
ref
731
remove
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
742
def
subst
eqMp
appThm
eqMp
sym
721
remove
refl
667
remove
719
remove
180
remove
573
remove
subst
743
def
subst
appThm
668
remove
appThm
appThm
nil
205
remove
707
remove
cons
nil
cons
nil
cons
cons
671
remove
subst
trans
sym
61
ref
eqMp
eqMp
eqMp
nil
282
remove
110
ref
723
remove
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
nil
109
ref
687
remove
cons
110
ref
689
remove
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
74
ref
81
ref
672
remove
appTerm
686
remove
appTerm
nil
cons
cons
75
ref
657
remove
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
380
ref
215
ref
654
ref
68
ref
appTerm
betaConv
appThm
386
ref
157
ref
387
ref
158
ref
380
ref
654
ref
159
ref
appTerm
betaConv
appThm
654
ref
168
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
387
ref
648
remove
654
ref
651
remove
appTerm
betaConv
absThm
appThm
appThm
nil
388
ref
654
remove
nil
cons
cons
nil
cons
nil
cons
cons
393
ref
subst
eqMp
eqMp
eqMp
absThm
eqMp
nil
72
ref
656
remove
appTerm
thm
nil
"P"
0
ref
469
ref
3
ref
cons
opType
744
def
var
"p"
469
ref
var
745
def
485
ref
473
ref
14
ref
15
ref
37
ref
0
ref
9
remove
471
ref
opType
746
def
0
ref
746
ref
3
ref
cons
opType
747
def
nil
cons
cons
opType
constTerm
748
def
22
remove
0
ref
469
ref
0
ref
746
ref
746
ref
nil
cons
749
def
cons
opType
nil
cons
750
def
cons
opType
constTerm
745
ref
varTerm
751
def
appTerm
752
def
"Data.List.map"
const
0
ref
472
ref
0
ref
11
remove
749
ref
cons
opType
nil
cons
cons
opType
constTerm
474
ref
appTerm
753
def
28
ref
appTerm
appTerm
appTerm
753
ref
25
ref
"Function.o"
const
754
def
0
ref
469
ref
0
ref
472
ref
33
remove
cons
opType
nil
cons
cons
opType
constTerm
751
ref
appTerm
474
ref
appTerm
755
def
appTerm
756
def
28
ref
appTerm
appTerm
appTerm
absTerm
757
def
appTerm
758
def
absTerm
759
def
appTerm
760
def
absTerm
761
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
470
remove
cons
nil
cons
35
ref
cons
54
ref
subst
subst
745
remove
nil
56
ref
760
remove
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
nil
491
ref
759
remove
nil
cons
cons
nil
cons
nil
cons
cons
490
ref
35
ref
cons
54
ref
subst
subst
473
ref
nil
56
ref
758
remove
nil
cons
762
def
cons
nil
cons
nil
cons
cons
62
ref
subst
748
ref
refl
763
def
752
ref
refl
764
def
473
ref
748
ref
753
ref
68
ref
appTerm
765
def
appTerm
67
remove
746
ref
constTerm
766
def
appTerm
absTerm
767
def
474
ref
appTerm
768
def
betaConv
nil
485
ref
767
ref
appTerm
769
def
axiom
nil
74
ref
769
remove
nil
cons
cons
75
ref
768
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
490
ref
491
ref
767
remove
nil
cons
cons
494
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
770
def
appThm
"A"
471
ref
cons
nil
cons
35
ref
cons
771
def
140
ref
subst
trans
appThm
753
ref
refl
772
def
nil
7
ref
755
remove
nil
cons
cons
nil
cons
nil
cons
cons
773
def
140
remove
subst
appThm
770
remove
trans
appThm
nil
"x"
746
ref
var
774
def
766
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
749
remove
cons
nil
cons
35
ref
cons
775
def
449
remove
subst
776
def
subst
trans
sym
61
ref
eqMp
nil
74
ref
748
ref
752
ref
765
remove
appTerm
appTerm
753
ref
756
ref
68
ref
appTerm
appTerm
appTerm
777
def
nil
cons
cons
75
ref
41
ref
157
ref
14
ref
158
ref
76
ref
748
ref
752
ref
753
ref
159
ref
appTerm
778
def
appTerm
appTerm
753
ref
756
ref
159
ref
appTerm
779
def
appTerm
780
def
appTerm
781
def
appTerm
748
ref
752
remove
753
ref
168
ref
appTerm
782
def
appTerm
appTerm
753
ref
756
remove
168
ref
appTerm
appTerm
appTerm
783
def
appTerm
784
def
absTerm
785
def
appTerm
786
def
absTerm
787
def
appTerm
788
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
137
ref
subst
proveHyp
nil
42
ref
787
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
remove
subst
157
ref
nil
56
ref
786
remove
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
nil
177
ref
785
remove
nil
cons
cons
nil
cons
nil
cons
cons
181
remove
subst
158
ref
nil
56
ref
784
remove
nil
cons
cons
nil
cons
nil
cons
cons
62
ref
subst
nil
74
ref
781
ref
nil
cons
789
def
cons
75
ref
783
remove
nil
cons
790
def
cons
nil
cons
cons
nil
cons
cons
791
def
92
ref
subst
791
remove
137
ref
subst
763
remove
764
remove
158
ref
748
ref
782
remove
appTerm
165
remove
0
ref
468
ref
750
ref
cons
opType
constTerm
474
ref
166
ref
appTerm
792
def
appTerm
793
def
778
ref
appTerm
appTerm
absTerm
794
def
159
ref
appTerm
795
def
betaConv
157
ref
14
ref
794
ref
appTerm
796
def
absTerm
797
def
166
remove
appTerm
798
def
betaConv
473
remove
41
ref
797
ref
appTerm
799
def
absTerm
800
def
474
remove
appTerm
801
def
betaConv
nil
485
ref
800
ref
appTerm
802
def
axiom
nil
74
ref
802
remove
nil
cons
cons
75
ref
801
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
490
ref
491
ref
800
remove
nil
cons
cons
494
remove
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
799
remove
nil
cons
cons
75
ref
798
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
202
ref
42
ref
797
remove
nil
cons
cons
204
remove
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
796
remove
nil
cons
cons
75
ref
795
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
179
ref
177
ref
794
remove
nil
cons
cons
206
remove
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
803
def
appThm
nil
"t"
746
ref
var
778
remove
nil
cons
cons
"h"
468
ref
var
792
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
771
remove
207
ref
subst
subst
185
remove
0
ref
2
ref
0
ref
746
ref
750
remove
cons
opType
nil
cons
cons
opType
constTerm
751
ref
792
remove
appTerm
804
def
appTerm
805
def
refl
793
ref
refl
781
remove
assume
806
def
appThm
appThm
806
remove
appThm
trans
trans
appThm
772
ref
773
remove
207
remove
subst
187
ref
refl
nil
203
remove
"g"
472
ref
var
807
def
493
remove
cons
"f"
469
remove
var
751
remove
nil
cons
cons
nil
cons
cons
cons
nil
cons
cons
"B"
471
remove
cons
201
remove
"C"
3
ref
cons
nil
cons
cons
cons
35
remove
cons
45
ref
37
remove
0
ref
"C"
varType
808
def
0
ref
808
ref
3
ref
cons
opType
nil
cons
cons
opType
constTerm
754
remove
0
ref
0
ref
468
remove
808
remove
nil
cons
809
def
cons
opType
810
def
0
ref
472
remove
0
ref
1
remove
809
remove
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
"f"
810
ref
var
811
def
varTerm
812
def
appTerm
807
ref
varTerm
813
def
appTerm
133
ref
appTerm
appTerm
812
ref
813
ref
133
ref
appTerm
appTerm
appTerm
absTerm
814
def
133
ref
appTerm
815
def
betaConv
807
remove
41
ref
814
ref
appTerm
816
def
absTerm
817
def
813
ref
appTerm
818
def
betaConv
811
remove
485
remove
817
ref
appTerm
819
def
absTerm
820
def
812
ref
appTerm
821
def
betaConv
nil
8
ref
0
ref
0
ref
810
ref
3
ref
cons
opType
822
def
3
ref
cons
opType
constTerm
820
ref
appTerm
823
def
axiom
nil
74
ref
823
remove
nil
cons
cons
75
ref
821
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
"A"
810
ref
nil
cons
cons
nil
cons
"P"
822
remove
var
820
remove
nil
cons
cons
"x"
810
remove
var
812
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
819
remove
nil
cons
cons
75
ref
818
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
490
remove
491
remove
817
remove
nil
cons
cons
492
remove
813
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
816
remove
nil
cons
cons
75
ref
815
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
202
remove
42
remove
814
remove
nil
cons
cons
253
remove
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
subst
subst
appThm
167
remove
779
ref
appTerm
824
def
refl
appThm
779
ref
refl
appThm
trans
appThm
appThm
sym
112
ref
"_16088"
746
ref
var
825
def
748
ref
825
remove
varTerm
appTerm
753
ref
187
ref
804
ref
appTerm
824
ref
appTerm
779
ref
appTerm
appTerm
826
def
appTerm
absTerm
827
def
805
remove
793
remove
780
ref
appTerm
828
def
appTerm
780
ref
appTerm
appTerm
betaConv
appThm
215
ref
76
ref
804
ref
appTerm
829
def
refl
827
ref
828
ref
appTerm
betaConv
appThm
appThm
76
ref
218
ref
804
ref
appTerm
830
def
appTerm
831
def
refl
827
ref
780
ref
appTerm
betaConv
appThm
appThm
appThm
nil
"_485"
746
ref
var
780
ref
nil
cons
832
def
cons
"_482"
746
remove
var
828
ref
nil
cons
833
def
cons
226
remove
804
ref
nil
cons
834
def
cons
nil
cons
cons
cons
nil
cons
cons
nil
"_484"
747
remove
var
827
remove
nil
cons
cons
nil
cons
nil
cons
cons
775
remove
255
remove
subst
subst
subst
eqMp
sym
nil
74
ref
834
ref
cons
75
ref
748
ref
828
remove
appTerm
835
def
826
ref
appTerm
836
def
nil
cons
837
def
cons
nil
cons
cons
nil
cons
cons
838
def
92
ref
subst
838
remove
137
ref
subst
40
ref
"_16090"
2
ref
var
839
def
835
ref
753
ref
187
ref
839
remove
varTerm
appTerm
824
ref
appTerm
779
ref
appTerm
appTerm
appTerm
absTerm
840
def
804
ref
appTerm
841
def
appTerm
refl
840
ref
46
remove
appTerm
betaConv
appThm
112
ref
841
remove
betaConv
appThm
835
ref
753
ref
716
remove
824
ref
appTerm
779
ref
appTerm
appTerm
appTerm
refl
appThm
trans
840
remove
refl
nil
56
ref
834
ref
cons
nil
cons
nil
cons
cons
62
ref
subst
804
ref
assume
eqMp
appThm
eqMp
sym
835
remove
refl
772
ref
nil
717
remove
779
ref
nil
cons
842
def
cons
718
remove
824
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
843
def
720
remove
subst
appThm
nil
158
ref
842
remove
cons
nil
cons
nil
cons
cons
803
remove
subst
trans
appThm
nil
774
ref
833
remove
cons
nil
cons
nil
cons
cons
776
ref
subst
trans
sym
61
ref
eqMp
eqMp
eqMp
nil
109
ref
834
remove
cons
844
def
110
ref
837
remove
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
nil
74
ref
829
remove
836
remove
appTerm
nil
cons
cons
75
ref
831
remove
748
remove
780
remove
appTerm
845
def
826
remove
appTerm
846
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
137
ref
subst
proveHyp
nil
74
ref
830
remove
nil
cons
847
def
cons
848
def
75
ref
846
remove
nil
cons
849
def
cons
nil
cons
cons
nil
cons
cons
850
def
92
remove
subst
850
remove
137
remove
subst
40
ref
"_16092"
2
ref
var
851
def
845
ref
753
ref
187
remove
851
remove
varTerm
appTerm
824
ref
appTerm
779
ref
appTerm
appTerm
appTerm
absTerm
852
def
804
ref
appTerm
853
def
appTerm
refl
852
ref
542
ref
appTerm
betaConv
appThm
112
ref
853
remove
betaConv
appThm
845
ref
753
remove
728
remove
824
remove
appTerm
779
remove
appTerm
appTerm
appTerm
refl
appThm
trans
852
remove
refl
nil
848
remove
75
ref
40
ref
804
remove
appTerm
542
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
nil
844
remove
nil
cons
nil
cons
cons
742
remove
subst
eqMp
appThm
eqMp
sym
845
remove
refl
772
remove
843
remove
743
remove
subst
appThm
appThm
nil
774
remove
832
remove
cons
nil
cons
nil
cons
cons
776
remove
subst
trans
sym
61
ref
eqMp
eqMp
eqMp
nil
109
ref
847
remove
cons
110
ref
849
remove
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
nil
109
remove
789
remove
cons
110
remove
790
remove
cons
nil
cons
cons
nil
cons
cons
124
remove
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
74
ref
81
ref
777
remove
appTerm
788
remove
appTerm
nil
cons
cons
75
ref
762
remove
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
380
ref
215
ref
757
ref
68
remove
appTerm
betaConv
appThm
386
ref
157
remove
387
ref
158
remove
380
ref
757
ref
159
remove
appTerm
betaConv
appThm
757
ref
168
remove
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
387
ref
15
ref
757
ref
28
ref
appTerm
betaConv
absThm
appThm
appThm
nil
388
remove
757
remove
nil
cons
cons
nil
cons
nil
cons
cons
393
remove
subst
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
8
remove
0
ref
744
remove
3
remove
cons
opType
constTerm
761
remove
appTerm
thm
394
ref
7
ref
394
ref
"q"
4
ref
var
854
def
387
ref
15
ref
112
ref
nil
15
ref
25
remove
854
ref
varTerm
855
def
appTerm
28
ref
appTerm
856
def
nil
cons
cons
nil
cons
nil
cons
cons
857
def
15
ref
40
ref
"Data.List.all"
const
0
remove
4
remove
65
remove
cons
opType
858
def
constTerm
859
def
26
ref
appTerm
860
def
28
ref
appTerm
appTerm
41
ref
45
ref
76
ref
406
ref
appTerm
861
def
235
ref
appTerm
absTerm
appTerm
appTerm
absTerm
862
def
28
ref
appTerm
863
def
betaConv
7
ref
14
ref
862
ref
appTerm
864
def
absTerm
865
def
26
ref
appTerm
866
def
betaConv
nil
72
ref
865
ref
appTerm
867
def
axiom
nil
74
ref
867
remove
nil
cons
cons
75
ref
866
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
34
ref
6
ref
865
remove
nil
cons
cons
131
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
864
remove
nil
cons
cons
75
ref
863
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
179
ref
177
ref
862
remove
nil
cons
cons
413
ref
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
868
def
subst
386
ref
45
ref
380
remove
415
ref
nil
7
ref
855
ref
nil
cons
cons
nil
cons
nil
cons
cons
617
remove
subst
appThm
nil
507
remove
420
remove
421
ref
296
ref
45
ref
424
remove
218
remove
855
remove
133
ref
appTerm
869
def
appTerm
870
def
appTerm
absTerm
appTerm
absTerm
appTerm
nil
cons
cons
618
remove
cons
nil
cons
cons
628
remove
subst
630
ref
631
remove
112
ref
415
remove
524
remove
421
remove
525
ref
45
ref
526
remove
45
ref
870
remove
absTerm
871
def
133
ref
appTerm
betaConv
872
def
appThm
absThm
appThm
absThm
appThm
appThm
appThm
872
remove
appThm
nil
7
ref
871
remove
nil
cons
cons
nil
cons
nil
cons
cons
537
remove
subst
eqMp
appThm
nil
56
ref
869
ref
nil
cons
873
def
cons
nil
cons
nil
cons
cons
637
remove
subst
trans
appThm
trans
trans
874
def
appThm
638
ref
appThm
absThm
appThm
trans
appThm
nil
7
ref
45
ref
76
ref
869
ref
appTerm
235
ref
appTerm
absTerm
875
def
nil
cons
cons
nil
cons
nil
cons
cons
868
remove
subst
386
remove
45
ref
861
remove
refl
875
ref
133
ref
appTerm
betaConv
appThm
nil
602
ref
632
ref
cons
75
ref
873
ref
cons
74
ref
406
remove
nil
cons
876
def
cons
nil
cons
cons
cons
nil
cons
cons
602
remove
40
ref
78
remove
610
remove
appTerm
appTerm
76
ref
83
remove
appTerm
603
ref
appTerm
appTerm
absTerm
877
def
603
ref
appTerm
878
def
betaConv
75
ref
245
ref
877
ref
appTerm
879
def
absTerm
880
def
79
remove
appTerm
881
def
betaConv
74
ref
245
ref
880
ref
appTerm
882
def
absTerm
883
def
77
remove
appTerm
884
def
betaConv
nil
245
ref
883
ref
appTerm
885
def
axiom
nil
74
ref
885
remove
nil
cons
cons
75
ref
884
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
250
ref
251
ref
883
remove
nil
cons
cons
252
ref
104
remove
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
882
remove
nil
cons
cons
75
ref
881
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
250
ref
251
ref
880
remove
nil
cons
cons
252
ref
106
remove
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
879
remove
nil
cons
cons
75
ref
878
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
250
ref
251
ref
877
remove
nil
cons
cons
252
ref
603
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
subst
trans
absThm
appThm
trans
appThm
nil
252
ref
41
remove
45
ref
76
remove
629
remove
869
ref
appTerm
886
def
appTerm
235
ref
appTerm
absTerm
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
640
ref
subst
trans
absThm
appThm
646
ref
trans
absThm
appThm
647
ref
trans
absThm
appThm
647
ref
trans
sym
61
ref
eqMp
nil
72
ref
7
ref
72
ref
854
ref
14
ref
15
ref
40
ref
860
remove
856
ref
appTerm
appTerm
859
remove
875
remove
appTerm
28
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
thm
394
ref
7
ref
394
remove
854
ref
387
remove
15
ref
112
remove
857
remove
15
ref
40
ref
"Data.List.any"
const
858
remove
constTerm
887
def
26
ref
appTerm
888
def
28
ref
appTerm
appTerm
296
ref
45
ref
639
remove
absTerm
appTerm
appTerm
absTerm
889
def
28
ref
appTerm
890
def
betaConv
7
ref
14
ref
889
ref
appTerm
891
def
absTerm
892
def
26
remove
appTerm
893
def
betaConv
nil
72
ref
892
ref
appTerm
894
def
axiom
nil
74
ref
894
remove
nil
cons
cons
75
ref
893
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
34
remove
6
ref
892
remove
nil
cons
cons
131
remove
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
891
remove
nil
cons
cons
75
ref
890
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
179
remove
177
remove
889
remove
nil
cons
cons
413
remove
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
895
def
subst
525
ref
45
ref
215
remove
874
remove
appThm
638
remove
appThm
absThm
appThm
trans
appThm
nil
7
ref
45
ref
81
ref
869
remove
appTerm
235
ref
appTerm
absTerm
896
def
nil
cons
cons
nil
cons
nil
cons
cons
895
remove
subst
525
remove
45
ref
630
remove
896
ref
133
remove
appTerm
betaConv
appThm
nil
"t3"
2
ref
var
897
def
632
remove
cons
"t2"
2
ref
var
898
def
873
remove
cons
"t1"
2
remove
var
899
def
876
remove
cons
nil
cons
cons
cons
nil
cons
cons
897
ref
40
ref
81
ref
899
ref
varTerm
900
def
appTerm
901
def
81
ref
898
ref
varTerm
902
def
appTerm
897
ref
varTerm
903
def
appTerm
appTerm
904
def
appTerm
81
ref
901
remove
902
ref
appTerm
appTerm
903
ref
appTerm
905
def
appTerm
906
def
absTerm
907
def
903
ref
appTerm
908
def
betaConv
898
ref
245
ref
907
ref
appTerm
909
def
absTerm
910
def
902
ref
appTerm
911
def
betaConv
899
ref
245
ref
910
ref
appTerm
912
def
absTerm
913
def
900
ref
appTerm
914
def
betaConv
245
ref
refl
915
def
899
ref
915
ref
898
ref
915
remove
897
ref
906
remove
assume
sym
40
ref
905
remove
appTerm
904
remove
appTerm
916
def
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
absThm
appThm
nil
245
ref
899
remove
245
ref
898
remove
245
ref
897
remove
916
remove
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
74
ref
245
remove
913
ref
appTerm
nil
cons
cons
75
ref
914
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
250
ref
251
ref
913
remove
nil
cons
cons
252
ref
900
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
ref
912
remove
nil
cons
cons
75
ref
911
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
ref
subst
proveHyp
250
ref
251
ref
910
remove
nil
cons
cons
252
ref
902
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
ref
subst
eqMp
eqMp
nil
74
remove
909
remove
nil
cons
cons
75
remove
908
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
130
remove
subst
proveHyp
250
remove
251
remove
907
remove
nil
cons
cons
252
ref
903
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
139
remove
subst
eqMp
eqMp
subst
trans
absThm
appThm
trans
appThm
nil
252
remove
296
remove
45
remove
81
remove
886
remove
appTerm
235
remove
appTerm
absTerm
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
640
remove
subst
trans
absThm
appThm
646
remove
trans
absThm
appThm
647
ref
trans
absThm
appThm
647
remove
trans
sym
61
remove
eqMp
nil
72
ref
7
ref
72
ref
854
remove
14
remove
15
remove
40
remove
888
remove
856
remove
appTerm
appTerm
887
remove
896
remove
appTerm
28
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
thm
nil
6
remove
7
ref
613
remove
absTerm
917
def
nil
cons
cons
nil
cons
nil
cons
cons
55
remove
subst
7
remove
nil
56
remove
614
remove
cons
nil
cons
nil
cons
cons
62
remove
subst
616
remove
eqMp
absThm
eqMp
nil
72
remove
917
remove
appTerm
thm