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