6
version
"Data.Bool.!"
const
0
def
"->"
typeOp
1
def
1
ref
1
ref
"A"
varType
2
def
1
ref
"B"
varType
3
def
"C"
varType
4
def
nil
cons
5
def
cons
opType
nil
cons
cons
opType
6
def
"bool"
typeOp
nil
opType
7
def
nil
cons
8
def
cons
opType
9
def
8
ref
cons
opType
constTerm
10
def
refl
11
def
"f"
6
ref
var
12
def
"="
const
13
def
1
ref
"Data.List.list"
typeOp
14
def
5
remove
opType
15
def
1
ref
15
ref
8
ref
cons
opType
nil
cons
cons
opType
constTerm
16
def
refl
17
def
nil
"l"
14
ref
3
ref
nil
cons
18
def
opType
19
def
var
20
def
"Data.List.[]"
const
21
def
19
ref
constTerm
22
def
nil
cons
cons
nil
cons
nil
cons
cons
20
ref
16
ref
"Data.List.zipWith"
"zipwith"
1
ref
6
ref
1
ref
14
ref
2
ref
nil
cons
23
def
opType
24
def
1
ref
19
ref
15
ref
nil
cons
25
def
cons
opType
26
def
nil
cons
27
def
cons
opType
nil
cons
cons
opType
28
def
var
29
def
nil
cons
cons
nil
cons
29
ref
"Data.Bool./\\"
const
1
ref
7
ref
1
ref
7
ref
8
ref
cons
opType
30
def
nil
cons
cons
opType
31
def
constTerm
32
def
10
ref
12
ref
0
ref
1
ref
1
ref
19
ref
8
ref
cons
opType
33
def
8
ref
cons
opType
constTerm
34
def
20
ref
16
ref
29
ref
varTerm
35
def
12
ref
varTerm
36
def
appTerm
37
def
21
ref
24
ref
constTerm
38
def
appTerm
20
ref
varTerm
39
def
appTerm
appTerm
21
remove
15
ref
constTerm
40
def
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
10
ref
12
ref
0
ref
1
ref
1
ref
2
ref
8
ref
cons
opType
41
def
8
ref
cons
opType
42
def
constTerm
43
def
"h"
2
ref
var
44
def
0
ref
1
ref
1
ref
24
ref
8
ref
cons
opType
45
def
8
ref
cons
opType
constTerm
46
def
"t"
24
ref
var
47
def
34
ref
20
ref
16
ref
37
ref
"Data.List.::"
const
48
def
1
ref
2
ref
1
ref
24
ref
24
ref
nil
cons
49
def
cons
opType
50
def
nil
cons
cons
opType
constTerm
51
def
44
ref
varTerm
52
def
appTerm
47
ref
varTerm
53
def
appTerm
54
def
appTerm
39
ref
appTerm
appTerm
48
ref
1
ref
4
remove
1
ref
15
ref
25
ref
cons
opType
nil
cons
cons
opType
constTerm
55
def
36
ref
52
ref
appTerm
"Data.List.head"
const
56
def
1
ref
19
ref
18
ref
cons
opType
constTerm
39
ref
appTerm
appTerm
appTerm
57
def
37
remove
53
ref
appTerm
"Data.List.tail"
const
58
def
1
ref
19
ref
19
ref
nil
cons
59
def
cons
opType
60
def
constTerm
39
ref
appTerm
61
def
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
62
def
refl
63
def
13
ref
1
ref
28
ref
1
ref
28
ref
8
ref
cons
opType
64
def
nil
cons
cons
opType
constTerm
65
def
35
ref
appTerm
66
def
"select"
const
67
def
1
ref
64
ref
28
ref
nil
cons
68
def
cons
opType
constTerm
69
def
62
ref
appTerm
appTerm
assume
sym
appThm
62
ref
35
ref
appTerm
betaConv
70
def
trans
"A"
68
remove
cons
nil
cons
71
def
nil
nil
cons
72
def
cons
nil
13
ref
1
ref
42
ref
1
ref
42
ref
8
ref
cons
opType
nil
cons
cons
opType
constTerm
73
def
"Data.Bool.?"
const
74
def
42
ref
constTerm
75
def
appTerm
76
def
"p"
41
ref
var
77
def
77
ref
varTerm
78
def
67
ref
1
ref
41
ref
23
ref
cons
opType
constTerm
78
ref
appTerm
appTerm
absTerm
appTerm
axiom
subst
63
remove
appThm
"p"
64
ref
var
79
def
79
remove
varTerm
80
def
69
remove
80
remove
appTerm
appTerm
absTerm
62
ref
appTerm
betaConv
trans
74
ref
1
ref
1
ref
1
ref
24
ref
1
ref
6
ref
27
remove
cons
opType
81
def
nil
cons
82
def
cons
opType
83
def
8
ref
cons
opType
84
def
8
ref
cons
opType
85
def
constTerm
86
def
refl
"fn"
83
ref
var
87
def
32
ref
13
ref
1
ref
81
ref
1
ref
81
ref
8
ref
cons
opType
nil
cons
cons
opType
constTerm
88
def
87
remove
varTerm
89
def
38
ref
appTerm
appTerm
12
ref
20
ref
40
ref
absTerm
90
def
absTerm
91
def
appTerm
appTerm
refl
43
ref
refl
92
def
44
ref
46
ref
refl
93
def
47
ref
88
ref
89
ref
54
ref
appTerm
appTerm
refl
44
ref
47
ref
"_16259"
81
ref
var
94
def
12
ref
20
ref
57
ref
94
remove
varTerm
36
ref
appTerm
61
ref
appTerm
appTerm
absTerm
absTerm
absTerm
95
def
absTerm
96
def
absTerm
97
def
52
ref
appTerm
betaConv
53
ref
refl
98
def
appThm
96
remove
53
ref
appTerm
betaConv
trans
89
remove
53
ref
appTerm
99
def
refl
appThm
95
remove
99
remove
appTerm
betaConv
trans
appThm
absThm
appThm
absThm
appThm
appThm
absThm
appThm
nil
"f"
1
ref
2
ref
1
ref
24
ref
1
ref
81
ref
82
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
var
97
remove
nil
cons
cons
"b"
81
remove
var
91
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
"A"
23
ref
cons
100
def
"B"
82
remove
cons
nil
cons
cons
72
ref
cons
"f"
1
ref
2
ref
1
ref
24
ref
1
ref
3
ref
18
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
101
def
var
102
def
74
ref
1
ref
1
ref
1
ref
24
ref
18
ref
cons
opType
103
def
8
ref
cons
opType
8
ref
cons
opType
constTerm
"fn"
103
remove
var
104
def
32
ref
13
ref
1
ref
3
ref
1
ref
3
ref
8
ref
cons
opType
105
def
nil
cons
cons
opType
constTerm
106
def
104
remove
varTerm
107
def
38
ref
appTerm
appTerm
"b"
3
ref
var
108
def
varTerm
109
def
appTerm
appTerm
43
ref
44
ref
46
ref
47
ref
106
remove
107
ref
54
ref
appTerm
appTerm
102
remove
varTerm
110
def
52
ref
appTerm
53
ref
appTerm
107
remove
53
ref
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
111
def
110
ref
appTerm
112
def
betaConv
108
remove
0
ref
1
ref
1
ref
101
ref
8
ref
cons
opType
113
def
8
ref
cons
opType
constTerm
111
ref
appTerm
114
def
absTerm
115
def
109
ref
appTerm
116
def
betaConv
nil
0
ref
1
ref
105
ref
8
ref
cons
opType
constTerm
117
def
115
ref
appTerm
118
def
axiom
nil
"p"
7
ref
var
119
def
118
remove
nil
cons
cons
"q"
7
ref
var
120
def
116
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
13
ref
31
ref
constTerm
121
def
"Data.Bool.==>"
const
31
ref
constTerm
122
def
119
ref
varTerm
123
def
appTerm
120
ref
varTerm
124
def
appTerm
125
def
appTerm
refl
119
ref
120
ref
121
ref
32
ref
123
ref
appTerm
126
def
124
ref
appTerm
127
def
appTerm
128
def
123
ref
appTerm
absTerm
129
def
absTerm
130
def
123
ref
appTerm
betaConv
124
ref
refl
131
def
appThm
129
remove
124
ref
appTerm
betaConv
trans
appThm
nil
13
ref
1
ref
31
ref
1
ref
31
ref
8
ref
cons
opType
132
def
nil
cons
cons
opType
constTerm
133
def
122
ref
appTerm
130
remove
appTerm
axiom
123
ref
refl
134
def
appThm
131
ref
appThm
eqMp
135
def
sym
136
def
128
remove
refl
120
ref
13
ref
1
ref
132
ref
1
ref
132
remove
8
ref
cons
opType
nil
cons
cons
opType
constTerm
137
def
"f"
31
remove
var
138
def
138
ref
varTerm
139
def
123
ref
appTerm
124
ref
appTerm
absTerm
140
def
appTerm
138
ref
139
ref
"Data.Bool.T"
const
7
ref
constTerm
141
def
appTerm
141
ref
appTerm
absTerm
142
def
appTerm
absTerm
143
def
124
ref
appTerm
betaConv
appThm
13
ref
1
ref
30
ref
1
ref
30
ref
8
ref
cons
opType
144
def
nil
cons
cons
opType
constTerm
145
def
126
remove
appTerm
refl
119
ref
143
remove
absTerm
146
def
123
ref
appTerm
betaConv
appThm
nil
133
remove
32
ref
appTerm
146
ref
appTerm
axiom
147
def
134
remove
appThm
eqMp
131
ref
appThm
eqMp
148
def
sym
138
ref
139
ref
refl
nil
"t"
7
ref
var
149
def
123
ref
nil
cons
150
def
cons
nil
cons
nil
cons
cons
121
ref
149
ref
varTerm
151
def
appTerm
141
ref
appTerm
assume
sym
nil
141
ref
axiom
152
def
eqMp
151
ref
assume
152
ref
deductAntisym
deductAntisym
153
def
subst
123
ref
assume
154
def
eqMp
appThm
nil
149
ref
124
ref
nil
cons
155
def
cons
nil
cons
nil
cons
cons
153
ref
subst
124
ref
assume
eqMp
appThm
absThm
eqMp
156
def
nil
"P"
7
ref
var
157
def
150
remove
cons
"Q"
7
ref
var
158
def
155
remove
cons
nil
cons
cons
nil
cons
cons
121
ref
refl
159
def
138
ref
139
remove
157
ref
varTerm
160
def
appTerm
161
def
158
ref
varTerm
162
def
appTerm
absTerm
163
def
119
ref
120
ref
123
ref
absTerm
absTerm
164
def
appTerm
betaConv
164
ref
160
ref
appTerm
betaConv
162
ref
refl
165
def
appThm
120
ref
160
ref
absTerm
162
ref
appTerm
betaConv
trans
trans
appThm
142
ref
164
ref
appTerm
betaConv
164
ref
141
ref
appTerm
betaConv
141
ref
refl
166
def
appThm
120
ref
141
ref
absTerm
141
ref
appTerm
betaConv
trans
trans
appThm
121
ref
32
ref
160
ref
appTerm
167
def
162
ref
appTerm
168
def
appTerm
refl
120
ref
137
remove
138
remove
161
remove
124
ref
appTerm
absTerm
appTerm
142
ref
appTerm
absTerm
162
ref
appTerm
betaConv
appThm
145
remove
167
remove
appTerm
refl
146
remove
160
ref
appTerm
betaConv
appThm
147
remove
160
ref
refl
appThm
eqMp
165
ref
appThm
eqMp
168
remove
assume
eqMp
169
def
164
remove
refl
appThm
eqMp
sym
152
ref
eqMp
170
def
subst
171
def
deductAntisym
eqMp
135
remove
125
ref
assume
eqMp
sym
154
ref
eqMp
159
ref
140
remove
119
ref
120
ref
124
ref
absTerm
172
def
absTerm
173
def
appTerm
betaConv
173
ref
123
ref
appTerm
betaConv
131
remove
appThm
172
ref
124
ref
appTerm
betaConv
trans
trans
appThm
142
remove
173
ref
appTerm
betaConv
173
ref
141
ref
appTerm
betaConv
166
remove
appThm
172
ref
141
ref
appTerm
betaConv
trans
trans
174
def
appThm
148
remove
127
remove
assume
eqMp
173
ref
refl
175
def
appThm
eqMp
sym
152
ref
eqMp
176
def
proveHyp
deductAntisym
177
def
subst
proveHyp
"A"
18
ref
cons
nil
cons
178
def
"P"
105
remove
var
115
remove
nil
cons
cons
"x"
3
ref
var
109
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
119
ref
43
ref
"P"
41
ref
var
179
def
varTerm
180
def
appTerm
181
def
nil
cons
182
def
cons
120
ref
180
ref
"x"
2
ref
var
183
def
varTerm
184
def
appTerm
185
def
nil
cons
186
def
cons
nil
cons
cons
nil
cons
cons
187
def
136
ref
subst
187
remove
176
remove
156
remove
deductAntisym
188
def
subst
121
ref
185
ref
appTerm
refl
183
ref
141
ref
absTerm
189
def
184
ref
appTerm
betaConv
appThm
77
ref
13
ref
1
ref
41
ref
42
remove
nil
cons
cons
opType
constTerm
78
ref
appTerm
189
remove
appTerm
absTerm
190
def
180
ref
appTerm
betaConv
191
def
nil
73
remove
43
ref
appTerm
190
remove
appTerm
axiom
180
ref
refl
192
def
appThm
193
def
181
ref
assume
eqMp
eqMp
184
ref
refl
194
def
appThm
eqMp
sym
152
ref
eqMp
eqMp
nil
157
ref
182
remove
cons
158
ref
186
ref
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
deductAntisym
eqMp
195
def
subst
eqMp
eqMp
nil
119
ref
114
remove
nil
cons
cons
120
ref
112
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
proveHyp
"A"
101
ref
nil
cons
cons
nil
cons
"P"
113
remove
var
111
remove
nil
cons
cons
"x"
101
remove
var
110
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
195
ref
subst
eqMp
eqMp
subst
subst
eqMp
nil
119
ref
86
ref
"_16258"
83
ref
var
196
def
32
ref
88
ref
196
ref
varTerm
197
def
38
ref
appTerm
198
def
appTerm
91
ref
appTerm
199
def
appTerm
43
ref
44
ref
46
ref
47
ref
88
remove
197
ref
54
ref
appTerm
200
def
appTerm
12
ref
20
ref
57
ref
197
ref
53
ref
appTerm
36
ref
appTerm
201
def
61
ref
appTerm
appTerm
202
def
absTerm
203
def
absTerm
204
def
appTerm
absTerm
205
def
appTerm
206
def
absTerm
207
def
appTerm
208
def
appTerm
209
def
absTerm
210
def
appTerm
211
def
nil
cons
cons
120
ref
86
remove
196
ref
32
ref
10
ref
12
ref
34
ref
20
ref
16
ref
198
remove
36
ref
appTerm
212
def
39
ref
appTerm
appTerm
213
def
40
ref
appTerm
214
def
absTerm
215
def
appTerm
216
def
absTerm
217
def
appTerm
218
def
appTerm
10
ref
12
ref
43
ref
44
ref
46
ref
47
ref
34
ref
20
ref
16
ref
200
remove
36
ref
appTerm
219
def
39
ref
appTerm
appTerm
220
def
202
remove
appTerm
221
def
absTerm
222
def
appTerm
223
def
absTerm
224
def
appTerm
225
def
absTerm
226
def
appTerm
227
def
absTerm
228
def
appTerm
229
def
appTerm
230
def
absTerm
231
def
appTerm
232
def
nil
cons
233
def
cons
nil
cons
234
def
cons
nil
cons
cons
177
ref
subst
nil
"P"
84
remove
var
235
def
196
ref
122
ref
210
ref
197
ref
appTerm
236
def
appTerm
232
ref
appTerm
237
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
83
ref
nil
cons
cons
nil
cons
238
def
72
ref
cons
121
ref
181
remove
appTerm
refl
191
remove
appThm
193
remove
eqMp
sym
239
def
subst
240
def
subst
196
ref
nil
149
ref
237
remove
nil
cons
cons
nil
cons
nil
cons
cons
153
ref
subst
nil
119
ref
236
ref
nil
cons
241
def
cons
234
ref
cons
nil
cons
cons
242
def
136
ref
subst
242
remove
188
ref
subst
236
ref
betaConv
236
remove
assume
eqMp
nil
119
ref
209
remove
nil
cons
243
def
cons
234
remove
cons
nil
cons
cons
244
def
177
ref
subst
proveHyp
244
ref
136
ref
subst
244
remove
188
ref
subst
231
ref
197
ref
appTerm
245
def
betaConv
246
def
sym
nil
157
ref
199
ref
nil
cons
cons
158
ref
208
remove
nil
cons
247
def
cons
nil
cons
cons
nil
cons
cons
248
def
170
ref
subst
nil
"P"
9
remove
var
249
def
217
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
6
ref
nil
cons
cons
nil
cons
250
def
72
ref
cons
251
def
239
ref
subst
252
def
subst
12
ref
nil
149
ref
216
remove
nil
cons
cons
nil
cons
nil
cons
cons
153
ref
subst
nil
"P"
33
remove
var
253
def
215
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
59
ref
cons
nil
cons
254
def
72
ref
cons
255
def
239
ref
subst
256
def
subst
20
ref
nil
149
ref
214
remove
nil
cons
cons
nil
cons
nil
cons
cons
153
ref
subst
213
remove
refl
90
remove
39
ref
appTerm
betaConv
appThm
13
ref
1
ref
26
ref
1
ref
26
remove
8
ref
cons
opType
nil
cons
cons
opType
constTerm
257
def
212
ref
appTerm
refl
91
remove
36
ref
appTerm
betaConv
appThm
199
remove
assume
36
ref
refl
258
def
appThm
eqMp
39
ref
refl
259
def
appThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
proveHyp
nil
119
ref
218
remove
nil
cons
cons
120
ref
229
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
188
ref
subst
proveHyp
248
remove
159
remove
163
remove
173
ref
appTerm
betaConv
173
remove
160
remove
appTerm
betaConv
165
remove
appThm
172
remove
162
ref
appTerm
betaConv
trans
trans
appThm
174
remove
appThm
169
remove
175
remove
appThm
eqMp
sym
152
ref
eqMp
260
def
subst
nil
249
ref
228
remove
nil
cons
cons
nil
cons
nil
cons
cons
252
remove
subst
12
ref
nil
149
ref
227
remove
nil
cons
cons
nil
cons
nil
cons
cons
153
ref
subst
nil
179
ref
226
remove
nil
cons
cons
nil
cons
nil
cons
cons
239
ref
subst
44
ref
nil
149
ref
225
remove
nil
cons
cons
nil
cons
nil
cons
cons
153
ref
subst
nil
"P"
45
ref
var
261
def
224
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
49
remove
cons
nil
cons
262
def
72
ref
cons
263
def
239
ref
subst
264
def
subst
47
ref
nil
149
ref
223
remove
nil
cons
cons
nil
cons
nil
cons
cons
153
ref
subst
nil
253
ref
222
remove
nil
cons
cons
nil
cons
nil
cons
cons
256
ref
subst
20
ref
nil
149
ref
221
remove
nil
cons
cons
nil
cons
nil
cons
cons
153
ref
subst
220
remove
refl
203
remove
39
ref
appTerm
betaConv
appThm
257
remove
219
ref
appTerm
refl
204
remove
36
ref
appTerm
betaConv
appThm
205
ref
53
ref
appTerm
265
def
betaConv
207
ref
52
ref
appTerm
266
def
betaConv
nil
119
ref
247
remove
cons
120
ref
266
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
100
remove
nil
cons
267
def
179
ref
207
remove
nil
cons
cons
183
ref
52
ref
nil
cons
cons
nil
cons
268
def
cons
nil
cons
cons
195
ref
subst
eqMp
eqMp
nil
119
ref
206
remove
nil
cons
cons
120
ref
265
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
proveHyp
262
ref
261
ref
205
remove
nil
cons
cons
"x"
24
ref
var
53
ref
nil
cons
cons
nil
cons
269
def
cons
nil
cons
cons
195
ref
subst
eqMp
eqMp
258
ref
appThm
eqMp
259
ref
appThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
proveHyp
eqMp
eqMp
238
ref
235
ref
231
ref
nil
cons
cons
270
def
"x"
83
remove
var
271
def
197
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
121
ref
75
remove
180
ref
appTerm
272
def
appTerm
273
def
refl
77
remove
0
ref
144
remove
constTerm
274
def
120
ref
122
ref
43
ref
183
ref
122
ref
78
remove
184
ref
appTerm
appTerm
124
ref
appTerm
absTerm
appTerm
appTerm
124
ref
appTerm
absTerm
appTerm
absTerm
275
def
180
remove
appTerm
betaConv
appThm
nil
76
remove
275
remove
appTerm
axiom
192
remove
appThm
eqMp
276
def
sym
nil
"P"
30
remove
var
277
def
158
ref
122
ref
43
ref
183
ref
122
ref
185
remove
appTerm
278
def
162
ref
appTerm
absTerm
279
def
appTerm
280
def
appTerm
162
ref
appTerm
281
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
8
ref
cons
nil
cons
282
def
72
ref
cons
239
remove
subst
subst
158
ref
nil
149
ref
281
remove
nil
cons
cons
nil
cons
nil
cons
cons
153
ref
subst
nil
119
ref
280
remove
nil
cons
283
def
cons
284
def
120
ref
162
ref
nil
cons
285
def
cons
nil
cons
286
def
cons
nil
cons
cons
287
def
136
ref
subst
287
ref
188
ref
subst
nil
119
ref
186
remove
cons
286
ref
cons
nil
cons
cons
177
ref
subst
279
ref
184
ref
appTerm
288
def
betaConv
nil
284
ref
120
ref
288
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
267
ref
179
ref
279
remove
nil
cons
cons
183
ref
184
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
195
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
157
ref
283
remove
cons
289
def
158
ref
285
ref
cons
nil
cons
290
def
cons
nil
cons
cons
170
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
291
def
subst
proveHyp
eqMp
nil
157
ref
243
remove
cons
158
ref
233
ref
cons
nil
cons
292
def
cons
nil
cons
cons
170
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
157
ref
241
remove
cons
292
ref
cons
nil
cons
cons
170
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
119
ref
0
remove
85
remove
constTerm
293
def
271
ref
122
ref
210
ref
271
ref
varTerm
294
def
appTerm
appTerm
232
ref
appTerm
absTerm
appTerm
nil
cons
cons
120
ref
122
ref
211
remove
appTerm
232
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
proveHyp
238
ref
235
ref
210
remove
nil
cons
cons
292
remove
cons
nil
cons
cons
nil
284
remove
120
ref
122
ref
272
ref
appTerm
295
def
162
ref
appTerm
nil
cons
296
def
cons
nil
cons
cons
nil
cons
cons
297
def
136
ref
subst
297
remove
188
ref
subst
nil
119
ref
272
remove
nil
cons
298
def
cons
299
def
286
remove
cons
nil
cons
cons
300
def
136
ref
subst
300
remove
188
ref
subst
287
remove
177
ref
subst
120
ref
122
ref
43
ref
183
ref
278
remove
124
ref
appTerm
absTerm
appTerm
appTerm
124
ref
appTerm
absTerm
301
def
162
remove
appTerm
302
def
betaConv
nil
299
remove
120
ref
274
ref
301
ref
appTerm
303
def
nil
cons
304
def
cons
nil
cons
cons
nil
cons
cons
305
def
177
ref
subst
276
remove
nil
119
ref
273
remove
303
ref
appTerm
nil
cons
cons
120
ref
295
remove
303
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
proveHyp
305
remove
nil
119
ref
121
ref
123
remove
appTerm
124
remove
appTerm
306
def
nil
cons
307
def
cons
120
ref
125
remove
nil
cons
308
def
cons
nil
cons
cons
nil
cons
cons
309
def
136
ref
subst
309
remove
188
ref
subst
136
ref
188
ref
306
remove
assume
154
remove
eqMp
eqMp
171
remove
deductAntisym
eqMp
eqMp
nil
157
ref
307
remove
cons
158
ref
308
remove
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
119
ref
304
remove
cons
120
ref
302
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
proveHyp
282
ref
277
ref
301
remove
nil
cons
cons
"x"
7
remove
var
310
def
285
remove
cons
nil
cons
cons
nil
cons
cons
195
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
157
ref
298
remove
cons
290
remove
cons
nil
cons
cons
170
ref
subst
deductAntisym
eqMp
eqMp
nil
289
remove
158
ref
296
remove
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
deductAntisym
eqMp
311
def
subst
eqMp
eqMp
proveHyp
nil
119
ref
233
remove
cons
120
ref
74
remove
1
ref
64
ref
8
ref
cons
opType
constTerm
62
ref
appTerm
312
def
nil
cons
313
def
cons
nil
cons
314
def
cons
nil
cons
cons
177
ref
subst
nil
235
remove
196
ref
122
ref
245
ref
appTerm
312
ref
appTerm
315
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
240
remove
subst
196
remove
nil
149
ref
315
remove
nil
cons
cons
nil
cons
nil
cons
cons
153
ref
subst
nil
119
ref
245
ref
nil
cons
316
def
cons
314
ref
cons
nil
cons
cons
317
def
136
ref
subst
317
remove
188
ref
subst
246
remove
245
remove
assume
eqMp
nil
119
ref
230
ref
nil
cons
318
def
cons
314
ref
cons
nil
cons
cons
319
def
177
ref
subst
proveHyp
319
ref
136
ref
subst
319
remove
188
ref
subst
"_16255"
6
ref
var
320
def
"_16256"
24
ref
var
321
def
"_16257"
19
ref
var
322
def
197
remove
321
ref
varTerm
appTerm
323
def
320
remove
varTerm
appTerm
322
ref
varTerm
324
def
appTerm
absTerm
absTerm
absTerm
325
def
refl
nil
119
ref
65
remove
325
ref
appTerm
325
ref
appTerm
nil
cons
cons
314
ref
cons
nil
cons
cons
177
ref
subst
proveHyp
nil
29
remove
325
ref
nil
cons
cons
nil
cons
nil
cons
cons
nil
119
ref
66
remove
325
ref
appTerm
326
def
nil
cons
327
def
cons
314
remove
cons
nil
cons
cons
328
def
136
remove
subst
328
remove
188
remove
subst
70
remove
sym
32
remove
refl
11
ref
12
ref
34
ref
refl
329
def
20
ref
17
ref
326
remove
assume
258
remove
appThm
325
remove
36
ref
appTerm
betaConv
trans
330
def
38
ref
refl
appThm
321
remove
322
ref
323
remove
36
ref
appTerm
324
ref
appTerm
absTerm
absTerm
331
def
38
ref
appTerm
betaConv
trans
259
ref
appThm
322
ref
212
remove
324
ref
appTerm
absTerm
39
ref
appTerm
betaConv
trans
appThm
40
ref
refl
332
def
appThm
absThm
appThm
absThm
appThm
appThm
11
ref
12
ref
92
ref
44
ref
93
ref
47
ref
329
ref
20
ref
17
ref
330
ref
54
ref
refl
appThm
331
ref
54
ref
appTerm
betaConv
trans
259
remove
appThm
322
ref
219
remove
324
ref
appTerm
absTerm
39
ref
appTerm
betaConv
trans
appThm
57
ref
refl
330
remove
98
remove
appThm
331
remove
53
ref
appTerm
betaConv
trans
61
ref
refl
appThm
322
remove
201
remove
324
remove
appTerm
absTerm
61
ref
appTerm
betaConv
trans
appThm
appThm
absThm
appThm
absThm
appThm
absThm
appThm
absThm
appThm
appThm
sym
230
remove
assume
eqMp
eqMp
71
remove
"P"
64
remove
var
62
remove
nil
cons
cons
"x"
28
ref
var
35
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
291
remove
subst
proveHyp
eqMp
nil
157
ref
327
remove
cons
158
ref
313
remove
cons
nil
cons
333
def
cons
nil
cons
cons
170
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
157
ref
318
remove
cons
333
ref
cons
nil
cons
cons
170
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
157
ref
316
remove
cons
333
ref
cons
nil
cons
cons
170
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
119
ref
293
remove
271
remove
122
ref
231
remove
294
remove
appTerm
appTerm
312
ref
appTerm
absTerm
appTerm
nil
cons
cons
120
ref
122
ref
232
remove
appTerm
312
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
proveHyp
238
remove
270
remove
333
remove
cons
nil
cons
cons
311
remove
subst
eqMp
eqMp
proveHyp
eqMp
eqMp
defineConstList
334
def
pop
hdTl
pop
335
def
28
remove
constTerm
36
ref
appTerm
336
def
38
ref
appTerm
337
def
39
ref
appTerm
appTerm
40
ref
appTerm
absTerm
338
def
39
ref
appTerm
339
def
betaConv
12
ref
34
ref
338
ref
appTerm
340
def
absTerm
341
def
36
ref
appTerm
342
def
betaConv
334
ref
nil
157
remove
10
ref
341
ref
appTerm
nil
cons
343
def
cons
158
remove
10
ref
12
ref
43
ref
44
ref
46
ref
47
ref
34
ref
20
ref
16
ref
336
ref
54
ref
appTerm
39
ref
appTerm
appTerm
57
remove
336
ref
53
ref
appTerm
61
remove
appTerm
appTerm
appTerm
absTerm
344
def
appTerm
345
def
absTerm
346
def
appTerm
347
def
absTerm
348
def
appTerm
349
def
absTerm
350
def
appTerm
nil
cons
351
def
cons
nil
cons
cons
nil
cons
cons
352
def
170
remove
subst
proveHyp
nil
119
ref
343
remove
cons
120
ref
342
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
proveHyp
250
ref
249
ref
341
remove
nil
cons
cons
"x"
6
remove
var
36
ref
nil
cons
cons
nil
cons
353
def
cons
nil
cons
cons
195
ref
subst
eqMp
eqMp
nil
119
ref
340
remove
nil
cons
cons
120
ref
339
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
proveHyp
254
ref
253
ref
338
remove
nil
cons
cons
"x"
19
ref
var
39
ref
nil
cons
cons
nil
cons
354
def
cons
nil
cons
cons
195
ref
subst
eqMp
eqMp
subst
appThm
332
remove
appThm
nil
"x"
15
remove
var
355
def
40
ref
nil
cons
cons
nil
cons
nil
cons
cons
"A"
25
remove
cons
nil
cons
72
ref
cons
nil
149
ref
13
ref
1
ref
2
ref
41
remove
nil
cons
cons
opType
constTerm
356
def
184
ref
appTerm
184
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
153
ref
subst
194
remove
eqMp
subst
357
def
subst
trans
absThm
appThm
nil
149
ref
141
ref
nil
cons
cons
nil
cons
nil
cons
cons
358
def
251
remove
149
ref
121
ref
43
ref
183
ref
151
ref
absTerm
appTerm
appTerm
151
ref
appTerm
absTerm
359
def
151
ref
appTerm
360
def
betaConv
nil
274
ref
359
ref
appTerm
361
def
axiom
nil
119
ref
361
remove
nil
cons
cons
120
ref
360
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
proveHyp
282
ref
277
ref
359
remove
nil
cons
cons
310
remove
151
ref
nil
cons
cons
nil
cons
362
def
cons
nil
cons
cons
195
ref
subst
eqMp
eqMp
363
def
subst
subst
364
def
trans
sym
152
ref
eqMp
nil
10
ref
12
ref
16
ref
337
remove
22
ref
appTerm
appTerm
40
remove
appTerm
absTerm
appTerm
thm
nil
261
ref
"l1"
24
ref
var
365
def
34
ref
"l2"
19
ref
var
366
def
13
ref
1
ref
14
remove
"Data.Pair.*"
typeOp
367
def
2
ref
18
remove
cons
opType
368
def
nil
cons
369
def
opType
370
def
1
ref
370
ref
8
ref
cons
opType
nil
cons
cons
opType
constTerm
371
def
"Data.List.zip"
"_16262"
24
ref
var
372
def
"_16263"
19
ref
var
373
def
335
remove
1
ref
1
ref
2
ref
1
ref
3
ref
369
remove
cons
opType
nil
cons
cons
opType
374
def
1
ref
24
ref
1
ref
19
ref
370
ref
nil
cons
cons
opType
nil
cons
cons
opType
375
def
nil
cons
cons
opType
constTerm
"Data.Pair.,"
const
376
def
374
remove
constTerm
377
def
appTerm
378
def
372
ref
varTerm
379
def
appTerm
373
ref
varTerm
380
def
appTerm
381
def
absTerm
382
def
absTerm
383
def
defineConst
384
def
pop
375
remove
constTerm
385
def
365
remove
varTerm
386
def
appTerm
366
remove
varTerm
387
def
appTerm
appTerm
378
remove
386
remove
appTerm
387
remove
appTerm
appTerm
absTerm
appTerm
absTerm
388
def
nil
cons
cons
nil
cons
nil
cons
cons
264
remove
subst
372
remove
nil
149
ref
34
ref
373
ref
371
remove
385
remove
379
ref
appTerm
380
ref
appTerm
appTerm
381
remove
appTerm
389
def
absTerm
390
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
153
ref
subst
nil
253
ref
390
remove
nil
cons
cons
nil
cons
nil
cons
cons
256
remove
subst
373
remove
nil
149
ref
389
remove
nil
cons
cons
nil
cons
nil
cons
cons
153
remove
subst
384
remove
379
ref
refl
appThm
383
remove
379
remove
appTerm
betaConv
trans
380
ref
refl
appThm
382
remove
380
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
46
ref
388
remove
appTerm
thm
11
remove
12
ref
92
remove
"h1"
2
remove
var
391
def
117
ref
refl
"h2"
3
ref
var
392
def
93
remove
"t1"
24
ref
var
393
def
329
remove
"t2"
19
ref
var
394
def
122
ref
13
ref
1
ref
"Number.Natural.natural"
typeOp
nil
opType
395
def
1
ref
395
ref
8
ref
cons
opType
nil
cons
cons
opType
constTerm
"Data.List.length"
const
396
def
1
ref
24
ref
395
remove
nil
cons
397
def
cons
opType
constTerm
393
ref
varTerm
398
def
appTerm
appTerm
396
remove
1
ref
19
ref
397
remove
cons
opType
constTerm
394
ref
varTerm
399
def
appTerm
appTerm
400
def
appTerm
401
def
refl
17
remove
nil
20
remove
48
remove
1
ref
3
ref
60
remove
nil
cons
cons
opType
constTerm
402
def
392
ref
varTerm
403
def
appTerm
399
ref
appTerm
404
def
nil
cons
cons
47
ref
398
ref
nil
cons
cons
44
ref
391
ref
varTerm
405
def
nil
cons
cons
nil
cons
cons
cons
nil
cons
cons
344
ref
39
remove
appTerm
406
def
betaConv
346
ref
53
ref
appTerm
407
def
betaConv
348
ref
52
ref
appTerm
408
def
betaConv
350
ref
36
ref
appTerm
409
def
betaConv
334
remove
352
remove
260
remove
subst
proveHyp
nil
119
ref
351
remove
cons
120
ref
409
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
proveHyp
250
remove
249
remove
350
remove
nil
cons
cons
353
remove
cons
nil
cons
cons
195
ref
subst
eqMp
eqMp
nil
119
ref
349
remove
nil
cons
cons
120
ref
408
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
proveHyp
267
ref
179
ref
348
remove
nil
cons
cons
268
ref
cons
nil
cons
cons
195
ref
subst
eqMp
eqMp
nil
119
ref
347
remove
nil
cons
cons
120
ref
407
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
proveHyp
262
ref
261
ref
346
remove
nil
cons
cons
269
ref
cons
nil
cons
cons
195
ref
subst
eqMp
eqMp
nil
119
ref
345
remove
nil
cons
cons
120
ref
406
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
proveHyp
254
remove
253
remove
344
remove
nil
cons
cons
354
remove
cons
nil
cons
cons
195
ref
subst
eqMp
eqMp
subst
55
ref
refl
36
remove
405
ref
appTerm
410
def
refl
nil
"t"
19
ref
var
399
ref
nil
cons
cons
"h"
3
ref
var
403
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
411
def
178
remove
72
remove
cons
412
def
47
ref
356
remove
56
remove
1
ref
24
ref
23
remove
cons
opType
constTerm
54
ref
appTerm
appTerm
52
ref
appTerm
absTerm
413
def
53
ref
appTerm
414
def
betaConv
44
ref
46
ref
413
ref
appTerm
415
def
absTerm
416
def
52
ref
appTerm
417
def
betaConv
nil
43
ref
416
ref
appTerm
418
def
axiom
nil
119
ref
418
remove
nil
cons
cons
120
ref
417
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
proveHyp
267
ref
179
ref
416
remove
nil
cons
cons
268
ref
cons
nil
cons
cons
195
ref
subst
eqMp
eqMp
nil
119
ref
415
remove
nil
cons
cons
120
ref
414
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
proveHyp
262
ref
261
ref
413
remove
nil
cons
cons
269
ref
cons
nil
cons
cons
195
ref
subst
eqMp
eqMp
subst
subst
appThm
appThm
336
ref
398
ref
appTerm
419
def
refl
411
remove
412
ref
47
remove
13
ref
1
ref
24
ref
45
remove
nil
cons
cons
opType
constTerm
58
remove
50
remove
constTerm
54
remove
appTerm
appTerm
53
ref
appTerm
absTerm
420
def
53
remove
appTerm
421
def
betaConv
44
remove
46
ref
420
ref
appTerm
422
def
absTerm
423
def
52
remove
appTerm
424
def
betaConv
nil
43
ref
423
ref
appTerm
425
def
axiom
nil
119
ref
425
remove
nil
cons
cons
120
ref
424
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
proveHyp
267
remove
179
remove
423
remove
nil
cons
cons
268
remove
cons
nil
cons
cons
195
ref
subst
eqMp
eqMp
nil
119
ref
422
remove
nil
cons
cons
120
ref
421
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
ref
subst
proveHyp
262
remove
261
remove
420
remove
nil
cons
cons
269
remove
cons
nil
cons
cons
195
ref
subst
eqMp
eqMp
subst
subst
appThm
appThm
trans
appThm
55
remove
410
remove
403
remove
appTerm
appTerm
419
remove
399
remove
appTerm
appTerm
426
def
refl
appThm
nil
355
remove
426
ref
nil
cons
cons
nil
cons
nil
cons
cons
357
remove
subst
trans
appThm
nil
149
ref
400
remove
nil
cons
cons
nil
cons
nil
cons
cons
149
remove
121
remove
122
remove
151
ref
appTerm
141
ref
appTerm
appTerm
141
remove
appTerm
absTerm
427
def
151
remove
appTerm
428
def
betaConv
nil
274
remove
427
ref
appTerm
429
def
axiom
nil
119
remove
429
remove
nil
cons
cons
120
remove
428
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
177
remove
subst
proveHyp
282
remove
277
remove
427
remove
nil
cons
cons
362
remove
cons
nil
cons
cons
195
remove
subst
eqMp
eqMp
subst
trans
absThm
appThm
358
ref
255
remove
363
ref
subst
subst
trans
absThm
appThm
358
ref
263
remove
363
ref
subst
subst
trans
absThm
appThm
358
ref
412
remove
363
ref
subst
subst
trans
absThm
appThm
358
remove
363
remove
subst
trans
absThm
appThm
364
remove
trans
sym
152
remove
eqMp
nil
10
remove
12
remove
43
ref
391
remove
117
ref
392
remove
46
ref
393
remove
34
ref
394
remove
401
remove
16
remove
336
remove
51
ref
405
remove
appTerm
398
remove
appTerm
appTerm
404
remove
appTerm
appTerm
426
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
thm
"Data.List.unzip"
"Data.List.foldr"
const
1
ref
1
ref
368
remove
1
ref
367
remove
24
ref
59
remove
cons
opType
430
def
430
ref
nil
cons
431
def
cons
opType
432
def
nil
cons
433
def
cons
opType
434
def
1
ref
430
ref
1
ref
370
remove
431
ref
cons
opType
435
def
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
67
ref
1
ref
1
ref
434
ref
8
ref
cons
opType
434
ref
nil
cons
cons
opType
constTerm
"f"
434
remove
var
436
def
43
remove
183
remove
117
remove
"y"
3
remove
var
437
def
13
ref
1
ref
432
ref
1
ref
432
ref
8
ref
cons
opType
438
def
nil
cons
cons
opType
constTerm
436
remove
varTerm
377
remove
184
ref
appTerm
437
remove
varTerm
439
def
appTerm
appTerm
appTerm
67
remove
1
ref
438
remove
433
remove
cons
opType
constTerm
"f"
432
remove
var
440
def
46
remove
"xs"
24
ref
var
441
def
34
remove
"ys"
19
ref
var
442
def
13
ref
1
ref
430
ref
1
ref
430
remove
8
ref
cons
opType
nil
cons
cons
opType
constTerm
440
remove
varTerm
376
remove
1
ref
24
remove
1
ref
19
remove
431
remove
cons
opType
nil
cons
cons
opType
constTerm
443
def
441
remove
varTerm
444
def
appTerm
442
remove
varTerm
445
def
appTerm
appTerm
appTerm
443
ref
51
remove
184
remove
appTerm
444
remove
appTerm
appTerm
402
remove
439
remove
appTerm
445
remove
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
443
remove
38
remove
appTerm
22
remove
appTerm
appTerm
446
def
defineConst
447
def
pop
448
def
pop
447
remove
nil
13
remove
1
ref
435
ref
1
remove
435
ref
8
remove
cons
opType
nil
cons
cons
opType
constTerm
448
remove
435
remove
constTerm
appTerm
446
remove
appTerm
thm