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