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