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