6
version
nil
"P"
"->"
typeOp
0
def
"Data.Sum.+"
typeOp
"A"
varType
1
def
"B"
varType
2
def
nil
cons
3
def
cons
4
def
opType
5
def
"bool"
typeOp
nil
opType
6
def
nil
cons
7
def
cons
opType
8
def
var
9
def
"x"
5
ref
var
10
def
"="
const
11
def
0
ref
5
ref
8
ref
nil
cons
12
def
cons
opType
constTerm
13
def
"Data.Sum.case.left.right"
const
14
def
0
ref
0
ref
1
ref
5
ref
nil
cons
15
def
cons
opType
16
def
0
ref
0
ref
2
ref
15
ref
cons
opType
17
def
0
ref
5
ref
15
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
"Data.Sum.left"
const
16
ref
constTerm
18
def
appTerm
"Data.Sum.right"
const
17
ref
constTerm
19
def
appTerm
20
def
10
ref
varTerm
21
def
appTerm
appTerm
21
ref
appTerm
22
def
absTerm
23
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
15
ref
cons
nil
cons
24
def
nil
nil
cons
25
def
cons
26
def
11
ref
0
ref
6
ref
0
ref
6
ref
7
ref
cons
opType
27
def
nil
cons
cons
opType
28
def
constTerm
29
def
"Data.Bool.!"
const
30
def
0
ref
0
ref
1
ref
7
ref
cons
opType
31
def
7
ref
cons
opType
32
def
constTerm
33
def
"P"
31
ref
var
34
def
varTerm
35
def
appTerm
36
def
appTerm
refl
"p"
31
ref
var
37
def
11
ref
0
ref
31
ref
32
ref
nil
cons
cons
opType
constTerm
37
ref
varTerm
38
def
appTerm
"x"
1
ref
var
39
def
"Data.Bool.T"
const
6
ref
constTerm
40
def
absTerm
41
def
appTerm
absTerm
42
def
35
ref
appTerm
betaConv
43
def
appThm
nil
11
ref
0
ref
32
ref
0
ref
32
ref
7
ref
cons
opType
44
def
nil
cons
cons
opType
constTerm
45
def
33
ref
appTerm
42
remove
appTerm
axiom
35
ref
refl
46
def
appThm
47
def
eqMp
sym
48
def
subst
49
def
subst
10
ref
nil
"t"
6
ref
var
50
def
22
ref
nil
cons
51
def
cons
nil
cons
nil
cons
cons
29
ref
50
ref
varTerm
52
def
appTerm
53
def
40
ref
appTerm
54
def
assume
sym
nil
40
ref
axiom
55
def
eqMp
52
ref
assume
55
ref
deductAntisym
deductAntisym
56
def
subst
10
ref
"Data.Bool.\\/"
const
28
ref
constTerm
57
def
"Data.Bool.?"
const
58
def
32
ref
constTerm
59
def
"a"
1
ref
var
60
def
13
ref
21
ref
appTerm
61
def
18
ref
60
ref
varTerm
62
def
appTerm
63
def
appTerm
64
def
absTerm
65
def
appTerm
66
def
appTerm
58
ref
0
ref
0
ref
2
ref
7
ref
cons
opType
67
def
7
ref
cons
opType
68
def
constTerm
69
def
"b"
2
ref
var
70
def
61
remove
19
ref
70
ref
varTerm
71
def
appTerm
72
def
appTerm
73
def
absTerm
74
def
appTerm
75
def
appTerm
76
def
absTerm
77
def
21
ref
appTerm
78
def
betaConv
79
def
nil
34
ref
60
ref
57
ref
59
ref
"a'"
1
ref
var
80
def
13
ref
63
ref
appTerm
81
def
18
ref
80
ref
varTerm
82
def
appTerm
appTerm
83
def
absTerm
84
def
appTerm
85
def
appTerm
69
ref
70
ref
81
ref
72
ref
appTerm
86
def
absTerm
appTerm
87
def
appTerm
88
def
absTerm
89
def
nil
cons
cons
nil
cons
nil
cons
cons
48
ref
subst
60
ref
nil
50
ref
88
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
84
ref
62
ref
appTerm
betaConv
sym
63
ref
refl
eqMp
"A"
1
ref
nil
cons
90
def
cons
91
def
nil
cons
92
def
34
ref
84
remove
nil
cons
cons
39
ref
62
ref
nil
cons
cons
nil
cons
93
def
cons
nil
cons
cons
29
ref
59
ref
35
ref
appTerm
94
def
appTerm
95
def
refl
37
ref
30
ref
0
ref
27
ref
7
ref
cons
opType
96
def
constTerm
97
def
"q"
6
ref
var
98
def
"Data.Bool.==>"
const
28
ref
constTerm
99
def
33
ref
39
ref
99
ref
38
ref
39
ref
varTerm
100
def
appTerm
101
def
appTerm
98
ref
varTerm
102
def
appTerm
absTerm
appTerm
appTerm
102
ref
appTerm
absTerm
appTerm
absTerm
103
def
35
ref
appTerm
betaConv
appThm
nil
45
remove
59
ref
appTerm
103
remove
appTerm
axiom
46
remove
appThm
eqMp
104
def
sym
nil
"P"
27
ref
var
105
def
"Q"
6
ref
var
106
def
99
ref
33
ref
39
ref
99
ref
35
ref
100
ref
appTerm
107
def
appTerm
108
def
106
ref
varTerm
109
def
appTerm
absTerm
110
def
appTerm
111
def
appTerm
109
ref
appTerm
112
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
7
ref
cons
nil
cons
113
def
25
ref
cons
114
def
48
ref
subst
115
def
subst
106
ref
nil
50
ref
112
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
"p"
6
ref
var
116
def
111
remove
nil
cons
117
def
cons
118
def
98
ref
109
ref
nil
cons
119
def
cons
nil
cons
120
def
cons
nil
cons
cons
121
def
29
ref
99
ref
116
ref
varTerm
122
def
appTerm
123
def
102
ref
appTerm
124
def
appTerm
refl
116
ref
98
ref
29
ref
"Data.Bool./\\"
const
28
ref
constTerm
125
def
122
ref
appTerm
126
def
102
ref
appTerm
127
def
appTerm
128
def
122
ref
appTerm
absTerm
129
def
absTerm
130
def
122
ref
appTerm
betaConv
102
ref
refl
131
def
appThm
129
remove
102
ref
appTerm
betaConv
trans
appThm
nil
11
ref
0
ref
28
ref
0
ref
28
ref
7
ref
cons
opType
132
def
nil
cons
cons
opType
constTerm
133
def
99
ref
appTerm
130
remove
appTerm
axiom
122
ref
refl
134
def
appThm
131
ref
appThm
eqMp
135
def
sym
136
def
subst
121
ref
29
ref
refl
137
def
"f"
28
remove
var
138
def
138
ref
varTerm
139
def
122
ref
appTerm
102
ref
appTerm
absTerm
140
def
116
ref
98
ref
102
ref
absTerm
141
def
absTerm
142
def
appTerm
betaConv
142
ref
122
ref
appTerm
betaConv
131
ref
appThm
141
ref
102
ref
appTerm
betaConv
trans
trans
appThm
138
ref
139
ref
40
ref
appTerm
40
ref
appTerm
absTerm
143
def
142
ref
appTerm
betaConv
142
ref
40
ref
appTerm
betaConv
40
ref
refl
144
def
appThm
141
ref
40
ref
appTerm
betaConv
trans
trans
145
def
appThm
128
remove
refl
98
ref
11
ref
0
ref
132
ref
0
ref
132
remove
7
ref
cons
opType
nil
cons
cons
opType
constTerm
146
def
140
remove
appTerm
143
ref
appTerm
absTerm
147
def
102
ref
appTerm
betaConv
appThm
11
ref
0
ref
27
ref
96
remove
nil
cons
cons
opType
constTerm
148
def
126
remove
appTerm
refl
116
ref
147
remove
absTerm
149
def
122
ref
appTerm
betaConv
appThm
nil
133
ref
125
ref
appTerm
149
ref
appTerm
axiom
150
def
134
remove
appThm
eqMp
131
remove
appThm
eqMp
151
def
127
remove
assume
eqMp
142
ref
refl
152
def
appThm
eqMp
sym
55
ref
eqMp
153
def
151
remove
sym
138
ref
139
ref
refl
nil
50
ref
122
ref
nil
cons
154
def
cons
nil
cons
nil
cons
cons
155
def
56
ref
subst
122
ref
assume
156
def
eqMp
appThm
nil
50
ref
102
ref
nil
cons
157
def
cons
nil
cons
nil
cons
cons
158
def
56
ref
subst
102
ref
assume
159
def
eqMp
appThm
absThm
eqMp
160
def
deductAntisym
161
def
subst
nil
116
ref
107
ref
nil
cons
162
def
cons
120
ref
cons
nil
cons
cons
136
ref
160
remove
nil
"P"
6
ref
var
163
def
154
ref
cons
106
ref
157
ref
cons
nil
cons
164
def
cons
nil
cons
cons
137
ref
138
ref
139
remove
163
ref
varTerm
165
def
appTerm
166
def
109
ref
appTerm
absTerm
167
def
116
ref
98
ref
122
ref
absTerm
absTerm
168
def
appTerm
betaConv
168
ref
165
ref
appTerm
betaConv
109
ref
refl
169
def
appThm
98
ref
165
ref
absTerm
109
ref
appTerm
betaConv
trans
trans
appThm
143
ref
168
ref
appTerm
betaConv
168
ref
40
ref
appTerm
betaConv
144
remove
appThm
98
ref
40
ref
absTerm
40
ref
appTerm
betaConv
trans
trans
appThm
29
ref
125
ref
165
ref
appTerm
170
def
109
ref
appTerm
171
def
appTerm
refl
98
ref
146
remove
138
remove
166
remove
102
ref
appTerm
absTerm
appTerm
143
remove
appTerm
absTerm
109
ref
appTerm
betaConv
appThm
148
ref
170
remove
appTerm
refl
149
remove
165
ref
appTerm
betaConv
appThm
150
remove
165
ref
refl
172
def
appThm
eqMp
169
ref
appThm
eqMp
171
remove
assume
eqMp
173
def
168
remove
refl
appThm
eqMp
sym
55
ref
eqMp
174
def
subst
175
def
deductAntisym
eqMp
135
remove
124
ref
assume
eqMp
sym
156
ref
eqMp
153
remove
proveHyp
deductAntisym
176
def
subst
110
ref
100
ref
appTerm
177
def
betaConv
nil
118
ref
98
ref
177
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
92
ref
34
ref
110
remove
nil
cons
cons
39
ref
100
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
116
ref
36
ref
nil
cons
178
def
cons
98
ref
162
ref
cons
nil
cons
cons
nil
cons
cons
179
def
136
ref
subst
179
remove
161
ref
subst
29
ref
107
ref
appTerm
refl
41
remove
100
ref
appTerm
betaConv
appThm
43
remove
47
remove
36
remove
assume
eqMp
eqMp
100
ref
refl
180
def
appThm
eqMp
sym
55
ref
eqMp
eqMp
nil
163
ref
178
remove
cons
106
ref
162
remove
cons
nil
cons
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
181
def
subst
eqMp
eqMp
eqMp
eqMp
nil
163
ref
117
remove
cons
182
def
106
ref
119
ref
cons
nil
cons
183
def
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
184
def
subst
proveHyp
nil
163
ref
85
remove
nil
cons
cons
106
ref
87
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
29
ref
57
ref
165
ref
appTerm
185
def
109
ref
appTerm
186
def
appTerm
refl
98
ref
97
ref
"r"
6
ref
var
187
def
99
ref
99
ref
165
ref
appTerm
188
def
187
ref
varTerm
189
def
appTerm
appTerm
190
def
99
ref
99
ref
102
ref
appTerm
191
def
189
ref
appTerm
appTerm
189
ref
appTerm
192
def
appTerm
absTerm
appTerm
absTerm
109
ref
appTerm
betaConv
appThm
148
ref
185
remove
appTerm
refl
116
ref
98
ref
97
ref
187
ref
99
ref
123
ref
189
ref
appTerm
appTerm
192
remove
appTerm
absTerm
appTerm
absTerm
absTerm
193
def
165
ref
appTerm
betaConv
appThm
nil
133
remove
57
ref
appTerm
193
remove
appTerm
axiom
172
ref
appThm
eqMp
169
ref
appThm
eqMp
194
def
sym
195
def
nil
105
ref
50
ref
99
ref
188
ref
52
ref
appTerm
196
def
appTerm
99
ref
99
ref
109
ref
appTerm
197
def
52
ref
appTerm
198
def
appTerm
52
ref
appTerm
199
def
appTerm
200
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
115
remove
subst
201
def
50
ref
nil
50
ref
200
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
202
def
nil
116
ref
196
ref
nil
cons
203
def
cons
98
ref
199
remove
nil
cons
204
def
cons
nil
cons
cons
nil
cons
cons
205
def
136
ref
subst
206
def
205
remove
161
ref
subst
207
def
nil
116
ref
198
ref
nil
cons
208
def
cons
98
ref
52
ref
nil
cons
209
def
cons
nil
cons
210
def
cons
nil
cons
cons
211
def
136
ref
subst
212
def
211
remove
161
ref
subst
213
def
nil
116
ref
165
ref
nil
cons
214
def
cons
215
def
210
ref
cons
nil
cons
cons
176
ref
subst
196
remove
assume
eqMp
eqMp
nil
163
ref
208
remove
cons
106
ref
209
ref
cons
nil
cons
cons
nil
cons
cons
174
ref
subst
216
def
deductAntisym
eqMp
eqMp
nil
163
ref
203
remove
cons
106
ref
204
remove
cons
nil
cons
cons
nil
cons
cons
174
ref
subst
217
def
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
subst
proveHyp
eqMp
absThm
eqMp
nil
116
ref
33
ref
89
remove
appTerm
218
def
nil
cons
cons
98
ref
30
ref
68
remove
constTerm
219
def
70
ref
57
ref
59
ref
60
ref
13
ref
72
ref
appTerm
220
def
63
ref
appTerm
absTerm
appTerm
221
def
appTerm
69
remove
"b'"
2
ref
var
222
def
220
remove
19
ref
222
ref
varTerm
223
def
appTerm
224
def
appTerm
225
def
absTerm
226
def
appTerm
227
def
appTerm
228
def
absTerm
229
def
appTerm
230
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
161
ref
subst
proveHyp
nil
"P"
67
ref
var
231
def
229
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
3
ref
cons
nil
cons
232
def
25
ref
cons
48
ref
subst
233
def
subst
70
ref
nil
50
ref
228
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
226
ref
71
ref
appTerm
betaConv
sym
72
ref
refl
eqMp
232
ref
231
ref
226
remove
nil
cons
cons
"x"
2
ref
var
234
def
71
ref
nil
cons
cons
nil
cons
235
def
cons
nil
cons
cons
184
ref
subst
proveHyp
nil
163
ref
221
remove
nil
cons
cons
106
ref
227
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
195
remove
201
remove
50
ref
202
remove
206
remove
207
remove
212
remove
213
remove
nil
116
ref
119
ref
cons
210
remove
cons
nil
cons
cons
176
ref
subst
198
remove
assume
eqMp
eqMp
216
remove
deductAntisym
eqMp
eqMp
217
remove
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
subst
proveHyp
eqMp
absThm
eqMp
eqMp
nil
116
ref
125
ref
218
remove
appTerm
230
remove
appTerm
nil
cons
cons
98
ref
30
ref
0
ref
8
ref
7
ref
cons
opType
236
def
constTerm
237
def
77
ref
appTerm
238
def
nil
cons
239
def
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
99
ref
refl
240
def
125
ref
refl
241
def
33
ref
refl
242
def
60
ref
77
ref
63
ref
appTerm
betaConv
absThm
appThm
appThm
219
ref
refl
243
def
70
ref
77
ref
72
ref
appTerm
betaConv
absThm
appThm
appThm
appThm
237
ref
refl
10
ref
79
remove
absThm
appThm
appThm
nil
"p"
8
ref
var
244
def
77
remove
nil
cons
245
def
cons
nil
cons
nil
cons
cons
244
ref
99
ref
125
ref
33
ref
60
ref
244
remove
varTerm
246
def
63
ref
appTerm
absTerm
appTerm
appTerm
219
ref
70
ref
246
ref
72
ref
appTerm
absTerm
appTerm
appTerm
appTerm
237
ref
10
ref
246
ref
21
ref
appTerm
absTerm
appTerm
appTerm
absTerm
247
def
246
ref
appTerm
248
def
betaConv
nil
30
ref
0
ref
236
ref
7
ref
cons
opType
constTerm
247
ref
appTerm
249
def
axiom
nil
116
ref
249
remove
nil
cons
cons
98
ref
248
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
"A"
12
remove
cons
nil
cons
"P"
236
remove
var
247
remove
nil
cons
cons
"x"
8
ref
var
246
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
250
def
nil
116
ref
239
remove
cons
98
ref
78
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
24
remove
9
ref
245
remove
cons
10
ref
21
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
251
def
nil
116
ref
76
remove
nil
cons
252
def
cons
253
def
98
ref
51
ref
cons
nil
cons
254
def
cons
nil
cons
cons
255
def
176
ref
subst
proveHyp
255
ref
136
ref
subst
255
remove
161
ref
subst
nil
231
ref
70
ref
99
ref
74
ref
71
ref
appTerm
256
def
appTerm
257
def
22
ref
appTerm
258
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
233
ref
subst
70
ref
nil
50
ref
258
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
116
ref
256
ref
nil
cons
259
def
cons
260
def
254
ref
cons
nil
cons
cons
261
def
136
ref
subst
261
remove
161
ref
subst
256
ref
betaConv
256
remove
assume
eqMp
262
def
nil
116
ref
73
ref
nil
cons
263
def
cons
264
def
254
ref
cons
nil
cons
cons
265
def
176
ref
subst
proveHyp
265
ref
136
ref
subst
265
remove
161
ref
subst
13
ref
refl
266
def
20
remove
refl
267
def
73
remove
assume
268
def
appThm
nil
"g"
17
remove
var
19
ref
nil
cons
cons
"f"
16
remove
var
18
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
269
def
91
ref
"B"
3
ref
cons
270
def
"C"
15
remove
cons
nil
cons
cons
cons
25
ref
cons
271
def
70
ref
11
ref
0
ref
"C"
varType
272
def
0
ref
272
ref
7
ref
cons
opType
nil
cons
cons
opType
constTerm
273
def
14
remove
0
ref
0
ref
1
ref
272
ref
nil
cons
274
def
cons
opType
275
def
0
ref
0
ref
2
ref
274
ref
cons
opType
276
def
0
ref
5
ref
274
ref
cons
opType
277
def
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
"f"
275
ref
var
278
def
varTerm
279
def
appTerm
"g"
276
ref
var
280
def
varTerm
281
def
appTerm
282
def
72
ref
appTerm
appTerm
281
ref
71
ref
appTerm
283
def
appTerm
absTerm
284
def
71
ref
appTerm
285
def
betaConv
280
ref
219
ref
284
ref
appTerm
286
def
absTerm
287
def
281
ref
appTerm
288
def
betaConv
278
ref
30
ref
0
ref
0
ref
276
ref
7
ref
cons
opType
289
def
7
ref
cons
opType
constTerm
290
def
287
ref
appTerm
291
def
absTerm
292
def
279
ref
appTerm
293
def
betaConv
nil
30
ref
0
ref
0
ref
275
ref
7
ref
cons
opType
294
def
7
ref
cons
opType
constTerm
295
def
292
ref
appTerm
296
def
axiom
nil
116
ref
296
remove
nil
cons
cons
98
ref
293
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
"A"
275
ref
nil
cons
cons
nil
cons
297
def
"P"
294
remove
var
298
def
292
remove
nil
cons
cons
"x"
275
remove
var
279
ref
nil
cons
cons
nil
cons
299
def
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
nil
116
ref
291
remove
nil
cons
cons
98
ref
288
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
"A"
276
ref
nil
cons
cons
nil
cons
300
def
"P"
289
remove
var
301
def
287
remove
nil
cons
cons
"x"
276
remove
var
281
ref
nil
cons
cons
nil
cons
302
def
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
nil
116
ref
286
remove
nil
cons
cons
98
ref
285
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
232
ref
231
ref
284
remove
nil
cons
cons
235
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
303
def
subst
subst
trans
appThm
268
ref
appThm
nil
10
ref
72
ref
nil
cons
cons
nil
cons
nil
cons
cons
26
remove
nil
50
ref
11
ref
0
ref
1
ref
31
ref
nil
cons
304
def
cons
opType
constTerm
305
def
100
ref
appTerm
100
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
180
remove
eqMp
306
def
subst
307
def
subst
trans
sym
55
ref
eqMp
eqMp
nil
163
ref
263
remove
cons
308
def
106
ref
51
ref
cons
nil
cons
309
def
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
163
ref
259
remove
cons
310
def
309
ref
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
116
ref
219
ref
234
ref
99
ref
74
ref
234
ref
varTerm
appTerm
appTerm
311
def
22
ref
appTerm
absTerm
appTerm
nil
cons
cons
98
ref
99
ref
75
ref
appTerm
312
def
22
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
232
ref
231
ref
74
remove
nil
cons
cons
313
def
309
ref
cons
nil
cons
cons
nil
118
remove
98
ref
99
ref
94
ref
appTerm
314
def
109
ref
appTerm
nil
cons
315
def
cons
nil
cons
cons
nil
cons
cons
316
def
136
ref
subst
316
remove
161
ref
subst
nil
116
ref
94
remove
nil
cons
317
def
cons
318
def
120
remove
cons
nil
cons
cons
319
def
136
ref
subst
319
remove
161
ref
subst
121
remove
176
ref
subst
98
ref
99
ref
33
ref
39
ref
108
remove
102
ref
appTerm
absTerm
appTerm
appTerm
102
ref
appTerm
absTerm
320
def
109
ref
appTerm
321
def
betaConv
nil
318
remove
98
ref
97
ref
320
ref
appTerm
322
def
nil
cons
323
def
cons
nil
cons
cons
nil
cons
cons
324
def
176
ref
subst
104
remove
nil
116
ref
95
remove
322
ref
appTerm
nil
cons
cons
98
ref
314
remove
322
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
324
remove
nil
116
ref
29
ref
122
ref
appTerm
325
def
102
ref
appTerm
326
def
nil
cons
327
def
cons
98
ref
124
remove
nil
cons
328
def
cons
nil
cons
cons
nil
cons
cons
329
def
136
ref
subst
329
remove
161
ref
subst
136
ref
161
ref
326
remove
assume
330
def
156
remove
eqMp
eqMp
175
remove
deductAntisym
eqMp
331
def
eqMp
nil
163
ref
327
remove
cons
106
ref
328
ref
cons
nil
cons
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
116
ref
323
remove
cons
98
ref
321
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
113
ref
105
ref
320
remove
nil
cons
cons
"x"
6
ref
var
332
def
119
remove
cons
nil
cons
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
163
ref
317
remove
cons
183
remove
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
nil
182
remove
106
ref
315
remove
cons
nil
cons
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
333
def
subst
eqMp
nil
34
ref
60
ref
99
ref
65
ref
62
ref
appTerm
334
def
appTerm
335
def
22
ref
appTerm
336
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
48
ref
subst
60
ref
nil
50
ref
336
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
116
ref
334
ref
nil
cons
337
def
cons
338
def
254
ref
cons
nil
cons
cons
339
def
136
ref
subst
339
remove
161
ref
subst
334
ref
betaConv
334
remove
assume
eqMp
340
def
nil
116
ref
64
ref
nil
cons
341
def
cons
342
def
254
remove
cons
nil
cons
cons
343
def
176
ref
subst
proveHyp
343
ref
136
ref
subst
343
remove
161
ref
subst
266
remove
267
remove
64
remove
assume
344
def
appThm
269
remove
271
remove
60
ref
273
ref
282
ref
63
ref
appTerm
appTerm
279
ref
62
ref
appTerm
345
def
appTerm
absTerm
346
def
62
ref
appTerm
347
def
betaConv
280
ref
33
ref
346
ref
appTerm
348
def
absTerm
349
def
281
ref
appTerm
350
def
betaConv
278
ref
290
ref
349
ref
appTerm
351
def
absTerm
352
def
279
ref
appTerm
353
def
betaConv
nil
295
ref
352
ref
appTerm
354
def
axiom
nil
116
ref
354
remove
nil
cons
cons
98
ref
353
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
297
ref
298
ref
352
remove
nil
cons
cons
299
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
nil
116
ref
351
remove
nil
cons
cons
98
ref
350
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
300
ref
301
ref
349
remove
nil
cons
cons
302
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
nil
116
ref
348
remove
nil
cons
cons
98
ref
347
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
92
ref
34
ref
346
remove
nil
cons
cons
93
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
355
def
subst
subst
trans
appThm
344
ref
appThm
nil
10
ref
63
ref
nil
cons
cons
nil
cons
nil
cons
cons
307
remove
subst
trans
sym
55
ref
eqMp
eqMp
nil
163
ref
341
remove
cons
356
def
309
ref
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
163
ref
337
remove
cons
357
def
309
ref
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
116
ref
33
ref
39
ref
99
ref
65
ref
100
ref
appTerm
appTerm
358
def
22
ref
appTerm
absTerm
appTerm
nil
cons
cons
98
ref
99
ref
66
ref
appTerm
359
def
22
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
92
ref
34
ref
65
remove
nil
cons
cons
360
def
309
ref
cons
nil
cons
cons
333
ref
subst
eqMp
nil
163
ref
66
remove
nil
cons
cons
361
def
106
ref
75
remove
nil
cons
cons
362
def
"R"
6
ref
var
363
def
51
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
116
ref
197
ref
363
ref
varTerm
364
def
appTerm
365
def
nil
cons
cons
98
ref
364
ref
nil
cons
366
def
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
nil
116
ref
188
ref
364
ref
appTerm
nil
cons
cons
98
ref
99
ref
365
remove
appTerm
364
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
187
remove
190
remove
99
ref
197
remove
189
ref
appTerm
appTerm
189
remove
appTerm
appTerm
absTerm
367
def
364
remove
appTerm
368
def
betaConv
194
remove
186
remove
assume
eqMp
nil
116
ref
97
ref
367
ref
appTerm
nil
cons
cons
98
ref
368
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
113
ref
105
ref
367
remove
nil
cons
cons
332
ref
366
remove
cons
nil
cons
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
eqMp
eqMp
369
def
subst
proveHyp
proveHyp
eqMp
nil
163
ref
252
remove
cons
370
def
309
remove
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
absThm
eqMp
nil
237
ref
23
remove
appTerm
thm
58
ref
0
ref
0
ref
0
ref
5
ref
"Number.Natural.natural"
typeOp
nil
opType
371
def
nil
cons
372
def
cons
opType
373
def
7
ref
cons
opType
374
def
7
ref
cons
opType
375
def
constTerm
376
def
refl
"fn"
373
ref
var
377
def
241
ref
242
ref
60
ref
11
ref
0
ref
371
ref
0
ref
371
ref
7
ref
cons
opType
378
def
nil
cons
379
def
cons
opType
380
def
constTerm
381
def
377
remove
varTerm
382
def
63
ref
appTerm
appTerm
refl
60
ref
"Number.Natural.zero"
const
371
ref
constTerm
383
def
absTerm
384
def
62
ref
appTerm
betaConv
appThm
absThm
appThm
appThm
243
ref
70
ref
381
ref
382
remove
72
ref
appTerm
appTerm
refl
70
ref
"Number.Natural.bit1"
const
0
ref
371
ref
372
ref
cons
opType
385
def
constTerm
386
def
383
ref
appTerm
387
def
absTerm
388
def
71
ref
appTerm
betaConv
appThm
absThm
appThm
appThm
absThm
appThm
nil
"f"
0
ref
1
ref
372
ref
cons
opType
var
384
remove
nil
cons
cons
"g"
0
ref
2
ref
372
ref
cons
opType
var
388
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
91
ref
270
ref
"C"
372
ref
cons
nil
cons
cons
cons
25
ref
cons
280
ref
58
ref
0
ref
0
ref
277
ref
7
ref
cons
opType
7
ref
cons
opType
constTerm
"fn"
277
remove
var
389
def
125
ref
33
ref
60
ref
273
ref
389
remove
varTerm
390
def
63
ref
appTerm
appTerm
345
ref
appTerm
absTerm
appTerm
appTerm
219
ref
70
ref
273
ref
390
remove
72
ref
appTerm
appTerm
283
ref
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
391
def
281
ref
appTerm
392
def
betaConv
278
ref
290
ref
391
ref
appTerm
393
def
absTerm
394
def
279
ref
appTerm
395
def
betaConv
nil
295
ref
394
ref
appTerm
396
def
axiom
nil
116
ref
396
remove
nil
cons
cons
98
ref
395
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
297
ref
298
ref
394
remove
nil
cons
cons
299
remove
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
nil
116
ref
393
remove
nil
cons
cons
98
ref
392
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
300
ref
301
ref
391
remove
nil
cons
cons
302
remove
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
397
def
subst
subst
eqMp
nil
116
ref
376
remove
"_28094"
373
ref
var
398
def
125
ref
33
ref
60
ref
381
ref
398
ref
varTerm
399
def
63
ref
appTerm
appTerm
383
ref
appTerm
absTerm
400
def
appTerm
401
def
appTerm
219
ref
70
ref
381
ref
399
ref
72
ref
appTerm
appTerm
387
ref
appTerm
absTerm
402
def
appTerm
403
def
appTerm
404
def
absTerm
405
def
appTerm
406
def
nil
cons
cons
98
ref
33
ref
60
ref
219
ref
222
ref
"Data.Bool.~"
const
27
remove
constTerm
407
def
81
ref
224
remove
appTerm
408
def
appTerm
409
def
absTerm
appTerm
absTerm
appTerm
410
def
nil
cons
411
def
cons
nil
cons
412
def
cons
nil
cons
cons
176
ref
subst
nil
"P"
374
remove
var
413
def
398
ref
99
ref
405
ref
399
ref
appTerm
414
def
appTerm
410
ref
appTerm
415
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
373
ref
nil
cons
cons
nil
cons
416
def
25
ref
cons
48
ref
subst
subst
398
remove
nil
50
ref
415
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
116
ref
414
ref
nil
cons
417
def
cons
412
ref
cons
nil
cons
cons
418
def
136
ref
subst
418
remove
161
ref
subst
414
ref
betaConv
414
remove
assume
eqMp
nil
116
ref
404
remove
nil
cons
419
def
cons
412
remove
cons
nil
cons
cons
420
def
176
ref
subst
proveHyp
420
ref
136
ref
subst
420
remove
161
ref
subst
nil
34
ref
60
ref
219
ref
70
ref
407
ref
86
remove
appTerm
absTerm
421
def
appTerm
422
def
absTerm
423
def
nil
cons
cons
nil
cons
nil
cons
cons
48
ref
subst
60
ref
nil
50
ref
422
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
231
ref
421
remove
nil
cons
cons
nil
cons
nil
cons
cons
233
ref
subst
222
ref
nil
50
ref
409
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
"a"
6
ref
var
424
def
408
ref
nil
cons
425
def
cons
nil
cons
nil
cons
cons
nil
50
ref
424
remove
varTerm
nil
cons
cons
nil
cons
nil
cons
cons
50
ref
29
ref
99
ref
52
ref
appTerm
"Data.Bool.F"
const
6
ref
constTerm
426
def
appTerm
appTerm
407
ref
52
ref
appTerm
427
def
appTerm
absTerm
428
def
52
ref
appTerm
429
def
betaConv
nil
97
ref
428
ref
appTerm
430
def
axiom
nil
116
ref
430
remove
nil
cons
cons
98
ref
429
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
113
ref
105
ref
428
remove
nil
cons
cons
332
ref
209
remove
cons
nil
cons
431
def
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
432
def
subst
subst
nil
116
ref
425
ref
cons
98
ref
426
ref
nil
cons
433
def
cons
nil
cons
434
def
cons
nil
cons
cons
435
def
136
ref
subst
435
remove
161
ref
subst
"Number.Natural.suc"
const
385
ref
constTerm
436
def
refl
437
def
nil
"n"
371
ref
var
438
def
383
ref
nil
cons
439
def
cons
440
def
nil
cons
nil
cons
cons
441
def
438
ref
381
ref
"Number.Natural.+"
const
0
ref
371
ref
385
ref
nil
cons
cons
opType
constTerm
442
def
383
ref
appTerm
443
def
438
ref
varTerm
444
def
appTerm
appTerm
444
ref
appTerm
absTerm
445
def
444
ref
appTerm
446
def
betaConv
nil
30
ref
0
ref
378
ref
7
ref
cons
opType
447
def
constTerm
448
def
445
ref
appTerm
449
def
axiom
nil
116
ref
449
remove
nil
cons
cons
98
ref
446
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
"A"
372
remove
cons
nil
cons
450
def
"P"
378
ref
var
451
def
445
remove
nil
cons
cons
"x"
371
ref
var
452
def
444
ref
nil
cons
453
def
cons
nil
cons
454
def
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
subst
455
def
appThm
456
def
241
ref
448
ref
refl
457
def
438
ref
nil
452
ref
436
ref
444
ref
appTerm
458
def
nil
cons
459
def
cons
nil
cons
nil
cons
cons
450
ref
25
ref
cons
460
def
306
ref
subst
461
def
subst
absThm
appThm
nil
50
ref
40
ref
nil
cons
cons
nil
cons
nil
cons
cons
462
def
460
ref
50
ref
29
ref
33
ref
39
ref
52
ref
absTerm
appTerm
appTerm
52
ref
appTerm
absTerm
463
def
52
ref
appTerm
464
def
betaConv
nil
97
ref
463
ref
appTerm
465
def
axiom
nil
116
ref
465
remove
nil
cons
cons
98
ref
464
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
113
ref
105
ref
463
remove
nil
cons
cons
431
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
subst
subst
466
def
trans
appThm
241
ref
381
ref
436
ref
383
ref
appTerm
467
def
appTerm
468
def
refl
441
remove
438
ref
381
ref
386
remove
444
ref
appTerm
469
def
appTerm
436
ref
"Number.Natural.bit0"
const
385
remove
constTerm
470
def
444
ref
appTerm
471
def
appTerm
472
def
appTerm
absTerm
473
def
444
ref
appTerm
474
def
betaConv
nil
448
ref
473
ref
appTerm
475
def
axiom
nil
116
ref
475
remove
nil
cons
cons
98
ref
474
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
450
ref
451
ref
473
remove
nil
cons
cons
454
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
437
ref
438
ref
381
ref
471
remove
appTerm
442
ref
444
ref
appTerm
476
def
444
ref
appTerm
477
def
appTerm
478
def
absTerm
479
def
444
ref
appTerm
480
def
betaConv
481
def
381
ref
refl
482
def
nil
381
ref
470
ref
383
ref
appTerm
appTerm
483
def
383
ref
appTerm
axiom
appThm
455
remove
appThm
nil
452
ref
439
ref
cons
nil
cons
nil
cons
cons
461
ref
subst
trans
sym
55
ref
eqMp
nil
116
ref
483
remove
443
remove
383
ref
appTerm
appTerm
484
def
nil
cons
cons
98
ref
448
ref
438
ref
99
ref
478
ref
appTerm
381
ref
470
remove
458
ref
appTerm
485
def
appTerm
486
def
442
ref
458
ref
appTerm
458
ref
appTerm
appTerm
487
def
appTerm
488
def
absTerm
489
def
appTerm
490
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
161
ref
subst
proveHyp
nil
451
ref
489
remove
nil
cons
cons
nil
cons
nil
cons
cons
460
ref
48
ref
subst
subst
438
ref
nil
50
ref
488
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
116
ref
478
ref
nil
cons
491
def
cons
98
ref
487
remove
nil
cons
492
def
cons
nil
cons
cons
nil
cons
cons
493
def
136
ref
subst
493
remove
161
ref
subst
482
ref
438
ref
486
remove
436
ref
472
ref
appTerm
appTerm
absTerm
494
def
444
ref
appTerm
495
def
betaConv
nil
448
ref
494
ref
appTerm
496
def
axiom
nil
116
ref
496
remove
nil
cons
cons
98
ref
495
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
450
ref
451
ref
494
remove
nil
cons
cons
454
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
437
ref
437
ref
478
remove
assume
appThm
appThm
trans
appThm
nil
438
ref
459
remove
cons
497
def
"m"
371
ref
var
498
def
453
ref
cons
nil
cons
499
def
cons
nil
cons
cons
438
ref
381
ref
442
ref
436
ref
498
ref
varTerm
500
def
appTerm
appTerm
444
ref
appTerm
appTerm
436
ref
442
ref
500
ref
appTerm
501
def
444
ref
appTerm
502
def
appTerm
503
def
appTerm
absTerm
504
def
444
ref
appTerm
505
def
betaConv
498
ref
448
ref
504
ref
appTerm
506
def
absTerm
507
def
500
ref
appTerm
508
def
betaConv
nil
448
ref
507
ref
appTerm
509
def
axiom
nil
116
ref
509
remove
nil
cons
cons
98
ref
508
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
450
ref
451
ref
507
remove
nil
cons
cons
452
ref
500
ref
nil
cons
510
def
cons
nil
cons
511
def
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
nil
116
ref
506
remove
nil
cons
cons
98
ref
505
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
450
ref
451
ref
504
remove
nil
cons
cons
454
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
512
def
subst
513
def
437
ref
nil
499
ref
nil
cons
cons
438
ref
381
ref
501
ref
458
ref
appTerm
appTerm
503
ref
appTerm
absTerm
514
def
444
ref
appTerm
515
def
betaConv
498
ref
448
ref
514
ref
appTerm
516
def
absTerm
517
def
500
ref
appTerm
518
def
betaConv
nil
448
ref
517
ref
appTerm
519
def
axiom
nil
116
ref
519
remove
nil
cons
cons
98
ref
518
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
450
ref
451
ref
517
remove
nil
cons
cons
511
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
nil
116
ref
516
remove
nil
cons
cons
98
ref
515
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
450
ref
451
ref
514
remove
nil
cons
cons
454
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
520
def
subst
appThm
521
def
trans
appThm
nil
452
ref
436
ref
436
ref
477
remove
appTerm
522
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
461
ref
subst
523
def
trans
sym
55
ref
eqMp
eqMp
nil
163
ref
491
remove
cons
106
ref
492
remove
cons
nil
cons
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
116
ref
125
ref
484
remove
appTerm
490
remove
appTerm
nil
cons
cons
98
ref
448
ref
479
ref
appTerm
nil
cons
524
def
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
240
ref
241
ref
479
ref
383
ref
appTerm
betaConv
appThm
457
ref
438
ref
240
ref
481
ref
appThm
479
ref
458
ref
appTerm
betaConv
appThm
absThm
appThm
appThm
appThm
457
ref
438
ref
481
remove
absThm
appThm
appThm
nil
"p"
378
ref
var
525
def
479
remove
nil
cons
526
def
cons
nil
cons
nil
cons
cons
525
ref
99
ref
125
ref
525
remove
varTerm
527
def
383
remove
appTerm
appTerm
448
ref
438
ref
99
ref
527
ref
444
ref
appTerm
528
def
appTerm
527
ref
458
ref
appTerm
appTerm
absTerm
appTerm
appTerm
appTerm
448
ref
438
ref
528
remove
absTerm
appTerm
appTerm
absTerm
529
def
527
ref
appTerm
530
def
betaConv
nil
30
ref
0
ref
447
ref
7
ref
cons
opType
constTerm
529
ref
appTerm
531
def
axiom
nil
116
ref
531
remove
nil
cons
cons
98
ref
530
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
"A"
379
remove
cons
nil
cons
"P"
447
ref
var
529
remove
nil
cons
cons
"x"
378
remove
var
527
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
nil
116
ref
524
remove
cons
98
ref
480
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
450
ref
451
ref
526
remove
cons
454
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
532
def
appThm
533
def
trans
534
def
subst
456
remove
trans
appThm
nil
452
ref
467
remove
nil
cons
cons
nil
cons
nil
cons
cons
461
ref
subst
trans
appThm
241
ref
457
ref
438
ref
482
ref
533
remove
appThm
534
ref
appThm
nil
452
ref
522
remove
nil
cons
cons
nil
cons
nil
cons
cons
461
remove
subst
trans
absThm
appThm
466
ref
trans
appThm
457
ref
438
ref
482
ref
437
ref
534
remove
appThm
appThm
nil
497
remove
nil
cons
nil
cons
cons
532
remove
subst
513
remove
trans
521
remove
trans
appThm
523
remove
trans
absThm
appThm
466
remove
trans
appThm
462
ref
50
ref
29
ref
125
ref
40
ref
appTerm
52
ref
appTerm
appTerm
52
ref
appTerm
absTerm
535
def
52
ref
appTerm
536
def
betaConv
nil
97
ref
535
ref
appTerm
537
def
axiom
nil
116
ref
537
remove
nil
cons
cons
98
ref
536
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
113
ref
105
ref
535
remove
nil
cons
cons
431
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
538
def
subst
539
def
trans
appThm
539
ref
trans
appThm
539
remove
trans
sym
55
ref
eqMp
nil
163
ref
448
ref
438
ref
381
ref
458
ref
appTerm
458
remove
appTerm
absTerm
appTerm
nil
cons
cons
106
ref
125
ref
468
remove
387
ref
appTerm
540
def
appTerm
125
ref
448
ref
438
ref
381
ref
472
remove
appTerm
469
ref
appTerm
absTerm
appTerm
appTerm
448
ref
438
ref
381
ref
436
ref
469
remove
appTerm
appTerm
485
remove
appTerm
absTerm
appTerm
appTerm
541
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
137
ref
167
remove
142
ref
appTerm
betaConv
142
remove
165
ref
appTerm
betaConv
169
remove
appThm
141
remove
109
remove
appTerm
betaConv
trans
trans
appThm
145
remove
appThm
173
remove
152
remove
appThm
eqMp
sym
55
ref
eqMp
542
def
subst
proveHyp
nil
163
ref
540
remove
nil
cons
cons
106
ref
541
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
174
ref
subst
proveHyp
trans
543
def
nil
498
ref
439
remove
cons
440
remove
"p"
371
ref
var
544
def
387
remove
nil
cons
cons
nil
cons
cons
cons
nil
cons
cons
29
ref
"_9294"
371
ref
var
545
def
29
ref
381
ref
444
ref
appTerm
546
def
545
remove
varTerm
appTerm
appTerm
426
ref
appTerm
absTerm
547
def
544
remove
varTerm
548
def
appTerm
549
def
appTerm
refl
547
ref
503
ref
appTerm
betaConv
appThm
137
ref
549
remove
betaConv
appThm
29
ref
546
ref
503
ref
appTerm
550
def
appTerm
426
ref
appTerm
refl
appThm
trans
547
remove
refl
381
ref
503
ref
appTerm
551
def
548
remove
appTerm
assume
sym
appThm
eqMp
sym
nil
50
ref
550
remove
nil
cons
cons
nil
cons
nil
cons
cons
50
ref
29
ref
53
remove
426
ref
appTerm
552
def
appTerm
427
ref
appTerm
absTerm
553
def
52
ref
appTerm
554
def
betaConv
nil
97
ref
553
ref
appTerm
555
def
axiom
nil
116
ref
555
remove
nil
cons
cons
98
ref
554
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
113
ref
105
ref
553
remove
nil
cons
cons
431
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
subst
407
ref
refl
556
def
nil
438
ref
503
ref
nil
cons
557
def
cons
499
ref
cons
nil
cons
cons
558
def
438
ref
29
ref
381
ref
500
ref
appTerm
444
ref
appTerm
559
def
appTerm
125
ref
"Number.Natural.<="
const
380
ref
constTerm
560
def
500
ref
appTerm
444
ref
appTerm
561
def
appTerm
560
ref
444
ref
appTerm
562
def
500
ref
appTerm
appTerm
563
def
appTerm
564
def
absTerm
565
def
444
ref
appTerm
566
def
betaConv
498
ref
448
ref
565
ref
appTerm
567
def
absTerm
568
def
500
ref
appTerm
569
def
betaConv
457
ref
498
ref
457
ref
438
ref
564
remove
assume
sym
29
ref
563
remove
appTerm
559
remove
appTerm
570
def
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
nil
448
ref
498
ref
448
ref
438
ref
570
remove
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
116
ref
448
ref
568
ref
appTerm
nil
cons
cons
98
ref
569
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
450
ref
451
ref
568
remove
nil
cons
cons
511
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
nil
116
ref
567
remove
nil
cons
cons
98
ref
566
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
450
ref
451
ref
565
remove
nil
cons
cons
454
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
subst
appThm
nil
"t2"
6
ref
var
571
def
560
remove
503
ref
appTerm
444
ref
appTerm
nil
cons
cons
"t1"
6
ref
var
572
def
562
remove
503
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
571
ref
29
ref
407
ref
125
ref
572
ref
varTerm
573
def
appTerm
571
remove
varTerm
574
def
appTerm
appTerm
appTerm
57
ref
407
ref
573
ref
appTerm
appTerm
407
ref
574
ref
appTerm
appTerm
appTerm
absTerm
575
def
574
ref
appTerm
576
def
betaConv
572
remove
97
ref
575
ref
appTerm
577
def
absTerm
578
def
573
ref
appTerm
579
def
betaConv
nil
97
ref
578
ref
appTerm
580
def
axiom
nil
116
ref
580
remove
nil
cons
cons
98
ref
579
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
113
ref
105
ref
578
remove
nil
cons
cons
332
ref
573
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
nil
116
ref
577
remove
nil
cons
cons
98
ref
576
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
113
ref
105
ref
575
remove
nil
cons
cons
332
ref
574
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
subst
trans
trans
sym
57
ref
refl
558
ref
438
ref
29
ref
407
ref
561
remove
appTerm
appTerm
"Number.Natural.<"
const
380
remove
constTerm
581
def
444
ref
appTerm
500
ref
appTerm
appTerm
absTerm
582
def
444
ref
appTerm
583
def
betaConv
498
ref
448
ref
582
ref
appTerm
584
def
absTerm
585
def
500
ref
appTerm
586
def
betaConv
nil
448
ref
585
ref
appTerm
587
def
axiom
nil
116
ref
587
remove
nil
cons
cons
98
ref
586
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
450
ref
451
ref
585
remove
nil
cons
cons
511
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
nil
116
ref
584
remove
nil
cons
cons
98
ref
583
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
450
ref
451
ref
582
remove
nil
cons
cons
454
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
588
def
subst
nil
498
ref
557
remove
cons
nil
cons
nil
cons
cons
589
def
438
ref
29
ref
581
remove
500
ref
appTerm
444
ref
appTerm
appTerm
58
ref
447
remove
constTerm
590
def
"d"
371
ref
var
591
def
546
ref
501
remove
436
ref
591
ref
varTerm
592
def
appTerm
593
def
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
594
def
444
ref
appTerm
595
def
betaConv
498
ref
448
ref
594
ref
appTerm
596
def
absTerm
597
def
500
ref
appTerm
598
def
betaConv
nil
448
ref
597
ref
appTerm
599
def
axiom
nil
116
ref
599
remove
nil
cons
cons
98
ref
598
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
450
ref
451
ref
597
remove
nil
cons
cons
511
remove
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
nil
116
ref
596
remove
nil
cons
cons
98
ref
595
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
450
ref
451
ref
594
remove
nil
cons
cons
454
remove
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
600
def
subst
trans
590
ref
refl
601
def
591
ref
546
ref
refl
nil
438
ref
593
remove
nil
cons
cons
498
ref
502
ref
nil
cons
602
def
cons
nil
cons
603
def
cons
nil
cons
cons
512
remove
subst
437
ref
nil
438
ref
592
ref
nil
cons
cons
604
def
603
remove
cons
nil
cons
cons
520
ref
subst
appThm
trans
appThm
absThm
appThm
trans
appThm
589
remove
588
remove
subst
558
remove
600
remove
subst
trans
601
remove
591
ref
551
ref
refl
nil
604
remove
499
remove
cons
nil
cons
cons
520
remove
subst
appThm
absThm
appThm
trans
appThm
sym
nil
116
ref
57
ref
590
ref
591
ref
546
remove
436
ref
436
ref
442
ref
502
ref
appTerm
592
ref
appTerm
appTerm
appTerm
appTerm
605
def
absTerm
606
def
appTerm
607
def
appTerm
590
remove
591
ref
551
ref
436
ref
476
ref
592
ref
appTerm
appTerm
appTerm
608
def
absTerm
609
def
appTerm
610
def
appTerm
611
def
nil
cons
cons
nil
cons
nil
cons
cons
325
ref
refl
612
def
nil
50
ref
407
ref
122
ref
appTerm
613
def
nil
cons
614
def
cons
nil
cons
nil
cons
cons
432
ref
subst
appThm
sym
612
remove
155
ref
50
ref
29
ref
407
ref
427
ref
appTerm
appTerm
52
ref
appTerm
absTerm
615
def
52
ref
appTerm
616
def
betaConv
nil
97
ref
615
ref
appTerm
617
def
axiom
nil
116
ref
617
remove
nil
cons
cons
98
ref
616
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
113
ref
105
ref
615
remove
nil
cons
cons
431
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
subst
appThm
nil
332
ref
154
ref
cons
nil
cons
618
def
nil
cons
cons
114
remove
306
ref
subst
619
def
subst
trans
sym
55
ref
eqMp
eqMp
subst
sym
nil
116
ref
407
ref
611
remove
appTerm
620
def
nil
cons
621
def
cons
434
ref
cons
nil
cons
cons
622
def
136
ref
subst
622
remove
161
ref
subst
nil
448
ref
498
remove
448
ref
438
ref
381
ref
502
remove
appTerm
476
ref
500
remove
appTerm
623
def
appTerm
624
def
absTerm
appTerm
absTerm
625
def
appTerm
626
def
axiom
nil
116
ref
626
remove
nil
cons
627
def
cons
628
def
434
ref
cons
nil
cons
cons
629
def
176
ref
subst
proveHyp
629
ref
136
ref
subst
629
remove
161
ref
subst
nil
"_2184"
371
ref
var
630
def
453
remove
cons
"_2183"
371
ref
var
631
def
510
ref
cons
nil
cons
cons
nil
cons
cons
438
remove
381
ref
442
remove
631
remove
varTerm
632
def
appTerm
444
remove
appTerm
appTerm
476
ref
632
ref
appTerm
appTerm
absTerm
633
def
630
remove
varTerm
634
def
appTerm
635
def
betaConv
625
ref
632
ref
appTerm
636
def
betaConv
nil
628
remove
98
ref
636
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
450
ref
451
ref
625
remove
nil
cons
cons
452
ref
632
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
nil
116
ref
448
ref
633
ref
appTerm
nil
cons
cons
98
ref
635
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
450
ref
451
ref
633
remove
nil
cons
cons
452
ref
634
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
subst
nil
116
ref
624
remove
nil
cons
cons
98
ref
551
ref
436
ref
623
ref
appTerm
appTerm
nil
cons
637
def
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
nil
"_9301"
371
ref
var
638
def
623
remove
nil
cons
cons
"_9300"
371
ref
var
639
def
602
remove
cons
nil
cons
cons
nil
cons
cons
nil
116
ref
381
ref
639
remove
varTerm
640
def
appTerm
638
remove
varTerm
641
def
appTerm
642
def
nil
cons
643
def
cons
98
ref
381
remove
436
ref
640
remove
appTerm
appTerm
436
ref
641
remove
appTerm
appTerm
nil
cons
644
def
cons
nil
cons
cons
nil
cons
cons
645
def
136
ref
subst
645
remove
161
ref
subst
437
remove
642
remove
assume
appThm
eqMp
nil
163
ref
643
remove
cons
106
ref
644
remove
cons
nil
cons
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
subst
eqMp
nil
116
ref
637
remove
cons
434
ref
cons
nil
cons
cons
176
ref
subst
proveHyp
nil
"_9299"
371
remove
var
646
def
510
remove
cons
nil
cons
nil
cons
cons
nil
116
ref
551
remove
436
remove
476
remove
646
remove
varTerm
647
def
appTerm
appTerm
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
29
ref
613
ref
appTerm
refl
155
remove
432
remove
subst
appThm
nil
332
ref
614
remove
cons
nil
cons
nil
cons
cons
619
ref
subst
trans
sym
55
ref
eqMp
subst
591
ref
407
ref
608
remove
appTerm
absTerm
648
def
647
ref
appTerm
649
def
betaConv
nil
116
ref
607
remove
nil
cons
cons
98
ref
610
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
116
ref
325
ref
426
ref
appTerm
650
def
nil
cons
651
def
cons
98
ref
29
ref
407
ref
57
ref
122
ref
appTerm
102
ref
appTerm
appTerm
appTerm
125
ref
613
remove
appTerm
407
ref
102
ref
appTerm
652
def
appTerm
appTerm
nil
cons
653
def
cons
nil
cons
654
def
cons
nil
cons
cons
655
def
136
ref
subst
655
remove
161
ref
subst
29
ref
"_534"
6
ref
var
656
def
29
ref
407
ref
57
ref
656
remove
varTerm
657
def
appTerm
102
ref
appTerm
appTerm
appTerm
125
ref
407
ref
657
remove
appTerm
appTerm
652
ref
appTerm
appTerm
absTerm
658
def
122
ref
appTerm
659
def
appTerm
refl
660
def
658
ref
426
ref
appTerm
betaConv
appThm
137
ref
659
remove
betaConv
appThm
661
def
29
ref
407
ref
57
ref
426
ref
appTerm
662
def
102
ref
appTerm
appTerm
appTerm
125
ref
407
ref
426
ref
appTerm
663
def
appTerm
652
ref
appTerm
appTerm
refl
appThm
trans
658
remove
refl
664
def
650
remove
assume
appThm
eqMp
sym
137
ref
556
ref
158
ref
50
ref
29
ref
662
remove
52
ref
appTerm
appTerm
52
ref
appTerm
absTerm
665
def
52
ref
appTerm
666
def
betaConv
nil
97
ref
665
ref
appTerm
667
def
axiom
nil
116
ref
667
remove
nil
cons
cons
98
ref
666
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
113
ref
105
ref
665
remove
nil
cons
cons
431
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
subst
appThm
appThm
241
ref
nil
29
ref
663
remove
appTerm
40
ref
appTerm
axiom
668
def
appThm
652
ref
refl
669
def
appThm
nil
50
ref
652
ref
nil
cons
670
def
cons
nil
cons
nil
cons
cons
671
def
538
remove
subst
trans
appThm
nil
332
ref
670
remove
cons
nil
cons
nil
cons
cons
619
remove
subst
trans
sym
55
ref
eqMp
eqMp
eqMp
nil
163
ref
651
ref
cons
106
ref
653
ref
cons
nil
cons
672
def
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
nil
116
ref
325
remove
40
ref
appTerm
673
def
nil
cons
674
def
cons
654
remove
cons
nil
cons
cons
675
def
136
ref
subst
675
remove
161
ref
subst
660
remove
"_532"
6
remove
var
676
def
29
ref
407
ref
57
ref
676
remove
varTerm
677
def
appTerm
102
ref
appTerm
appTerm
appTerm
125
ref
407
ref
677
remove
appTerm
appTerm
652
ref
appTerm
appTerm
absTerm
40
ref
appTerm
betaConv
appThm
661
remove
29
ref
407
ref
57
ref
40
ref
appTerm
678
def
102
remove
appTerm
appTerm
appTerm
125
ref
407
ref
40
ref
appTerm
679
def
appTerm
652
remove
appTerm
appTerm
refl
appThm
trans
664
remove
673
remove
assume
appThm
eqMp
sym
137
ref
556
ref
158
remove
50
ref
29
ref
678
remove
52
ref
appTerm
appTerm
40
ref
appTerm
absTerm
680
def
52
ref
appTerm
681
def
betaConv
nil
97
ref
680
ref
appTerm
682
def
axiom
nil
116
ref
682
remove
nil
cons
cons
98
ref
681
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
113
ref
105
ref
680
remove
nil
cons
cons
431
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
subst
appThm
nil
29
ref
679
remove
appTerm
426
ref
appTerm
axiom
683
def
trans
appThm
241
ref
683
remove
appThm
669
remove
appThm
671
remove
50
ref
29
ref
125
ref
426
ref
appTerm
52
ref
appTerm
appTerm
426
ref
appTerm
absTerm
684
def
52
ref
appTerm
685
def
betaConv
nil
97
ref
684
ref
appTerm
686
def
axiom
nil
116
ref
686
remove
nil
cons
cons
98
ref
685
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
113
ref
105
ref
684
remove
nil
cons
cons
431
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
subst
trans
appThm
nil
50
ref
433
ref
cons
nil
cons
nil
cons
cons
50
ref
29
ref
29
ref
426
ref
appTerm
687
def
52
ref
appTerm
appTerm
427
remove
appTerm
absTerm
688
def
52
ref
appTerm
689
def
betaConv
nil
97
ref
688
ref
appTerm
690
def
axiom
nil
116
ref
690
remove
nil
cons
cons
98
ref
689
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
113
ref
105
ref
688
remove
nil
cons
cons
431
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
subst
668
remove
trans
trans
sym
55
ref
eqMp
eqMp
eqMp
nil
163
ref
674
remove
cons
691
def
672
remove
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
50
ref
57
remove
54
remove
appTerm
552
remove
appTerm
absTerm
692
def
122
ref
appTerm
693
def
betaConv
nil
97
ref
692
ref
appTerm
694
def
axiom
nil
116
ref
694
remove
nil
cons
cons
98
ref
693
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
113
ref
105
ref
692
remove
nil
cons
cons
618
remove
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
nil
691
remove
106
ref
651
remove
cons
363
ref
653
remove
cons
nil
cons
cons
cons
nil
cons
cons
369
ref
subst
proveHyp
proveHyp
proveHyp
subst
241
ref
nil
451
ref
606
ref
nil
cons
cons
nil
cons
nil
cons
cons
460
remove
137
remove
556
ref
59
ref
refl
nil
"t"
31
ref
var
35
remove
nil
cons
695
def
cons
nil
cons
nil
cons
cons
91
ref
"B"
7
ref
cons
nil
cons
cons
25
ref
cons
"t"
0
ref
4
remove
opType
696
def
var
697
def
11
ref
0
ref
696
ref
0
ref
696
ref
7
ref
cons
opType
698
def
nil
cons
cons
opType
constTerm
699
def
697
ref
varTerm
700
def
appTerm
39
ref
700
ref
100
remove
appTerm
absTerm
701
def
appTerm
702
def
absTerm
703
def
700
ref
appTerm
704
def
betaConv
30
ref
0
ref
698
ref
7
ref
cons
opType
constTerm
705
def
refl
697
ref
702
remove
assume
sym
699
remove
701
remove
appTerm
700
ref
appTerm
706
def
assume
sym
deductAntisym
absThm
appThm
nil
705
ref
697
remove
706
remove
absTerm
appTerm
axiom
eqMp
nil
116
ref
705
remove
703
ref
appTerm
nil
cons
cons
98
ref
704
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
"A"
696
ref
nil
cons
cons
nil
cons
"P"
698
remove
var
703
remove
nil
cons
cons
"x"
696
ref
var
700
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
subst
subst
appThm
appThm
appThm
33
ref
39
ref
407
ref
107
remove
appTerm
absTerm
appTerm
refl
appThm
sym
nil
37
ref
695
remove
cons
nil
cons
nil
cons
cons
37
remove
29
ref
407
ref
59
remove
39
ref
101
ref
absTerm
appTerm
appTerm
appTerm
33
ref
39
ref
407
ref
101
remove
appTerm
absTerm
appTerm
appTerm
absTerm
707
def
38
ref
appTerm
708
def
betaConv
nil
30
ref
44
remove
constTerm
707
ref
appTerm
709
def
axiom
nil
116
ref
709
remove
nil
cons
cons
98
ref
708
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
"A"
304
remove
cons
nil
cons
"P"
32
remove
var
707
remove
nil
cons
cons
"x"
31
remove
var
38
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
subst
eqMp
subst
710
def
subst
457
ref
591
ref
556
ref
606
remove
592
ref
appTerm
betaConv
appThm
absThm
appThm
trans
appThm
nil
451
ref
609
ref
nil
cons
cons
nil
cons
nil
cons
cons
710
remove
subst
457
remove
591
ref
556
remove
609
remove
592
remove
appTerm
betaConv
appThm
absThm
appThm
trans
appThm
trans
620
remove
assume
eqMp
nil
163
ref
448
ref
591
remove
407
ref
605
remove
appTerm
absTerm
appTerm
nil
cons
cons
106
ref
448
remove
648
ref
appTerm
nil
cons
711
def
cons
nil
cons
cons
nil
cons
cons
542
ref
subst
proveHyp
nil
116
ref
711
remove
cons
98
ref
649
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
450
remove
451
remove
648
remove
nil
cons
cons
452
remove
647
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
eqMp
subst
eqMp
eqMp
nil
163
ref
627
remove
cons
106
ref
433
ref
cons
nil
cons
712
def
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
163
ref
621
remove
cons
712
ref
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
subst
deductAntisym
543
remove
eqMp
482
remove
400
ref
62
ref
appTerm
713
def
betaConv
nil
163
ref
401
remove
nil
cons
714
def
cons
106
ref
403
remove
nil
cons
715
def
cons
nil
cons
cons
nil
cons
cons
716
def
174
ref
subst
nil
116
ref
714
remove
cons
98
ref
713
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
92
ref
34
ref
400
remove
nil
cons
cons
93
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
appThm
nil
70
ref
223
ref
nil
cons
cons
nil
cons
nil
cons
cons
717
def
402
ref
71
ref
appTerm
718
def
betaConv
716
remove
542
ref
subst
nil
116
ref
715
remove
cons
98
ref
718
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
232
ref
231
ref
402
remove
nil
cons
cons
235
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
subst
appThm
399
remove
refl
408
remove
assume
appThm
eqMp
eqMp
eqMp
nil
163
ref
425
remove
cons
712
remove
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
163
ref
419
remove
cons
106
ref
411
remove
cons
nil
cons
719
def
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
163
ref
417
remove
cons
719
ref
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
116
ref
30
ref
375
remove
constTerm
"x"
373
remove
var
720
def
99
ref
405
ref
720
remove
varTerm
appTerm
appTerm
410
ref
appTerm
absTerm
appTerm
nil
cons
cons
98
ref
99
ref
406
remove
appTerm
410
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
416
remove
413
remove
405
remove
nil
cons
cons
719
remove
cons
nil
cons
cons
333
ref
subst
eqMp
eqMp
proveHyp
nil
33
ref
423
remove
appTerm
thm
58
ref
0
ref
0
ref
0
ref
5
ref
90
ref
cons
opType
721
def
7
ref
cons
opType
722
def
7
ref
cons
opType
723
def
constTerm
724
def
refl
"fn"
721
ref
var
725
def
241
remove
242
remove
60
ref
305
ref
725
remove
varTerm
726
def
63
ref
appTerm
appTerm
refl
60
ref
62
ref
absTerm
727
def
62
ref
appTerm
betaConv
appThm
absThm
appThm
appThm
219
ref
70
ref
305
ref
726
remove
72
ref
appTerm
appTerm
"g"
0
ref
2
ref
90
ref
cons
opType
var
varTerm
71
ref
appTerm
728
def
appTerm
absTerm
appTerm
refl
appThm
absThm
appThm
nil
"f"
0
ref
1
ref
90
ref
cons
opType
var
727
remove
nil
cons
cons
nil
cons
nil
cons
cons
91
ref
270
ref
"C"
90
remove
cons
nil
cons
cons
cons
25
ref
cons
397
ref
subst
subst
eqMp
nil
116
ref
724
ref
"_28098"
721
ref
var
729
def
125
ref
33
ref
60
ref
305
ref
729
ref
varTerm
730
def
63
ref
appTerm
appTerm
62
ref
appTerm
absTerm
731
def
appTerm
732
def
appTerm
219
ref
70
ref
305
ref
730
ref
72
ref
appTerm
appTerm
728
remove
appTerm
absTerm
appTerm
733
def
appTerm
734
def
absTerm
735
def
appTerm
736
def
nil
cons
cons
98
ref
724
remove
729
ref
732
ref
absTerm
737
def
appTerm
738
def
nil
cons
739
def
cons
nil
cons
740
def
cons
nil
cons
cons
176
ref
subst
nil
"P"
722
remove
var
741
def
729
ref
99
ref
735
ref
730
ref
appTerm
742
def
appTerm
738
ref
appTerm
743
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
721
ref
nil
cons
cons
nil
cons
744
def
25
ref
cons
48
ref
subst
745
def
subst
729
ref
nil
50
ref
743
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
116
ref
742
ref
nil
cons
746
def
cons
740
ref
cons
nil
cons
cons
747
def
136
ref
subst
747
remove
161
ref
subst
742
ref
betaConv
742
remove
assume
eqMp
nil
116
ref
734
remove
nil
cons
748
def
cons
740
remove
cons
nil
cons
cons
749
def
176
ref
subst
proveHyp
749
ref
136
ref
subst
749
remove
161
ref
subst
737
ref
730
ref
appTerm
750
def
betaConv
751
def
sym
nil
163
ref
732
remove
nil
cons
752
def
cons
753
def
106
ref
733
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
174
ref
subst
eqMp
744
ref
741
ref
737
ref
nil
cons
cons
754
def
"x"
721
ref
var
755
def
730
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
ref
subst
proveHyp
eqMp
nil
163
ref
748
remove
cons
106
ref
739
ref
cons
nil
cons
756
def
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
163
ref
746
remove
cons
756
ref
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
116
ref
30
ref
723
remove
constTerm
757
def
755
ref
99
ref
735
ref
755
ref
varTerm
758
def
appTerm
appTerm
738
ref
appTerm
absTerm
appTerm
nil
cons
cons
98
ref
99
ref
736
remove
appTerm
738
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
744
ref
741
ref
735
remove
nil
cons
cons
756
remove
cons
nil
cons
cons
333
ref
subst
eqMp
eqMp
proveHyp
nil
116
ref
739
remove
cons
98
ref
33
ref
60
ref
33
ref
80
ref
29
ref
83
ref
appTerm
305
ref
62
ref
appTerm
759
def
82
ref
appTerm
760
def
appTerm
761
def
absTerm
762
def
appTerm
763
def
absTerm
764
def
appTerm
765
def
nil
cons
766
def
cons
nil
cons
767
def
cons
nil
cons
cons
176
ref
subst
nil
741
remove
729
ref
99
ref
750
ref
appTerm
765
ref
appTerm
768
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
745
remove
subst
729
remove
nil
50
ref
768
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
116
ref
750
ref
nil
cons
769
def
cons
767
ref
cons
nil
cons
cons
770
def
136
ref
subst
770
remove
161
ref
subst
751
remove
750
remove
assume
eqMp
nil
116
ref
752
remove
cons
771
def
767
remove
cons
nil
cons
cons
772
def
176
ref
subst
proveHyp
772
ref
136
ref
subst
772
remove
161
ref
subst
nil
34
ref
764
remove
nil
cons
cons
nil
cons
nil
cons
cons
48
ref
subst
60
ref
nil
50
ref
763
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
34
ref
762
remove
nil
cons
cons
nil
cons
nil
cons
cons
48
ref
subst
80
remove
nil
50
ref
761
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
116
ref
83
ref
nil
cons
773
def
cons
98
ref
760
ref
nil
cons
774
def
cons
nil
cons
cons
nil
cons
cons
775
def
331
remove
nil
116
ref
328
ref
cons
98
ref
191
ref
122
ref
appTerm
nil
cons
776
def
cons
nil
cons
cons
nil
cons
cons
161
ref
subst
proveHyp
191
remove
refl
330
remove
appThm
sym
nil
116
ref
157
ref
cons
777
def
98
ref
157
ref
cons
nil
cons
cons
nil
cons
cons
778
def
136
ref
subst
778
remove
161
ref
subst
159
remove
eqMp
nil
163
ref
157
remove
cons
164
remove
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
777
remove
98
ref
154
remove
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
nil
163
ref
328
remove
cons
106
ref
776
remove
cons
nil
cons
cons
nil
cons
cons
779
def
542
ref
subst
eqMp
176
ref
779
remove
174
ref
subst
eqMp
deductAntisym
deductAntisym
780
def
subst
775
ref
136
ref
subst
775
remove
161
ref
subst
731
ref
62
ref
appTerm
781
def
betaConv
nil
771
remove
98
ref
781
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
92
ref
34
ref
731
remove
nil
cons
cons
93
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
782
def
sym
730
remove
refl
83
ref
assume
appThm
trans
nil
60
ref
82
remove
nil
cons
cons
nil
cons
nil
cons
cons
782
remove
subst
trans
eqMp
nil
163
ref
773
ref
cons
106
ref
774
ref
cons
nil
cons
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
nil
116
ref
99
ref
83
ref
appTerm
760
ref
appTerm
nil
cons
cons
98
ref
99
ref
760
ref
appTerm
83
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
161
ref
subst
proveHyp
nil
116
ref
774
ref
cons
98
ref
773
ref
cons
nil
cons
cons
nil
cons
cons
783
def
136
ref
subst
783
remove
161
ref
subst
18
ref
refl
760
remove
assume
appThm
eqMp
nil
163
ref
774
remove
cons
106
ref
773
remove
cons
nil
cons
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
753
remove
106
ref
766
remove
cons
nil
cons
784
def
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
163
ref
769
remove
cons
784
ref
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
116
ref
757
remove
755
remove
99
ref
737
remove
758
remove
appTerm
appTerm
765
ref
appTerm
absTerm
appTerm
nil
cons
cons
98
ref
99
ref
738
remove
appTerm
765
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
744
remove
754
remove
784
remove
cons
nil
cons
cons
333
ref
subst
eqMp
eqMp
proveHyp
nil
33
ref
60
ref
33
ref
"b"
1
remove
var
785
def
29
ref
81
remove
18
remove
785
remove
varTerm
786
def
appTerm
appTerm
appTerm
759
remove
786
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
thm
58
remove
0
ref
0
ref
0
ref
5
remove
3
ref
cons
opType
787
def
7
ref
cons
opType
788
def
7
remove
cons
opType
789
def
constTerm
790
def
refl
"fn"
787
ref
var
791
def
125
ref
33
ref
60
ref
11
remove
0
ref
2
ref
67
remove
nil
cons
cons
opType
constTerm
792
def
791
remove
varTerm
793
def
63
ref
appTerm
appTerm
"f"
696
remove
var
varTerm
62
ref
appTerm
794
def
appTerm
absTerm
appTerm
appTerm
refl
243
remove
70
ref
792
ref
793
remove
72
ref
appTerm
appTerm
refl
70
ref
71
ref
absTerm
795
def
71
ref
appTerm
betaConv
appThm
absThm
appThm
appThm
absThm
appThm
nil
"g"
0
remove
2
ref
3
ref
cons
opType
var
795
remove
nil
cons
cons
nil
cons
nil
cons
cons
91
remove
270
remove
"C"
3
remove
cons
nil
cons
cons
cons
25
ref
cons
397
remove
subst
subst
eqMp
nil
116
ref
790
ref
"_28096"
787
ref
var
796
def
125
remove
33
ref
60
ref
792
ref
796
ref
varTerm
797
def
63
ref
appTerm
appTerm
794
remove
appTerm
absTerm
appTerm
798
def
appTerm
219
ref
70
ref
792
ref
797
ref
72
ref
appTerm
appTerm
71
ref
appTerm
absTerm
799
def
appTerm
800
def
appTerm
801
def
absTerm
802
def
appTerm
803
def
nil
cons
cons
98
ref
790
remove
796
ref
800
ref
absTerm
804
def
appTerm
805
def
nil
cons
806
def
cons
nil
cons
807
def
cons
nil
cons
cons
176
ref
subst
nil
"P"
788
remove
var
808
def
796
ref
99
ref
802
ref
797
ref
appTerm
809
def
appTerm
805
ref
appTerm
810
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
787
ref
nil
cons
cons
nil
cons
811
def
25
ref
cons
48
ref
subst
812
def
subst
796
ref
nil
50
ref
810
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
116
ref
809
ref
nil
cons
813
def
cons
807
ref
cons
nil
cons
cons
814
def
136
ref
subst
814
remove
161
ref
subst
809
ref
betaConv
809
remove
assume
eqMp
nil
116
ref
801
remove
nil
cons
815
def
cons
807
remove
cons
nil
cons
cons
816
def
176
ref
subst
proveHyp
816
ref
136
ref
subst
816
remove
161
ref
subst
804
ref
797
ref
appTerm
817
def
betaConv
818
def
sym
nil
163
ref
798
remove
nil
cons
cons
106
ref
800
remove
nil
cons
819
def
cons
nil
cons
cons
nil
cons
cons
542
remove
subst
eqMp
811
ref
808
ref
804
ref
nil
cons
cons
820
def
"x"
787
ref
var
821
def
797
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
184
remove
subst
proveHyp
eqMp
nil
163
ref
815
remove
cons
106
ref
806
ref
cons
nil
cons
822
def
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
163
ref
813
remove
cons
822
ref
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
116
ref
30
remove
789
remove
constTerm
823
def
821
ref
99
ref
802
ref
821
ref
varTerm
824
def
appTerm
appTerm
805
ref
appTerm
absTerm
appTerm
nil
cons
cons
98
ref
99
ref
803
remove
appTerm
805
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
811
ref
808
ref
802
remove
nil
cons
cons
822
remove
cons
nil
cons
cons
333
ref
subst
eqMp
eqMp
proveHyp
nil
116
ref
806
remove
cons
98
ref
219
ref
70
ref
219
ref
222
ref
29
ref
225
ref
appTerm
792
ref
71
ref
appTerm
223
remove
appTerm
825
def
appTerm
826
def
absTerm
827
def
appTerm
828
def
absTerm
829
def
appTerm
830
def
nil
cons
831
def
cons
nil
cons
832
def
cons
nil
cons
cons
176
ref
subst
nil
808
remove
796
ref
99
ref
817
ref
appTerm
830
ref
appTerm
833
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
812
remove
subst
796
remove
nil
50
ref
833
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
116
ref
817
ref
nil
cons
834
def
cons
832
ref
cons
nil
cons
cons
835
def
136
ref
subst
835
remove
161
ref
subst
818
remove
817
remove
assume
eqMp
nil
116
ref
819
ref
cons
836
def
832
remove
cons
nil
cons
cons
837
def
176
ref
subst
proveHyp
837
ref
136
ref
subst
837
remove
161
ref
subst
nil
231
ref
829
remove
nil
cons
cons
nil
cons
nil
cons
cons
233
ref
subst
70
ref
nil
50
ref
828
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
231
ref
827
remove
nil
cons
cons
nil
cons
nil
cons
cons
233
ref
subst
222
remove
nil
50
ref
826
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
116
ref
225
ref
nil
cons
838
def
cons
98
ref
825
ref
nil
cons
839
def
cons
nil
cons
cons
nil
cons
cons
840
def
780
ref
subst
840
ref
136
ref
subst
840
remove
161
ref
subst
799
ref
71
ref
appTerm
841
def
betaConv
nil
836
remove
98
ref
841
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
232
ref
231
ref
799
remove
nil
cons
cons
235
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
842
def
sym
797
remove
refl
225
ref
assume
appThm
trans
717
remove
842
remove
subst
trans
eqMp
nil
163
ref
838
ref
cons
106
ref
839
ref
cons
nil
cons
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
nil
116
ref
99
ref
225
ref
appTerm
825
ref
appTerm
nil
cons
cons
98
ref
99
ref
825
ref
appTerm
225
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
161
ref
subst
proveHyp
nil
116
ref
839
ref
cons
98
ref
838
ref
cons
nil
cons
cons
nil
cons
cons
843
def
136
ref
subst
843
remove
161
ref
subst
19
ref
refl
825
remove
assume
appThm
eqMp
nil
163
ref
839
remove
cons
106
ref
838
remove
cons
nil
cons
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
163
ref
819
remove
cons
106
ref
831
remove
cons
nil
cons
844
def
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
163
ref
834
remove
cons
844
ref
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
116
ref
823
remove
821
remove
99
ref
804
remove
824
remove
appTerm
appTerm
830
ref
appTerm
absTerm
appTerm
nil
cons
cons
98
ref
99
ref
805
remove
appTerm
830
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
811
remove
820
remove
844
remove
cons
nil
cons
cons
333
ref
subst
eqMp
eqMp
proveHyp
nil
219
ref
"a"
2
remove
var
845
def
219
ref
70
ref
29
ref
13
remove
19
remove
845
remove
varTerm
846
def
appTerm
appTerm
72
ref
appTerm
appTerm
792
ref
846
remove
appTerm
71
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
thm
250
remove
nil
238
remove
thm
nil
298
ref
278
ref
290
ref
280
ref
237
ref
10
ref
99
ref
"Data.Sum.isLeft"
const
8
ref
constTerm
847
def
21
ref
appTerm
appTerm
273
ref
282
ref
21
ref
appTerm
appTerm
848
def
279
ref
"Data.Sum.destLeft"
const
721
remove
constTerm
849
def
21
ref
appTerm
appTerm
appTerm
appTerm
850
def
absTerm
851
def
appTerm
852
def
absTerm
853
def
appTerm
854
def
absTerm
855
def
nil
cons
cons
nil
cons
nil
cons
cons
297
remove
25
ref
cons
48
ref
subst
856
def
subst
278
ref
nil
50
ref
854
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
301
ref
853
remove
nil
cons
cons
nil
cons
nil
cons
cons
300
remove
25
ref
cons
48
ref
subst
857
def
subst
280
ref
nil
50
ref
852
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
9
ref
851
remove
nil
cons
cons
nil
cons
nil
cons
cons
49
ref
subst
10
ref
nil
50
ref
850
ref
nil
cons
858
def
cons
nil
cons
nil
cons
cons
56
ref
subst
251
ref
nil
253
ref
98
ref
858
ref
cons
nil
cons
859
def
cons
nil
cons
cons
860
def
176
ref
subst
proveHyp
860
ref
136
ref
subst
860
remove
161
ref
subst
nil
231
ref
70
ref
257
ref
850
ref
appTerm
861
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
233
ref
subst
70
ref
nil
50
ref
861
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
260
ref
859
ref
cons
nil
cons
cons
862
def
136
ref
subst
862
remove
161
ref
subst
262
ref
nil
264
ref
859
ref
cons
nil
cons
cons
863
def
176
ref
subst
proveHyp
863
ref
136
ref
subst
863
remove
161
ref
subst
240
ref
847
ref
refl
864
def
268
ref
appThm
70
ref
407
ref
847
ref
72
ref
appTerm
865
def
appTerm
866
def
absTerm
867
def
71
ref
appTerm
868
def
betaConv
nil
219
ref
867
ref
appTerm
869
def
axiom
nil
116
ref
869
remove
nil
cons
cons
98
ref
868
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
232
ref
231
ref
867
remove
nil
cons
cons
235
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
nil
116
ref
866
remove
nil
cons
cons
98
ref
29
ref
865
ref
appTerm
426
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
nil
163
ref
865
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
116
ref
407
ref
165
ref
appTerm
870
def
nil
cons
871
def
cons
98
ref
29
ref
165
ref
appTerm
426
ref
appTerm
nil
cons
872
def
cons
nil
cons
cons
nil
cons
cons
873
def
136
ref
subst
873
remove
161
ref
subst
nil
215
remove
434
remove
cons
nil
cons
cons
780
remove
subst
29
ref
870
ref
appTerm
refl
116
ref
123
remove
426
ref
appTerm
absTerm
874
def
165
ref
appTerm
betaConv
appThm
nil
148
remove
407
ref
appTerm
874
remove
appTerm
axiom
172
remove
appThm
eqMp
870
remove
assume
eqMp
nil
116
ref
188
remove
426
ref
appTerm
nil
cons
cons
98
ref
99
ref
426
ref
appTerm
875
def
165
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
161
ref
subst
proveHyp
nil
116
ref
433
ref
cons
98
ref
214
ref
cons
nil
cons
cons
nil
cons
cons
876
def
136
ref
subst
876
remove
161
ref
subst
116
ref
122
remove
absTerm
877
def
165
remove
appTerm
878
def
betaConv
nil
687
remove
97
ref
877
ref
appTerm
879
def
appTerm
axiom
426
ref
assume
eqMp
nil
116
ref
879
remove
nil
cons
cons
98
ref
878
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
113
ref
105
ref
877
remove
nil
cons
cons
332
remove
214
ref
cons
nil
cons
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
eqMp
nil
163
ref
433
remove
cons
106
ref
214
remove
cons
nil
cons
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
163
ref
871
remove
cons
106
ref
872
remove
cons
nil
cons
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
880
def
subst
eqMp
trans
appThm
273
ref
refl
881
def
282
remove
refl
882
def
268
ref
appThm
303
remove
trans
appThm
883
def
279
ref
refl
884
def
849
ref
refl
885
def
268
ref
appThm
appThm
appThm
appThm
nil
50
ref
273
ref
283
ref
appTerm
279
remove
849
ref
72
ref
appTerm
appTerm
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
50
ref
29
ref
875
remove
52
ref
appTerm
appTerm
40
ref
appTerm
absTerm
886
def
52
ref
appTerm
887
def
betaConv
nil
97
ref
886
ref
appTerm
888
def
axiom
nil
116
ref
888
remove
nil
cons
cons
98
ref
887
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
113
ref
105
ref
886
remove
nil
cons
cons
431
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
889
def
subst
trans
sym
55
ref
eqMp
eqMp
nil
308
ref
106
ref
858
ref
cons
nil
cons
890
def
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
310
ref
890
ref
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
116
ref
219
ref
234
ref
311
ref
850
ref
appTerm
absTerm
appTerm
nil
cons
cons
98
ref
312
ref
850
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
232
ref
313
ref
890
ref
cons
nil
cons
cons
333
ref
subst
eqMp
nil
34
ref
60
ref
335
ref
850
ref
appTerm
891
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
48
ref
subst
60
ref
nil
50
ref
891
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
338
ref
859
ref
cons
nil
cons
cons
892
def
136
ref
subst
892
remove
161
ref
subst
340
ref
nil
342
ref
859
remove
cons
nil
cons
cons
893
def
176
ref
subst
proveHyp
893
ref
136
ref
subst
893
remove
161
ref
subst
240
ref
864
remove
344
ref
appThm
nil
50
ref
847
remove
63
ref
appTerm
894
def
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
60
ref
894
remove
absTerm
895
def
62
ref
appTerm
896
def
betaConv
nil
33
ref
895
ref
appTerm
897
def
axiom
nil
116
ref
897
remove
nil
cons
cons
98
ref
896
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
92
ref
34
ref
895
remove
nil
cons
cons
93
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
eqMp
trans
appThm
881
remove
882
remove
344
ref
appThm
355
remove
trans
appThm
898
def
884
remove
885
remove
344
ref
appThm
60
ref
305
remove
849
remove
63
ref
appTerm
appTerm
62
ref
appTerm
absTerm
899
def
62
ref
appTerm
900
def
betaConv
nil
33
ref
899
ref
appTerm
901
def
axiom
nil
116
ref
901
remove
nil
cons
cons
98
ref
900
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
92
ref
34
ref
899
remove
nil
cons
cons
93
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
trans
appThm
appThm
nil
"x"
272
remove
var
902
def
345
ref
nil
cons
cons
nil
cons
nil
cons
cons
"A"
274
remove
cons
nil
cons
25
remove
cons
306
remove
subst
903
def
subst
trans
appThm
462
remove
50
ref
29
ref
99
ref
40
remove
appTerm
52
ref
appTerm
appTerm
52
ref
appTerm
absTerm
904
def
52
remove
appTerm
905
def
betaConv
nil
97
remove
904
ref
appTerm
906
def
axiom
nil
116
ref
906
remove
nil
cons
cons
98
ref
905
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
113
remove
105
remove
904
remove
nil
cons
cons
431
remove
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
subst
907
def
trans
sym
55
ref
eqMp
eqMp
nil
356
ref
890
ref
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
357
ref
890
ref
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
116
ref
33
ref
39
ref
358
ref
850
ref
appTerm
absTerm
appTerm
nil
cons
cons
98
ref
359
ref
850
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
92
ref
360
ref
890
ref
cons
nil
cons
cons
333
ref
subst
eqMp
nil
361
ref
362
ref
363
ref
858
remove
cons
nil
cons
cons
cons
nil
cons
cons
369
ref
subst
proveHyp
proveHyp
eqMp
nil
370
ref
890
remove
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
295
ref
855
remove
appTerm
thm
nil
298
remove
278
ref
290
remove
280
ref
237
remove
10
ref
99
remove
"Data.Sum.isRight"
const
8
remove
constTerm
908
def
21
ref
appTerm
appTerm
848
remove
281
ref
"Data.Sum.destRight"
const
787
remove
constTerm
909
def
21
remove
appTerm
appTerm
appTerm
appTerm
910
def
absTerm
911
def
appTerm
912
def
absTerm
913
def
appTerm
914
def
absTerm
915
def
nil
cons
cons
nil
cons
nil
cons
cons
856
remove
subst
278
remove
nil
50
ref
914
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
301
remove
913
remove
nil
cons
cons
nil
cons
nil
cons
cons
857
remove
subst
280
remove
nil
50
ref
912
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
9
remove
911
remove
nil
cons
cons
nil
cons
nil
cons
cons
49
remove
subst
10
remove
nil
50
ref
910
ref
nil
cons
916
def
cons
nil
cons
nil
cons
cons
56
ref
subst
251
remove
nil
253
remove
98
ref
916
ref
cons
nil
cons
917
def
cons
nil
cons
cons
918
def
176
ref
subst
proveHyp
918
ref
136
ref
subst
918
remove
161
ref
subst
nil
231
ref
70
ref
257
remove
910
ref
appTerm
919
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
233
remove
subst
70
ref
nil
50
ref
919
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
nil
260
remove
917
ref
cons
nil
cons
cons
920
def
136
ref
subst
920
remove
161
ref
subst
262
remove
nil
264
remove
917
ref
cons
nil
cons
cons
921
def
176
ref
subst
proveHyp
921
ref
136
ref
subst
921
remove
161
ref
subst
240
ref
908
ref
refl
922
def
268
ref
appThm
nil
50
ref
908
ref
72
ref
appTerm
923
def
nil
cons
cons
nil
cons
nil
cons
cons
56
ref
subst
70
ref
923
remove
absTerm
924
def
71
ref
appTerm
925
def
betaConv
nil
219
ref
924
ref
appTerm
926
def
axiom
nil
116
ref
926
remove
nil
cons
cons
98
ref
925
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
232
ref
231
ref
924
remove
nil
cons
cons
235
ref
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
eqMp
trans
appThm
883
remove
281
ref
refl
927
def
909
ref
refl
928
def
268
remove
appThm
70
remove
792
remove
909
ref
72
remove
appTerm
appTerm
71
ref
appTerm
absTerm
929
def
71
remove
appTerm
930
def
betaConv
nil
219
ref
929
ref
appTerm
931
def
axiom
nil
116
ref
931
remove
nil
cons
cons
98
ref
930
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
232
ref
231
remove
929
remove
nil
cons
cons
235
remove
cons
nil
cons
cons
181
ref
subst
eqMp
eqMp
trans
appThm
appThm
nil
902
remove
283
remove
nil
cons
cons
nil
cons
nil
cons
cons
903
remove
subst
trans
appThm
907
remove
trans
sym
55
ref
eqMp
eqMp
nil
308
remove
106
remove
916
ref
cons
nil
cons
932
def
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
310
remove
932
ref
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
116
ref
219
remove
234
remove
311
remove
910
ref
appTerm
absTerm
appTerm
nil
cons
cons
98
ref
312
remove
910
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
232
remove
313
remove
932
ref
cons
nil
cons
cons
333
ref
subst
eqMp
nil
34
ref
60
ref
335
remove
910
ref
appTerm
933
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
48
remove
subst
60
ref
nil
50
ref
933
remove
nil
cons
cons
nil
cons
nil
cons
cons
56
remove
subst
nil
338
remove
917
ref
cons
nil
cons
cons
934
def
136
ref
subst
934
remove
161
ref
subst
340
remove
nil
342
remove
917
remove
cons
nil
cons
cons
935
def
176
ref
subst
proveHyp
935
ref
136
remove
subst
935
remove
161
remove
subst
240
remove
922
remove
344
ref
appThm
60
remove
407
remove
908
remove
63
ref
appTerm
936
def
appTerm
937
def
absTerm
938
def
62
remove
appTerm
939
def
betaConv
nil
33
ref
938
ref
appTerm
940
def
axiom
nil
116
ref
940
remove
nil
cons
cons
98
ref
939
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
92
ref
34
remove
938
remove
nil
cons
cons
93
remove
cons
nil
cons
cons
181
remove
subst
eqMp
eqMp
nil
116
ref
937
remove
nil
cons
cons
98
ref
29
remove
936
ref
appTerm
426
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
ref
subst
proveHyp
nil
163
remove
936
remove
nil
cons
cons
nil
cons
nil
cons
cons
880
remove
subst
eqMp
trans
appThm
898
remove
927
remove
928
remove
344
remove
appThm
appThm
appThm
appThm
nil
50
remove
273
remove
345
remove
appTerm
281
remove
909
remove
63
remove
appTerm
appTerm
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
889
remove
subst
trans
sym
55
remove
eqMp
eqMp
nil
356
remove
932
ref
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
357
remove
932
ref
cons
nil
cons
cons
174
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
116
remove
33
remove
39
remove
358
remove
910
ref
appTerm
absTerm
appTerm
nil
cons
cons
98
remove
359
remove
910
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
176
remove
subst
proveHyp
92
remove
360
remove
932
ref
cons
nil
cons
cons
333
remove
subst
eqMp
nil
361
remove
362
remove
363
remove
916
remove
cons
nil
cons
cons
cons
nil
cons
cons
369
remove
subst
proveHyp
proveHyp
eqMp
nil
370
remove
932
remove
cons
nil
cons
cons
174
remove
subst
deductAntisym
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
295
remove
915
remove
appTerm
thm