6
version
nil
"P"
"->"
typeOp
0
def
"Data.List.list"
typeOp
"A"
varType
1
def
nil
cons
2
def
opType
3
def
"bool"
typeOp
nil
opType
4
def
nil
cons
5
def
cons
opType
6
def
var
7
def
"l1"
3
ref
var
8
def
"Data.Bool.!"
const
9
def
0
ref
6
ref
5
ref
cons
opType
10
def
constTerm
11
def
"l2"
3
ref
var
12
def
"="
const
13
def
0
ref
3
ref
6
ref
nil
cons
14
def
cons
opType
constTerm
15
def
"Data.List.foldr"
const
16
def
0
ref
0
ref
1
ref
0
ref
3
ref
3
ref
nil
cons
17
def
cons
opType
18
def
nil
cons
19
def
cons
opType
20
def
0
ref
3
ref
19
remove
cons
opType
21
def
nil
cons
22
def
cons
opType
constTerm
23
def
"Data.List.::"
const
20
ref
constTerm
24
def
appTerm
25
def
12
ref
varTerm
26
def
appTerm
27
def
8
ref
varTerm
28
def
appTerm
appTerm
"Data.List.@"
const
21
remove
constTerm
29
def
28
ref
appTerm
26
ref
appTerm
30
def
appTerm
31
def
absTerm
32
def
appTerm
33
def
absTerm
34
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
17
ref
cons
nil
cons
35
def
nil
nil
cons
36
def
cons
37
def
13
ref
0
ref
4
ref
0
ref
4
ref
5
ref
cons
opType
38
def
nil
cons
cons
opType
39
def
constTerm
40
def
9
ref
0
ref
0
ref
1
ref
5
ref
cons
opType
41
def
5
ref
cons
opType
42
def
constTerm
43
def
"P"
41
ref
var
44
def
varTerm
45
def
appTerm
46
def
appTerm
refl
"p"
41
ref
var
47
def
13
ref
0
ref
41
ref
42
ref
nil
cons
cons
opType
constTerm
47
remove
varTerm
appTerm
"x"
1
ref
var
48
def
"Data.Bool.T"
const
4
ref
constTerm
49
def
absTerm
50
def
appTerm
absTerm
51
def
45
ref
appTerm
betaConv
52
def
appThm
nil
13
ref
0
ref
42
ref
0
ref
42
remove
5
ref
cons
opType
nil
cons
cons
opType
constTerm
43
ref
appTerm
51
remove
appTerm
axiom
45
ref
refl
appThm
53
def
eqMp
sym
54
def
subst
55
def
subst
8
ref
nil
"t"
4
ref
var
56
def
33
remove
nil
cons
cons
nil
cons
nil
cons
cons
40
ref
56
ref
varTerm
57
def
appTerm
49
ref
appTerm
assume
sym
nil
49
ref
axiom
58
def
eqMp
57
ref
assume
58
ref
deductAntisym
deductAntisym
59
def
subst
nil
7
ref
32
remove
nil
cons
cons
nil
cons
nil
cons
cons
55
ref
subst
12
ref
nil
56
ref
31
ref
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
8
ref
31
remove
absTerm
60
def
28
ref
appTerm
61
def
betaConv
62
def
15
ref
refl
63
def
nil
"b"
3
ref
var
26
ref
nil
cons
64
def
cons
65
def
"f"
20
ref
var
24
ref
nil
cons
cons
nil
cons
66
def
cons
nil
cons
cons
67
def
"A"
2
ref
cons
68
def
"B"
17
ref
cons
69
def
nil
cons
cons
36
ref
cons
70
def
"b"
"B"
varType
71
def
var
72
def
13
ref
0
ref
71
ref
0
ref
71
ref
5
ref
cons
opType
73
def
nil
cons
cons
opType
constTerm
74
def
16
ref
0
ref
0
ref
1
ref
0
ref
71
ref
71
ref
nil
cons
75
def
cons
opType
nil
cons
76
def
cons
opType
77
def
0
ref
71
ref
0
ref
3
ref
75
ref
cons
opType
nil
cons
cons
opType
nil
cons
78
def
cons
opType
constTerm
79
def
"f"
77
ref
var
80
def
varTerm
81
def
appTerm
82
def
72
ref
varTerm
83
def
appTerm
84
def
"Data.List.[]"
const
3
ref
constTerm
85
def
appTerm
86
def
appTerm
83
ref
appTerm
absTerm
87
def
83
ref
appTerm
88
def
betaConv
80
ref
9
ref
0
ref
73
ref
5
ref
cons
opType
constTerm
89
def
87
ref
appTerm
90
def
absTerm
91
def
81
ref
appTerm
92
def
betaConv
nil
9
ref
0
ref
0
ref
77
ref
5
ref
cons
opType
93
def
5
ref
cons
opType
constTerm
94
def
91
ref
appTerm
95
def
axiom
nil
"p"
4
ref
var
96
def
95
remove
nil
cons
cons
"q"
4
ref
var
97
def
92
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
40
ref
"Data.Bool.==>"
const
39
ref
constTerm
98
def
96
ref
varTerm
99
def
appTerm
97
ref
varTerm
100
def
appTerm
101
def
appTerm
refl
96
ref
97
ref
40
ref
"Data.Bool./\\"
const
39
ref
constTerm
102
def
99
ref
appTerm
103
def
100
ref
appTerm
104
def
appTerm
105
def
99
ref
appTerm
absTerm
106
def
absTerm
107
def
99
ref
appTerm
betaConv
100
ref
refl
108
def
appThm
106
remove
100
ref
appTerm
betaConv
trans
appThm
nil
13
ref
0
ref
39
ref
0
ref
39
ref
5
ref
cons
opType
109
def
nil
cons
cons
opType
constTerm
110
def
98
ref
appTerm
107
remove
appTerm
axiom
99
ref
refl
111
def
appThm
108
ref
appThm
eqMp
112
def
sym
113
def
105
remove
refl
97
ref
13
ref
0
ref
109
ref
0
ref
109
remove
5
ref
cons
opType
nil
cons
cons
opType
constTerm
114
def
"f"
39
remove
var
115
def
115
ref
varTerm
116
def
99
ref
appTerm
100
ref
appTerm
absTerm
117
def
appTerm
115
ref
116
ref
49
ref
appTerm
49
ref
appTerm
absTerm
118
def
appTerm
absTerm
119
def
100
ref
appTerm
betaConv
appThm
13
ref
0
ref
38
ref
0
ref
38
ref
5
ref
cons
opType
120
def
nil
cons
cons
opType
constTerm
121
def
103
remove
appTerm
refl
96
ref
119
remove
absTerm
122
def
99
ref
appTerm
betaConv
appThm
nil
110
remove
102
ref
appTerm
122
ref
appTerm
axiom
123
def
111
remove
appThm
eqMp
108
ref
appThm
eqMp
124
def
sym
115
ref
116
ref
refl
nil
56
ref
99
ref
nil
cons
125
def
cons
nil
cons
nil
cons
cons
59
ref
subst
99
ref
assume
126
def
eqMp
appThm
nil
56
ref
100
ref
nil
cons
127
def
cons
nil
cons
nil
cons
cons
59
ref
subst
100
ref
assume
eqMp
appThm
absThm
eqMp
128
def
nil
"P"
4
ref
var
129
def
125
remove
cons
"Q"
4
ref
var
130
def
127
remove
cons
nil
cons
cons
nil
cons
cons
40
ref
refl
131
def
115
ref
116
remove
129
ref
varTerm
132
def
appTerm
133
def
130
ref
varTerm
134
def
appTerm
absTerm
135
def
96
ref
97
ref
99
ref
absTerm
absTerm
136
def
appTerm
betaConv
136
ref
132
ref
appTerm
betaConv
134
ref
refl
137
def
appThm
97
ref
132
ref
absTerm
134
ref
appTerm
betaConv
trans
trans
appThm
118
ref
136
ref
appTerm
betaConv
136
ref
49
ref
appTerm
betaConv
49
ref
refl
138
def
appThm
97
ref
49
ref
absTerm
49
ref
appTerm
betaConv
trans
trans
appThm
40
ref
102
ref
132
ref
appTerm
139
def
134
ref
appTerm
140
def
appTerm
refl
97
ref
114
remove
115
remove
133
remove
100
ref
appTerm
absTerm
appTerm
118
ref
appTerm
absTerm
134
ref
appTerm
betaConv
appThm
121
remove
139
remove
appTerm
refl
122
remove
132
ref
appTerm
betaConv
appThm
123
remove
132
ref
refl
appThm
eqMp
137
ref
appThm
eqMp
140
remove
assume
eqMp
141
def
136
remove
refl
appThm
eqMp
sym
58
ref
eqMp
142
def
subst
deductAntisym
eqMp
112
remove
101
remove
assume
eqMp
sym
126
remove
eqMp
131
ref
117
remove
96
ref
97
ref
100
ref
absTerm
143
def
absTerm
144
def
appTerm
betaConv
144
ref
99
remove
appTerm
betaConv
108
remove
appThm
143
ref
100
remove
appTerm
betaConv
trans
trans
appThm
118
remove
144
ref
appTerm
betaConv
144
ref
49
ref
appTerm
betaConv
138
remove
appThm
143
ref
49
ref
appTerm
betaConv
trans
trans
145
def
appThm
124
remove
104
remove
assume
eqMp
144
ref
refl
146
def
appThm
eqMp
sym
58
ref
eqMp
147
def
proveHyp
deductAntisym
148
def
subst
proveHyp
"A"
77
ref
nil
cons
149
def
cons
nil
cons
150
def
"P"
93
remove
var
151
def
91
remove
nil
cons
cons
"x"
77
ref
var
81
ref
nil
cons
cons
nil
cons
152
def
cons
nil
cons
cons
nil
96
ref
46
ref
nil
cons
153
def
cons
97
ref
45
remove
48
ref
varTerm
154
def
appTerm
155
def
nil
cons
156
def
cons
nil
cons
cons
nil
cons
cons
157
def
113
ref
subst
157
remove
147
remove
128
remove
deductAntisym
158
def
subst
40
ref
155
remove
appTerm
refl
50
remove
154
ref
appTerm
betaConv
appThm
52
remove
53
remove
46
remove
assume
eqMp
eqMp
154
ref
refl
159
def
appThm
eqMp
sym
58
ref
eqMp
eqMp
nil
129
ref
153
remove
cons
130
ref
156
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
160
def
subst
eqMp
eqMp
nil
96
ref
90
remove
nil
cons
cons
97
ref
88
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
"A"
75
ref
cons
161
def
nil
cons
162
def
"P"
73
remove
var
163
def
87
remove
nil
cons
cons
"x"
71
ref
var
164
def
83
ref
nil
cons
cons
nil
cons
165
def
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
166
def
subst
subst
appThm
nil
"l"
3
ref
var
167
def
64
ref
cons
168
def
nil
cons
nil
cons
cons
169
def
167
ref
15
ref
29
ref
85
ref
appTerm
170
def
167
ref
varTerm
171
def
appTerm
appTerm
171
ref
appTerm
absTerm
172
def
171
ref
appTerm
173
def
betaConv
nil
11
ref
172
ref
appTerm
174
def
axiom
nil
96
ref
174
remove
nil
cons
cons
97
ref
173
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
35
ref
7
ref
172
remove
nil
cons
cons
"x"
3
ref
var
175
def
171
ref
nil
cons
176
def
cons
nil
cons
177
def
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
subst
178
def
appThm
nil
175
ref
64
remove
cons
nil
cons
179
def
nil
cons
cons
37
ref
nil
56
ref
13
ref
0
ref
1
ref
41
remove
nil
cons
cons
opType
constTerm
154
ref
appTerm
154
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
159
ref
eqMp
180
def
subst
181
def
subst
trans
sym
58
ref
eqMp
nil
96
ref
15
ref
27
ref
85
ref
appTerm
appTerm
170
remove
26
ref
appTerm
182
def
appTerm
183
def
nil
cons
cons
97
ref
43
ref
"h"
1
ref
var
184
def
11
ref
"t"
3
ref
var
185
def
98
ref
15
ref
27
ref
185
ref
varTerm
186
def
appTerm
appTerm
29
ref
186
ref
appTerm
187
def
26
ref
appTerm
188
def
appTerm
189
def
appTerm
15
ref
27
remove
24
ref
184
ref
varTerm
190
def
appTerm
191
def
186
ref
appTerm
192
def
appTerm
appTerm
29
ref
192
ref
appTerm
193
def
26
ref
appTerm
194
def
appTerm
195
def
appTerm
196
def
absTerm
197
def
appTerm
198
def
absTerm
199
def
appTerm
200
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
158
ref
subst
proveHyp
nil
44
ref
199
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
184
ref
nil
56
ref
198
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
7
ref
197
remove
nil
cons
cons
nil
cons
nil
cons
cons
55
ref
subst
185
ref
nil
56
ref
196
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
96
ref
189
ref
nil
cons
201
def
cons
97
ref
195
remove
nil
cons
202
def
cons
nil
cons
cons
nil
cons
cons
203
def
113
ref
subst
203
remove
158
ref
subst
63
ref
67
remove
70
ref
185
ref
74
ref
84
ref
192
ref
appTerm
204
def
appTerm
81
ref
190
ref
appTerm
205
def
84
ref
186
ref
appTerm
206
def
appTerm
appTerm
absTerm
207
def
186
ref
appTerm
208
def
betaConv
184
ref
11
ref
207
ref
appTerm
209
def
absTerm
210
def
190
ref
appTerm
211
def
betaConv
72
ref
43
ref
210
ref
appTerm
212
def
absTerm
213
def
83
ref
appTerm
214
def
betaConv
80
ref
89
ref
213
ref
appTerm
215
def
absTerm
216
def
81
ref
appTerm
217
def
betaConv
nil
94
ref
216
ref
appTerm
218
def
axiom
nil
96
ref
218
remove
nil
cons
cons
97
ref
217
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
150
ref
151
ref
216
remove
nil
cons
cons
152
remove
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
215
remove
nil
cons
cons
97
ref
214
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
162
ref
163
ref
213
remove
nil
cons
cons
165
ref
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
212
remove
nil
cons
cons
97
ref
211
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
68
ref
nil
cons
219
def
44
ref
210
remove
nil
cons
cons
48
ref
190
ref
nil
cons
cons
nil
cons
220
def
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
209
remove
nil
cons
cons
97
ref
208
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
35
ref
7
ref
207
remove
nil
cons
cons
175
ref
186
ref
nil
cons
221
def
cons
nil
cons
222
def
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
223
def
subst
subst
191
ref
refl
189
remove
assume
appThm
trans
appThm
169
ref
185
ref
15
ref
193
remove
171
ref
appTerm
appTerm
191
ref
187
remove
171
ref
appTerm
appTerm
appTerm
absTerm
224
def
186
ref
appTerm
225
def
betaConv
184
ref
11
ref
224
ref
appTerm
226
def
absTerm
227
def
190
ref
appTerm
228
def
betaConv
167
ref
43
ref
227
ref
appTerm
229
def
absTerm
230
def
171
ref
appTerm
231
def
betaConv
nil
11
ref
230
ref
appTerm
232
def
axiom
nil
96
ref
232
remove
nil
cons
cons
97
ref
231
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
35
ref
7
ref
230
remove
nil
cons
cons
177
ref
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
229
remove
nil
cons
cons
97
ref
228
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
219
ref
44
ref
227
remove
nil
cons
cons
220
ref
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
226
remove
nil
cons
cons
97
ref
225
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
35
ref
7
ref
224
remove
nil
cons
cons
222
ref
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
subst
233
def
appThm
nil
175
ref
191
ref
188
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
181
ref
subst
trans
sym
58
ref
eqMp
eqMp
nil
129
ref
201
remove
cons
130
ref
202
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
96
ref
102
ref
183
remove
appTerm
200
remove
appTerm
nil
cons
cons
97
ref
11
ref
60
ref
appTerm
nil
cons
234
def
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
98
ref
refl
235
def
102
ref
refl
236
def
60
ref
85
ref
appTerm
betaConv
appThm
43
ref
refl
237
def
184
ref
11
ref
refl
238
def
185
ref
235
ref
60
ref
186
ref
appTerm
betaConv
appThm
60
ref
192
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
238
ref
8
ref
62
remove
absThm
appThm
appThm
nil
"p"
6
ref
var
239
def
60
remove
nil
cons
240
def
cons
nil
cons
nil
cons
cons
239
ref
98
ref
102
ref
239
ref
varTerm
241
def
85
ref
appTerm
appTerm
43
ref
184
ref
11
ref
185
ref
98
ref
241
ref
186
ref
appTerm
appTerm
241
ref
192
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
11
ref
167
ref
241
ref
171
ref
appTerm
absTerm
appTerm
appTerm
absTerm
242
def
241
ref
appTerm
243
def
betaConv
nil
9
ref
0
ref
10
ref
5
ref
cons
opType
constTerm
242
ref
appTerm
244
def
axiom
nil
96
ref
244
remove
nil
cons
cons
97
ref
243
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
"A"
14
remove
cons
nil
cons
"P"
10
remove
var
242
remove
nil
cons
cons
"x"
6
remove
var
241
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
245
def
subst
eqMp
eqMp
nil
96
ref
234
remove
cons
97
ref
61
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
35
ref
7
ref
240
remove
cons
175
ref
28
ref
nil
cons
246
def
cons
nil
cons
247
def
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
248
def
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
11
ref
34
remove
appTerm
thm
238
ref
167
ref
63
ref
nil
8
ref
176
remove
cons
12
ref
85
ref
nil
cons
249
def
cons
nil
cons
cons
nil
cons
cons
250
def
248
ref
subst
167
ref
15
ref
29
ref
171
ref
appTerm
85
ref
appTerm
appTerm
171
ref
appTerm
absTerm
251
def
171
ref
appTerm
252
def
betaConv
nil
11
ref
251
ref
appTerm
253
def
axiom
nil
96
ref
253
remove
nil
cons
cons
97
ref
252
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
35
ref
7
ref
251
remove
nil
cons
cons
177
ref
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
254
def
trans
appThm
171
ref
refl
appThm
nil
177
ref
nil
cons
cons
181
ref
subst
trans
absThm
appThm
nil
56
ref
49
ref
nil
cons
cons
nil
cons
nil
cons
cons
255
def
37
remove
56
ref
40
ref
43
ref
48
ref
57
ref
absTerm
appTerm
appTerm
57
ref
appTerm
absTerm
256
def
57
ref
appTerm
257
def
betaConv
nil
9
ref
120
remove
constTerm
258
def
256
ref
appTerm
259
def
axiom
nil
96
ref
259
remove
nil
cons
cons
97
ref
257
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
"A"
5
ref
cons
nil
cons
260
def
"P"
38
remove
var
261
def
256
remove
nil
cons
cons
"x"
4
remove
var
57
ref
nil
cons
cons
nil
cons
262
def
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
263
def
subst
subst
264
def
trans
sym
58
ref
eqMp
nil
11
ref
167
ref
15
ref
25
remove
85
ref
appTerm
171
ref
appTerm
appTerm
171
ref
appTerm
absTerm
appTerm
thm
nil
151
ref
80
ref
89
ref
72
ref
11
ref
8
ref
11
ref
12
ref
74
ref
84
ref
30
ref
appTerm
appTerm
265
def
82
remove
84
ref
26
ref
appTerm
266
def
appTerm
267
def
28
ref
appTerm
268
def
appTerm
269
def
absTerm
270
def
appTerm
271
def
absTerm
272
def
appTerm
273
def
absTerm
274
def
appTerm
275
def
absTerm
276
def
nil
cons
cons
nil
cons
nil
cons
cons
150
remove
36
ref
cons
277
def
54
ref
subst
278
def
subst
80
ref
nil
56
ref
275
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
163
ref
274
remove
nil
cons
cons
nil
cons
nil
cons
cons
162
ref
36
ref
cons
279
def
54
ref
subst
280
def
subst
72
ref
nil
56
ref
273
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
7
ref
272
remove
nil
cons
cons
nil
cons
nil
cons
cons
55
ref
subst
8
ref
nil
56
ref
271
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
7
ref
270
remove
nil
cons
cons
nil
cons
nil
cons
cons
55
ref
subst
12
ref
nil
56
ref
269
ref
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
8
ref
269
remove
absTerm
281
def
28
ref
appTerm
282
def
betaConv
283
def
74
ref
refl
284
def
84
ref
refl
285
def
178
remove
appThm
appThm
nil
72
ref
266
ref
nil
cons
286
def
cons
nil
cons
nil
cons
cons
287
def
166
ref
subst
288
def
appThm
nil
164
ref
286
ref
cons
nil
cons
nil
cons
cons
279
ref
180
ref
subst
289
def
subst
290
def
trans
sym
58
ref
eqMp
nil
96
ref
74
ref
84
ref
182
remove
appTerm
appTerm
267
ref
85
ref
appTerm
291
def
appTerm
292
def
nil
cons
cons
97
ref
43
ref
184
ref
11
ref
185
ref
98
ref
74
ref
84
ref
188
ref
appTerm
appTerm
267
ref
186
ref
appTerm
293
def
appTerm
294
def
appTerm
74
ref
84
ref
194
remove
appTerm
appTerm
267
remove
192
ref
appTerm
295
def
appTerm
296
def
appTerm
297
def
absTerm
298
def
appTerm
299
def
absTerm
300
def
appTerm
301
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
158
ref
subst
proveHyp
nil
44
ref
300
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
184
ref
nil
56
ref
299
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
7
ref
298
remove
nil
cons
cons
nil
cons
nil
cons
cons
55
ref
subst
185
ref
nil
56
ref
297
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
96
ref
294
ref
nil
cons
302
def
cons
97
ref
296
remove
nil
cons
303
def
cons
nil
cons
cons
nil
cons
cons
304
def
113
ref
subst
304
remove
158
ref
subst
284
ref
285
remove
233
remove
appThm
nil
185
ref
188
remove
nil
cons
cons
nil
cons
nil
cons
cons
223
ref
subst
205
ref
refl
305
def
294
remove
assume
appThm
trans
trans
appThm
287
remove
223
ref
subst
306
def
appThm
nil
164
ref
205
ref
293
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
289
ref
subst
trans
sym
58
ref
eqMp
eqMp
nil
129
ref
302
remove
cons
130
ref
303
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
96
ref
102
ref
292
remove
appTerm
301
remove
appTerm
nil
cons
cons
97
ref
11
ref
281
ref
appTerm
nil
cons
307
def
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
235
ref
236
ref
281
ref
85
ref
appTerm
betaConv
appThm
237
ref
184
ref
238
ref
185
ref
235
ref
281
ref
186
ref
appTerm
betaConv
appThm
281
ref
192
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
238
ref
8
ref
283
remove
absThm
appThm
appThm
nil
239
ref
281
remove
nil
cons
308
def
cons
nil
cons
nil
cons
cons
245
ref
subst
eqMp
eqMp
nil
96
ref
307
remove
cons
97
ref
282
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
35
ref
7
ref
308
remove
cons
247
ref
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
309
def
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
94
ref
276
remove
appTerm
thm
nil
"P"
0
ref
0
ref
71
ref
76
remove
cons
opType
310
def
5
ref
cons
opType
311
def
var
312
def
"g"
310
ref
var
313
def
94
ref
80
ref
89
ref
72
ref
11
ref
8
ref
11
ref
12
ref
98
ref
102
ref
89
ref
"s"
71
ref
var
314
def
74
ref
313
ref
varTerm
315
def
83
ref
appTerm
314
ref
varTerm
316
def
appTerm
appTerm
316
ref
appTerm
absTerm
317
def
appTerm
318
def
appTerm
43
ref
48
ref
89
ref
"s1"
71
ref
var
319
def
89
ref
"s2"
71
ref
var
320
def
74
ref
315
ref
81
ref
154
ref
appTerm
321
def
319
ref
varTerm
322
def
appTerm
appTerm
320
ref
varTerm
323
def
appTerm
appTerm
321
remove
315
ref
322
ref
appTerm
324
def
323
ref
appTerm
325
def
appTerm
appTerm
absTerm
326
def
appTerm
327
def
absTerm
328
def
appTerm
329
def
absTerm
330
def
appTerm
331
def
appTerm
332
def
appTerm
265
remove
315
ref
84
ref
28
ref
appTerm
appTerm
266
ref
appTerm
333
def
appTerm
334
def
appTerm
335
def
absTerm
336
def
appTerm
337
def
absTerm
338
def
appTerm
339
def
absTerm
340
def
appTerm
341
def
absTerm
342
def
appTerm
343
def
absTerm
344
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
310
remove
nil
cons
cons
nil
cons
36
ref
cons
54
ref
subst
345
def
subst
313
ref
nil
56
ref
343
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
151
remove
342
remove
nil
cons
cons
nil
cons
nil
cons
cons
278
remove
subst
80
ref
nil
56
ref
341
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
163
ref
340
remove
nil
cons
cons
nil
cons
nil
cons
cons
280
ref
subst
72
ref
nil
56
ref
339
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
7
ref
338
remove
nil
cons
cons
nil
cons
nil
cons
cons
55
ref
subst
8
ref
nil
56
ref
337
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
7
ref
336
remove
nil
cons
cons
nil
cons
nil
cons
cons
55
ref
subst
12
ref
nil
56
ref
335
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
96
ref
332
remove
nil
cons
346
def
cons
97
ref
334
remove
nil
cons
347
def
cons
nil
cons
cons
nil
cons
cons
348
def
113
ref
subst
348
remove
158
ref
subst
nil
129
ref
318
remove
nil
cons
349
def
cons
130
ref
331
remove
nil
cons
350
def
cons
nil
cons
cons
nil
cons
cons
351
def
142
ref
subst
351
remove
131
remove
135
remove
144
ref
appTerm
betaConv
144
remove
132
remove
appTerm
betaConv
137
remove
appThm
143
remove
134
remove
appTerm
betaConv
trans
trans
appThm
145
remove
appThm
141
remove
146
remove
appThm
eqMp
sym
58
ref
eqMp
352
def
subst
284
ref
309
ref
appThm
333
ref
refl
appThm
sym
8
ref
74
ref
268
remove
appTerm
333
remove
appTerm
absTerm
353
def
28
ref
appTerm
354
def
betaConv
355
def
284
ref
288
remove
appThm
315
ref
refl
356
def
166
ref
appThm
266
ref
refl
357
def
appThm
nil
314
ref
286
ref
cons
nil
cons
nil
cons
cons
317
ref
316
ref
appTerm
358
def
betaConv
nil
96
ref
349
remove
cons
97
ref
358
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
162
ref
163
ref
317
remove
nil
cons
cons
164
ref
316
ref
nil
cons
cons
nil
cons
359
def
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
subst
trans
appThm
290
remove
trans
sym
58
ref
eqMp
nil
96
ref
74
ref
291
remove
appTerm
315
ref
86
remove
appTerm
266
ref
appTerm
appTerm
360
def
nil
cons
cons
97
ref
43
ref
184
ref
11
ref
185
ref
98
ref
74
ref
293
remove
appTerm
315
ref
206
ref
appTerm
266
ref
appTerm
361
def
appTerm
362
def
appTerm
74
ref
295
remove
appTerm
315
ref
204
remove
appTerm
266
remove
appTerm
appTerm
363
def
appTerm
364
def
absTerm
365
def
appTerm
366
def
absTerm
367
def
appTerm
368
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
158
ref
subst
proveHyp
nil
44
ref
367
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
ref
subst
184
ref
nil
56
ref
366
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
7
ref
365
remove
nil
cons
cons
nil
cons
nil
cons
cons
55
ref
subst
185
ref
nil
56
ref
364
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
96
ref
362
ref
nil
cons
369
def
cons
97
ref
363
remove
nil
cons
370
def
cons
nil
cons
cons
nil
cons
cons
371
def
113
ref
subst
371
remove
158
ref
subst
284
ref
306
remove
305
remove
362
remove
assume
appThm
trans
appThm
356
ref
223
ref
appThm
357
remove
appThm
nil
320
ref
286
remove
cons
319
ref
206
remove
nil
cons
cons
220
ref
cons
cons
nil
cons
cons
326
ref
323
ref
appTerm
372
def
betaConv
328
ref
322
ref
appTerm
373
def
betaConv
330
ref
154
ref
appTerm
374
def
betaConv
nil
96
ref
350
remove
cons
97
ref
374
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
219
ref
44
ref
330
remove
nil
cons
cons
48
ref
154
ref
nil
cons
cons
nil
cons
375
def
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
329
remove
nil
cons
cons
97
ref
373
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
162
ref
163
ref
328
remove
nil
cons
cons
164
ref
322
ref
nil
cons
376
def
cons
nil
cons
377
def
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
327
remove
nil
cons
cons
97
ref
372
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
162
ref
163
ref
326
remove
nil
cons
cons
164
ref
323
ref
nil
cons
378
def
cons
nil
cons
379
def
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
subst
trans
appThm
nil
164
ref
205
remove
361
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
289
ref
subst
trans
sym
58
ref
eqMp
eqMp
nil
129
ref
369
remove
cons
130
ref
370
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
96
ref
102
ref
360
remove
appTerm
368
remove
appTerm
nil
cons
cons
97
ref
11
ref
353
ref
appTerm
nil
cons
380
def
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
235
ref
236
ref
353
ref
85
ref
appTerm
betaConv
appThm
237
ref
184
ref
238
ref
185
ref
235
ref
353
ref
186
ref
appTerm
betaConv
appThm
353
ref
192
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
238
ref
8
ref
355
remove
absThm
appThm
appThm
nil
239
ref
353
remove
nil
cons
381
def
cons
nil
cons
nil
cons
cons
245
ref
subst
eqMp
eqMp
nil
96
ref
380
remove
cons
97
ref
354
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
35
ref
7
ref
381
remove
cons
247
ref
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
eqMp
proveHyp
proveHyp
eqMp
nil
129
ref
346
remove
cons
130
ref
347
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
382
def
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
9
ref
0
ref
311
remove
5
ref
cons
opType
constTerm
383
def
344
remove
appTerm
thm
9
ref
0
ref
0
ref
0
ref
71
ref
0
ref
1
ref
75
ref
cons
opType
384
def
nil
cons
385
def
cons
opType
386
def
5
ref
cons
opType
387
def
5
ref
cons
opType
constTerm
388
def
refl
389
def
"f"
386
ref
var
390
def
89
ref
refl
391
def
72
ref
284
ref
nil
167
ref
249
ref
cons
nil
cons
nil
cons
cons
167
ref
74
ref
"Data.List.foldl"
const
392
def
0
ref
386
ref
78
remove
cons
opType
constTerm
393
def
390
ref
varTerm
394
def
appTerm
395
def
83
ref
appTerm
396
def
171
ref
appTerm
appTerm
79
ref
"Function.flip"
const
397
def
0
ref
386
ref
149
remove
cons
opType
constTerm
394
ref
appTerm
398
def
appTerm
399
def
83
ref
appTerm
400
def
"Data.List.reverse"
const
18
remove
constTerm
401
def
171
ref
appTerm
402
def
appTerm
appTerm
absTerm
403
def
171
ref
appTerm
404
def
betaConv
72
ref
11
ref
403
ref
appTerm
405
def
absTerm
406
def
83
ref
appTerm
407
def
betaConv
390
ref
89
ref
406
ref
appTerm
408
def
absTerm
409
def
394
ref
appTerm
410
def
betaConv
nil
388
ref
409
ref
appTerm
411
def
axiom
nil
96
ref
411
remove
nil
cons
cons
97
ref
410
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
"A"
386
ref
nil
cons
412
def
cons
nil
cons
413
def
"P"
387
remove
var
414
def
409
remove
nil
cons
cons
"x"
386
remove
var
394
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
408
remove
nil
cons
cons
97
ref
407
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
162
ref
163
ref
406
remove
nil
cons
cons
165
ref
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
405
remove
nil
cons
cons
97
ref
404
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
35
ref
7
ref
403
remove
nil
cons
cons
177
ref
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
415
def
subst
400
ref
refl
416
def
nil
15
ref
401
ref
85
ref
appTerm
appTerm
85
ref
appTerm
axiom
appThm
nil
80
ref
398
ref
nil
cons
cons
nil
cons
417
def
nil
cons
cons
166
ref
subst
418
def
trans
trans
appThm
83
ref
refl
419
def
appThm
nil
165
remove
nil
cons
cons
289
ref
subst
trans
absThm
appThm
255
ref
279
remove
263
ref
subst
subst
420
def
trans
absThm
appThm
255
ref
413
remove
36
ref
cons
421
def
263
ref
subst
subst
422
def
trans
sym
58
ref
eqMp
nil
388
ref
390
ref
89
ref
72
ref
74
ref
396
ref
85
ref
appTerm
appTerm
83
ref
appTerm
absTerm
appTerm
absTerm
appTerm
thm
389
ref
390
ref
391
ref
72
ref
237
ref
184
ref
238
ref
185
ref
284
ref
nil
167
ref
192
ref
nil
cons
cons
nil
cons
nil
cons
cons
415
ref
subst
416
ref
185
ref
15
ref
401
ref
192
ref
appTerm
appTerm
29
ref
401
ref
186
ref
appTerm
423
def
appTerm
191
remove
85
ref
appTerm
424
def
appTerm
appTerm
absTerm
425
def
186
ref
appTerm
426
def
betaConv
184
ref
11
ref
425
ref
appTerm
427
def
absTerm
428
def
190
ref
appTerm
429
def
betaConv
nil
43
ref
428
ref
appTerm
430
def
axiom
nil
96
ref
430
remove
nil
cons
cons
97
ref
429
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
219
ref
44
ref
428
remove
nil
cons
cons
220
ref
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
427
remove
nil
cons
cons
97
ref
426
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
35
ref
7
ref
425
remove
nil
cons
cons
222
ref
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
appThm
nil
12
ref
424
remove
nil
cons
cons
8
ref
423
ref
nil
cons
cons
417
ref
cons
cons
nil
cons
cons
309
ref
subst
399
ref
refl
431
def
nil
185
ref
249
remove
cons
417
ref
cons
nil
cons
cons
223
ref
subst
nil
"y"
71
ref
var
432
def
400
ref
85
ref
appTerm
nil
cons
cons
220
ref
cons
nil
cons
cons
"B"
2
remove
cons
433
def
161
remove
"C"
75
ref
cons
nil
cons
434
def
cons
cons
36
ref
cons
"y"
1
ref
var
435
def
13
ref
0
ref
"C"
varType
436
def
0
ref
436
ref
5
ref
cons
opType
nil
cons
cons
opType
constTerm
397
ref
0
ref
0
ref
1
ref
0
ref
71
ref
436
remove
nil
cons
437
def
cons
opType
nil
cons
cons
opType
438
def
0
ref
71
ref
0
ref
1
ref
437
remove
cons
opType
nil
cons
cons
opType
439
def
nil
cons
cons
opType
440
def
constTerm
441
def
"f"
438
ref
var
442
def
varTerm
443
def
appTerm
444
def
164
ref
varTerm
445
def
appTerm
435
ref
varTerm
446
def
appTerm
appTerm
443
ref
446
ref
appTerm
445
ref
appTerm
447
def
appTerm
absTerm
448
def
446
ref
appTerm
449
def
betaConv
164
ref
43
ref
448
ref
appTerm
450
def
absTerm
451
def
445
ref
appTerm
452
def
betaConv
442
ref
89
ref
451
ref
appTerm
453
def
absTerm
454
def
443
ref
appTerm
455
def
betaConv
nil
9
ref
0
ref
0
ref
438
ref
5
ref
cons
opType
456
def
5
ref
cons
opType
constTerm
457
def
454
ref
appTerm
458
def
axiom
nil
96
ref
458
remove
nil
cons
cons
97
ref
455
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
"A"
438
ref
nil
cons
459
def
cons
nil
cons
460
def
"P"
456
ref
var
461
def
454
remove
nil
cons
cons
"x"
438
ref
var
443
ref
nil
cons
cons
nil
cons
462
def
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
453
remove
nil
cons
cons
97
ref
452
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
162
ref
163
ref
451
remove
nil
cons
cons
164
ref
445
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
450
remove
nil
cons
cons
97
ref
449
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
219
ref
44
ref
448
remove
nil
cons
cons
48
ref
446
ref
nil
cons
cons
nil
cons
463
def
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
subst
464
def
subst
trans
394
ref
refl
418
remove
appThm
190
ref
refl
appThm
trans
appThm
423
ref
refl
appThm
trans
trans
trans
appThm
nil
167
ref
221
remove
cons
72
ref
394
ref
83
ref
appTerm
190
ref
appTerm
465
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
415
ref
subst
appThm
nil
164
ref
399
ref
465
ref
appTerm
423
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
289
ref
subst
trans
absThm
appThm
264
ref
trans
absThm
appThm
255
ref
263
ref
subst
466
def
trans
absThm
appThm
420
ref
trans
absThm
appThm
422
ref
trans
sym
58
ref
eqMp
nil
388
ref
390
ref
89
ref
72
ref
43
ref
184
ref
11
ref
185
ref
74
ref
396
ref
192
ref
appTerm
appTerm
395
ref
465
remove
appTerm
186
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
thm
238
ref
8
ref
238
ref
12
ref
63
ref
nil
167
ref
246
remove
cons
467
def
65
remove
"f"
0
ref
3
ref
0
ref
1
ref
17
ref
cons
opType
nil
cons
cons
opType
468
def
var
397
ref
0
ref
20
remove
468
ref
nil
cons
cons
opType
constTerm
24
remove
appTerm
469
def
nil
cons
cons
nil
cons
cons
cons
nil
cons
cons
70
remove
415
ref
subst
subst
23
remove
refl
nil
66
remove
nil
cons
cons
68
ref
69
remove
"C"
17
remove
cons
nil
cons
cons
cons
36
ref
cons
442
ref
13
ref
0
ref
438
remove
456
remove
nil
cons
cons
opType
constTerm
397
ref
0
ref
439
remove
459
remove
cons
opType
constTerm
444
remove
appTerm
appTerm
443
ref
appTerm
absTerm
470
def
443
remove
appTerm
471
def
betaConv
nil
457
remove
470
ref
appTerm
472
def
axiom
nil
96
ref
472
remove
nil
cons
cons
97
ref
471
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
460
remove
461
remove
470
remove
nil
cons
cons
462
remove
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
473
def
subst
subst
appThm
26
ref
refl
appThm
401
ref
28
ref
appTerm
474
def
refl
appThm
nil
8
ref
474
ref
nil
cons
475
def
cons
nil
cons
nil
cons
cons
248
remove
subst
trans
trans
476
def
appThm
29
ref
474
ref
appTerm
26
ref
appTerm
477
def
refl
appThm
nil
175
ref
477
ref
nil
cons
cons
nil
cons
nil
cons
cons
181
ref
subst
trans
absThm
appThm
264
ref
trans
absThm
appThm
264
ref
trans
sym
58
ref
eqMp
nil
11
ref
8
ref
11
ref
12
ref
15
ref
392
ref
0
ref
468
remove
22
remove
cons
opType
constTerm
469
remove
appTerm
478
def
26
ref
appTerm
28
ref
appTerm
appTerm
477
remove
appTerm
absTerm
appTerm
absTerm
appTerm
thm
238
ref
167
ref
63
remove
250
remove
476
remove
subst
nil
167
ref
402
ref
nil
cons
479
def
cons
nil
cons
nil
cons
cons
480
def
254
remove
subst
trans
appThm
402
ref
refl
481
def
appThm
nil
175
remove
479
remove
cons
nil
cons
nil
cons
cons
181
remove
subst
trans
absThm
appThm
264
ref
trans
sym
58
ref
eqMp
nil
11
ref
167
ref
15
ref
478
remove
85
ref
appTerm
171
ref
appTerm
appTerm
402
ref
appTerm
absTerm
appTerm
thm
94
ref
refl
80
ref
391
ref
72
ref
238
ref
167
ref
74
ref
84
remove
402
ref
appTerm
482
def
appTerm
483
def
refl
nil
390
ref
397
remove
0
ref
77
remove
412
remove
cons
opType
constTerm
81
remove
appTerm
484
def
nil
cons
cons
nil
cons
nil
cons
cons
415
ref
subst
79
remove
refl
68
ref
"B"
75
remove
cons
434
remove
cons
cons
36
ref
cons
473
remove
subst
appThm
419
remove
appThm
481
ref
appThm
trans
appThm
nil
164
ref
482
remove
nil
cons
cons
nil
cons
nil
cons
cons
289
ref
subst
trans
absThm
appThm
264
ref
trans
absThm
appThm
420
ref
trans
absThm
appThm
255
ref
277
remove
263
ref
subst
subst
trans
sym
58
ref
eqMp
nil
94
remove
80
remove
89
ref
72
ref
11
ref
167
ref
483
remove
393
remove
484
remove
appTerm
83
ref
appTerm
171
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
thm
389
remove
390
ref
391
ref
72
ref
238
ref
167
ref
284
ref
480
ref
415
ref
subst
416
ref
167
ref
15
ref
401
ref
402
ref
appTerm
appTerm
171
ref
appTerm
absTerm
485
def
171
ref
appTerm
486
def
betaConv
nil
11
ref
485
ref
appTerm
487
def
axiom
nil
96
ref
487
remove
nil
cons
cons
97
ref
486
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
35
ref
7
ref
485
remove
nil
cons
cons
177
ref
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
appThm
trans
appThm
400
ref
171
ref
appTerm
488
def
refl
appThm
nil
164
ref
488
ref
nil
cons
cons
nil
cons
nil
cons
cons
289
ref
subst
trans
absThm
appThm
264
ref
trans
absThm
appThm
420
ref
trans
absThm
appThm
422
remove
trans
sym
58
ref
eqMp
nil
388
ref
390
ref
89
ref
72
ref
11
ref
167
ref
74
ref
396
ref
402
ref
appTerm
appTerm
488
remove
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
thm
nil
414
ref
390
ref
89
ref
72
ref
11
ref
8
ref
11
ref
12
ref
74
ref
396
ref
30
ref
appTerm
appTerm
489
def
395
remove
396
ref
28
ref
appTerm
490
def
appTerm
26
ref
appTerm
appTerm
absTerm
491
def
appTerm
492
def
absTerm
493
def
appTerm
494
def
absTerm
495
def
appTerm
496
def
absTerm
497
def
nil
cons
cons
nil
cons
nil
cons
cons
421
remove
54
ref
subst
498
def
subst
390
ref
nil
56
ref
496
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
163
ref
495
remove
nil
cons
cons
nil
cons
nil
cons
cons
280
ref
subst
72
ref
nil
56
ref
494
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
7
ref
493
remove
nil
cons
cons
nil
cons
nil
cons
cons
55
ref
subst
8
ref
nil
56
ref
492
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
7
ref
491
remove
nil
cons
cons
nil
cons
nil
cons
cons
55
ref
subst
12
ref
284
ref
nil
167
ref
30
ref
nil
cons
cons
nil
cons
nil
cons
cons
415
ref
subst
499
def
416
remove
12
ref
15
remove
401
ref
30
remove
appTerm
appTerm
29
remove
401
remove
26
ref
appTerm
500
def
appTerm
474
ref
appTerm
501
def
appTerm
absTerm
502
def
26
ref
appTerm
503
def
betaConv
8
ref
11
ref
502
ref
appTerm
504
def
absTerm
505
def
28
remove
appTerm
506
def
betaConv
nil
11
ref
505
ref
appTerm
507
def
axiom
nil
96
ref
507
remove
nil
cons
cons
97
ref
506
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
35
ref
7
ref
505
remove
nil
cons
cons
247
remove
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
504
remove
nil
cons
cons
97
ref
503
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
35
ref
7
ref
502
remove
nil
cons
cons
179
remove
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
appThm
508
def
nil
12
ref
475
remove
cons
8
ref
500
ref
nil
cons
cons
417
remove
cons
cons
509
def
nil
cons
cons
309
remove
subst
trans
trans
appThm
nil
168
remove
72
ref
490
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
415
ref
subst
431
remove
nil
467
remove
nil
cons
nil
cons
cons
415
ref
subst
510
def
appThm
500
ref
refl
appThm
trans
appThm
nil
164
ref
399
remove
400
ref
474
remove
appTerm
511
def
appTerm
500
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
289
ref
subst
trans
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
388
ref
497
remove
appTerm
thm
nil
312
remove
313
ref
388
remove
390
ref
89
ref
72
ref
11
ref
8
ref
11
ref
12
ref
98
ref
102
ref
89
ref
314
ref
74
ref
315
ref
316
ref
appTerm
83
ref
appTerm
appTerm
316
ref
appTerm
absTerm
512
def
appTerm
513
def
appTerm
514
def
89
ref
319
ref
89
ref
320
ref
43
ref
48
ref
74
ref
324
remove
394
ref
323
ref
appTerm
154
ref
appTerm
appTerm
appTerm
394
ref
325
remove
appTerm
154
ref
appTerm
appTerm
absTerm
515
def
appTerm
516
def
absTerm
517
def
appTerm
518
def
absTerm
519
def
appTerm
520
def
appTerm
521
def
appTerm
489
remove
315
ref
490
remove
appTerm
396
remove
26
remove
appTerm
appTerm
appTerm
522
def
appTerm
523
def
absTerm
524
def
appTerm
525
def
absTerm
526
def
appTerm
527
def
absTerm
528
def
appTerm
529
def
absTerm
530
def
appTerm
531
def
absTerm
532
def
nil
cons
cons
nil
cons
nil
cons
cons
345
remove
subst
313
ref
nil
56
ref
531
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
414
remove
530
remove
nil
cons
cons
nil
cons
nil
cons
cons
498
remove
subst
390
remove
nil
56
ref
529
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
163
ref
528
remove
nil
cons
cons
nil
cons
nil
cons
cons
280
remove
subst
72
remove
nil
56
ref
527
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
7
ref
526
remove
nil
cons
cons
nil
cons
nil
cons
cons
55
ref
subst
8
remove
nil
56
ref
525
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
7
ref
524
remove
nil
cons
cons
nil
cons
nil
cons
cons
55
ref
subst
12
remove
nil
56
ref
523
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
96
ref
521
remove
nil
cons
533
def
cons
97
ref
522
remove
nil
cons
534
def
cons
nil
cons
cons
nil
cons
cons
535
def
113
ref
subst
535
remove
158
ref
subst
nil
129
ref
513
remove
nil
cons
536
def
cons
130
ref
520
remove
nil
cons
537
def
cons
nil
cons
cons
nil
cons
cons
538
def
142
ref
subst
538
remove
352
remove
subst
284
ref
499
remove
508
remove
trans
appThm
356
remove
510
remove
appThm
169
remove
415
ref
subst
appThm
appThm
sym
236
ref
391
ref
314
ref
284
ref
512
ref
316
ref
appTerm
539
def
betaConv
nil
96
ref
536
remove
cons
97
ref
539
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
162
ref
163
ref
512
remove
nil
cons
cons
359
ref
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
appThm
316
ref
refl
540
def
appThm
nil
359
remove
nil
cons
cons
289
ref
subst
trans
absThm
appThm
420
ref
trans
appThm
237
ref
48
ref
391
ref
319
ref
391
ref
320
ref
284
ref
315
ref
323
ref
appTerm
541
def
refl
nil
432
ref
376
ref
cons
nil
cons
nil
cons
cons
464
ref
subst
appThm
nil
320
ref
376
remove
cons
319
ref
378
remove
cons
nil
cons
cons
nil
cons
cons
515
ref
154
ref
appTerm
542
def
betaConv
517
ref
323
ref
appTerm
543
def
betaConv
519
ref
322
ref
appTerm
544
def
betaConv
nil
96
ref
537
remove
cons
97
ref
544
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
162
ref
163
ref
519
remove
nil
cons
cons
377
remove
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
518
remove
nil
cons
cons
97
ref
543
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
162
remove
163
remove
517
remove
nil
cons
cons
379
remove
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
516
remove
nil
cons
cons
97
ref
542
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
219
ref
44
ref
515
remove
nil
cons
cons
375
remove
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
subst
trans
appThm
nil
432
remove
541
ref
322
ref
appTerm
545
def
nil
cons
cons
nil
cons
nil
cons
cons
464
remove
subst
appThm
nil
164
ref
394
remove
545
ref
appTerm
154
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
289
remove
subst
trans
absThm
appThm
420
ref
trans
absThm
appThm
420
remove
trans
absThm
appThm
466
remove
trans
appThm
255
ref
56
ref
40
remove
102
ref
49
remove
appTerm
57
ref
appTerm
appTerm
57
ref
appTerm
absTerm
546
def
57
remove
appTerm
547
def
betaConv
nil
258
remove
546
ref
appTerm
548
def
axiom
nil
96
ref
548
remove
nil
cons
cons
97
ref
547
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
260
remove
261
remove
546
remove
nil
cons
cons
262
remove
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
subst
trans
sym
58
ref
eqMp
nil
96
ref
514
remove
43
ref
48
ref
89
ref
319
ref
89
remove
320
ref
74
ref
541
remove
398
remove
154
ref
appTerm
549
def
322
ref
appTerm
550
def
appTerm
appTerm
549
ref
545
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
nil
cons
cons
97
ref
74
ref
400
ref
501
remove
appTerm
appTerm
551
def
315
ref
511
ref
appTerm
400
remove
500
remove
appTerm
552
def
appTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
235
ref
236
ref
391
ref
314
remove
284
ref
"_16135"
71
ref
var
553
def
"_16136"
71
remove
var
554
def
315
remove
554
ref
varTerm
appTerm
555
def
553
remove
varTerm
appTerm
absTerm
absTerm
556
def
83
ref
appTerm
betaConv
540
ref
appThm
554
ref
555
ref
83
remove
appTerm
absTerm
316
remove
appTerm
betaConv
trans
appThm
540
remove
appThm
absThm
appThm
appThm
237
ref
48
ref
391
ref
319
remove
391
remove
320
remove
284
remove
556
ref
550
ref
appTerm
betaConv
323
ref
refl
557
def
appThm
554
ref
555
ref
550
remove
appTerm
absTerm
323
ref
appTerm
betaConv
trans
appThm
549
remove
refl
556
ref
322
ref
appTerm
betaConv
557
remove
appThm
554
ref
555
ref
322
remove
appTerm
absTerm
323
remove
appTerm
betaConv
trans
appThm
appThm
absThm
appThm
absThm
appThm
absThm
appThm
appThm
appThm
551
remove
refl
556
ref
552
ref
appTerm
betaConv
511
ref
refl
appThm
554
remove
555
remove
552
remove
appTerm
absTerm
511
remove
appTerm
betaConv
trans
appThm
appThm
nil
313
remove
556
remove
nil
cons
cons
509
remove
cons
nil
cons
cons
382
remove
subst
eqMp
eqMp
eqMp
proveHyp
proveHyp
eqMp
nil
129
ref
533
remove
cons
130
ref
534
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
383
remove
532
remove
appTerm
thm
9
ref
0
ref
0
ref
"Number.Natural.natural"
typeOp
nil
opType
558
def
5
ref
cons
opType
559
def
5
ref
cons
opType
constTerm
560
def
refl
561
def
"k"
558
ref
var
562
def
13
ref
0
ref
558
ref
559
ref
nil
cons
cons
opType
constTerm
563
def
refl
564
def
nil
"b"
558
ref
var
562
ref
varTerm
565
def
nil
cons
566
def
cons
567
def
"f"
0
ref
1
ref
0
ref
558
ref
558
ref
nil
cons
568
def
cons
opType
569
def
nil
cons
570
def
cons
opType
571
def
var
48
ref
"n"
558
ref
var
572
def
"Number.Natural.suc"
const
569
ref
constTerm
573
def
572
ref
varTerm
574
def
appTerm
575
def
absTerm
absTerm
576
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
577
def
68
remove
"B"
568
ref
cons
578
def
nil
cons
cons
36
ref
cons
579
def
166
remove
subst
subst
appThm
"Number.Natural.+"
const
0
ref
558
ref
570
remove
cons
opType
constTerm
580
def
refl
581
def
nil
563
ref
"Data.List.length"
const
0
ref
3
remove
568
ref
cons
opType
582
def
constTerm
583
def
85
ref
appTerm
584
def
appTerm
"Number.Natural.zero"
const
558
ref
constTerm
585
def
appTerm
axiom
appThm
565
ref
refl
586
def
appThm
nil
572
ref
566
ref
cons
587
def
nil
cons
nil
cons
cons
572
ref
563
ref
580
ref
585
remove
appTerm
574
ref
appTerm
appTerm
574
ref
appTerm
absTerm
588
def
574
ref
appTerm
589
def
betaConv
nil
560
ref
588
ref
appTerm
590
def
axiom
nil
96
ref
590
remove
nil
cons
cons
97
ref
589
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
"A"
568
ref
cons
591
def
nil
cons
592
def
"P"
559
remove
var
593
def
588
remove
nil
cons
cons
"x"
558
ref
var
594
def
574
ref
nil
cons
cons
nil
cons
595
def
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
subst
trans
appThm
nil
594
ref
566
remove
cons
nil
cons
596
def
nil
cons
cons
592
ref
36
ref
cons
597
def
180
remove
subst
598
def
subst
trans
absThm
appThm
255
remove
597
remove
263
remove
subst
subst
599
def
trans
sym
58
ref
eqMp
nil
96
ref
560
ref
562
ref
563
ref
16
remove
0
ref
571
remove
0
ref
558
ref
582
remove
nil
cons
cons
opType
nil
cons
600
def
cons
opType
constTerm
601
def
576
ref
appTerm
565
ref
appTerm
602
def
85
ref
appTerm
appTerm
580
ref
584
remove
appTerm
565
ref
appTerm
appTerm
absTerm
appTerm
603
def
nil
cons
cons
97
ref
43
ref
184
ref
11
ref
185
ref
98
remove
560
ref
562
ref
563
ref
602
ref
186
ref
appTerm
appTerm
580
ref
583
ref
186
ref
appTerm
604
def
appTerm
565
ref
appTerm
605
def
appTerm
absTerm
606
def
appTerm
607
def
appTerm
560
ref
562
ref
563
ref
602
ref
192
ref
appTerm
appTerm
580
ref
583
ref
192
ref
appTerm
608
def
appTerm
565
ref
appTerm
appTerm
absTerm
appTerm
609
def
appTerm
610
def
absTerm
611
def
appTerm
612
def
absTerm
613
def
appTerm
614
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
158
ref
subst
proveHyp
nil
44
ref
613
remove
nil
cons
cons
nil
cons
nil
cons
cons
54
remove
subst
184
ref
nil
56
ref
612
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
7
ref
611
remove
nil
cons
cons
nil
cons
nil
cons
cons
55
remove
subst
185
ref
nil
56
remove
610
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
remove
subst
nil
96
ref
607
remove
nil
cons
615
def
cons
616
def
97
ref
609
remove
nil
cons
617
def
cons
nil
cons
cons
nil
cons
cons
618
def
113
remove
subst
618
remove
158
remove
subst
561
ref
562
ref
564
ref
577
remove
579
ref
223
remove
subst
subst
576
remove
190
ref
appTerm
betaConv
606
ref
565
ref
appTerm
619
def
betaConv
nil
616
remove
97
ref
619
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
592
ref
593
ref
606
remove
nil
cons
cons
596
ref
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
appThm
nil
"f"
569
remove
var
573
ref
nil
cons
cons
"y"
558
ref
var
620
def
605
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
578
remove
592
ref
cons
36
ref
cons
435
ref
74
remove
48
ref
"f"
384
ref
var
621
def
varTerm
622
def
154
ref
appTerm
absTerm
446
ref
appTerm
appTerm
622
ref
446
ref
appTerm
appTerm
absTerm
623
def
446
remove
appTerm
624
def
betaConv
621
remove
43
ref
623
ref
appTerm
625
def
absTerm
626
def
622
ref
appTerm
627
def
betaConv
nil
9
remove
0
ref
0
ref
384
ref
5
ref
cons
opType
628
def
5
ref
cons
opType
constTerm
626
ref
appTerm
629
def
axiom
nil
96
ref
629
remove
nil
cons
cons
97
ref
627
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
"A"
385
remove
cons
nil
cons
"P"
628
remove
var
626
remove
nil
cons
cons
"x"
384
remove
var
622
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
625
remove
nil
cons
cons
97
ref
624
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
219
ref
44
ref
623
remove
nil
cons
cons
463
remove
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
subst
subst
trans
trans
appThm
581
ref
185
ref
563
ref
608
remove
appTerm
573
ref
604
ref
appTerm
appTerm
absTerm
630
def
186
ref
appTerm
631
def
betaConv
184
ref
11
ref
630
ref
appTerm
632
def
absTerm
633
def
190
remove
appTerm
634
def
betaConv
nil
43
remove
633
ref
appTerm
635
def
axiom
nil
96
ref
635
remove
nil
cons
cons
97
ref
634
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
219
remove
44
remove
633
remove
nil
cons
cons
220
remove
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
632
remove
nil
cons
cons
97
ref
631
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
35
ref
7
ref
630
remove
nil
cons
cons
222
remove
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
appThm
586
ref
appThm
nil
587
remove
"m"
558
ref
var
636
def
604
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
572
ref
563
ref
580
ref
573
ref
636
ref
varTerm
637
def
appTerm
appTerm
574
ref
appTerm
appTerm
573
ref
580
ref
637
ref
appTerm
574
ref
appTerm
appTerm
appTerm
absTerm
638
def
574
remove
appTerm
639
def
betaConv
636
remove
560
ref
638
ref
appTerm
640
def
absTerm
641
def
637
ref
appTerm
642
def
betaConv
nil
560
ref
641
ref
appTerm
643
def
axiom
nil
96
ref
643
remove
nil
cons
cons
97
ref
642
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
592
ref
593
ref
641
remove
nil
cons
cons
594
ref
637
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
640
remove
nil
cons
cons
97
ref
639
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
592
ref
593
ref
638
remove
nil
cons
cons
595
remove
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
subst
trans
appThm
nil
594
ref
573
ref
605
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
598
ref
subst
trans
absThm
appThm
599
ref
trans
sym
58
ref
eqMp
eqMp
nil
129
remove
615
remove
cons
130
remove
617
remove
cons
nil
cons
cons
nil
cons
cons
142
remove
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
96
ref
102
remove
603
remove
appTerm
614
remove
appTerm
nil
cons
cons
97
ref
11
ref
167
ref
560
ref
562
ref
563
ref
602
remove
171
ref
appTerm
appTerm
580
remove
583
ref
171
ref
appTerm
644
def
appTerm
565
ref
appTerm
645
def
appTerm
absTerm
646
def
appTerm
647
def
absTerm
648
def
appTerm
649
def
nil
cons
650
def
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
235
ref
236
remove
648
ref
85
remove
appTerm
betaConv
appThm
237
remove
184
remove
238
ref
185
remove
235
remove
648
ref
186
remove
appTerm
betaConv
appThm
648
ref
192
remove
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
238
ref
167
ref
648
ref
171
ref
appTerm
651
def
betaConv
652
def
absThm
appThm
appThm
nil
239
remove
648
remove
nil
cons
653
def
cons
nil
cons
nil
cons
cons
245
remove
subst
eqMp
eqMp
654
def
nil
649
remove
thm
238
remove
167
ref
561
remove
562
ref
564
remove
nil
567
remove
"f"
0
ref
558
remove
0
ref
1
remove
568
ref
cons
opType
nil
cons
cons
opType
655
def
var
656
def
572
remove
48
ref
575
remove
absTerm
absTerm
657
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
579
remove
415
remove
subst
subst
601
remove
refl
433
remove
591
remove
"C"
568
remove
cons
nil
cons
cons
cons
36
remove
cons
nil
13
remove
0
ref
440
ref
0
ref
440
remove
5
remove
cons
opType
nil
cons
cons
opType
constTerm
441
remove
appTerm
442
remove
164
remove
435
remove
447
remove
absTerm
absTerm
absTerm
appTerm
axiom
subst
657
ref
refl
appThm
656
ref
48
ref
620
ref
656
remove
varTerm
620
ref
varTerm
658
def
appTerm
154
ref
appTerm
absTerm
absTerm
absTerm
657
ref
appTerm
betaConv
48
ref
620
remove
657
ref
658
ref
appTerm
betaConv
159
remove
appThm
48
remove
573
remove
658
remove
appTerm
absTerm
154
remove
appTerm
betaConv
trans
absThm
absThm
trans
trans
appThm
586
ref
appThm
481
remove
appThm
480
remove
646
ref
565
ref
appTerm
659
def
betaConv
652
remove
654
remove
nil
96
ref
650
remove
cons
97
ref
651
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
35
ref
7
ref
653
remove
cons
177
ref
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
nil
96
ref
647
remove
nil
cons
cons
97
ref
659
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
592
remove
593
remove
646
remove
nil
cons
cons
596
remove
cons
nil
cons
cons
160
ref
subst
eqMp
eqMp
subst
581
remove
167
ref
563
ref
583
remove
402
remove
appTerm
appTerm
644
remove
appTerm
absTerm
660
def
171
ref
appTerm
661
def
betaConv
nil
11
ref
660
ref
appTerm
662
def
axiom
nil
96
remove
662
remove
nil
cons
cons
97
remove
661
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
remove
subst
proveHyp
35
remove
7
remove
660
remove
nil
cons
cons
177
remove
cons
nil
cons
cons
160
remove
subst
eqMp
eqMp
appThm
586
remove
appThm
trans
trans
trans
appThm
645
ref
refl
appThm
nil
594
remove
645
ref
nil
cons
cons
nil
cons
nil
cons
cons
598
remove
subst
trans
absThm
appThm
599
remove
trans
absThm
appThm
264
remove
trans
sym
58
remove
eqMp
nil
11
remove
167
remove
560
remove
562
remove
563
remove
392
remove
0
remove
655
remove
600
remove
cons
opType
constTerm
657
remove
appTerm
565
remove
appTerm
171
remove
appTerm
appTerm
645
remove
appTerm
absTerm
appTerm
absTerm
appTerm
thm