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