6
version
"Data.Bool.==>"
const
"->"
typeOp
0
def
"bool"
typeOp
nil
opType
1
def
0
ref
1
ref
1
ref
nil
cons
2
def
cons
opType
3
def
nil
cons
cons
opType
4
def
constTerm
5
def
refl
6
def
"Data.Bool.~"
const
3
ref
constTerm
7
def
refl
8
def
nil
"t"
1
ref
var
9
def
"Data.List.null"
const
0
ref
"Data.List.list"
typeOp
10
def
"A"
varType
11
def
nil
cons
12
def
opType
13
def
2
ref
cons
opType
14
def
constTerm
15
def
"Data.List.[]"
const
13
ref
constTerm
16
def
appTerm
17
def
nil
cons
cons
nil
cons
nil
cons
cons
"="
const
18
def
4
ref
constTerm
19
def
9
ref
varTerm
20
def
appTerm
"Data.Bool.T"
const
1
ref
constTerm
21
def
appTerm
assume
sym
nil
21
ref
axiom
22
def
eqMp
20
ref
assume
22
ref
deductAntisym
deductAntisym
23
def
subst
nil
17
ref
axiom
eqMp
appThm
nil
19
ref
7
ref
21
ref
appTerm
24
def
appTerm
"Data.Bool.F"
const
1
ref
constTerm
25
def
appTerm
axiom
trans
appThm
18
ref
0
ref
11
ref
0
ref
11
ref
2
ref
cons
opType
26
def
nil
cons
27
def
cons
opType
constTerm
28
def
"Data.List.nth"
const
29
def
0
ref
13
ref
0
ref
"Number.Natural.natural"
typeOp
nil
opType
30
def
12
ref
cons
opType
31
def
nil
cons
cons
opType
constTerm
32
def
16
ref
appTerm
33
def
"Number.Natural.-"
const
0
ref
30
ref
0
ref
30
ref
30
ref
nil
cons
34
def
cons
opType
35
def
nil
cons
cons
opType
36
def
constTerm
37
def
"Data.List.length"
const
38
def
0
ref
13
ref
34
ref
cons
opType
constTerm
39
def
16
ref
appTerm
40
def
appTerm
"Number.Natural.bit1"
const
35
ref
constTerm
"Number.Natural.zero"
const
30
ref
constTerm
41
def
appTerm
42
def
appTerm
appTerm
appTerm
"Data.List.last"
const
0
ref
13
ref
12
ref
cons
opType
constTerm
43
def
16
ref
appTerm
appTerm
44
def
refl
appThm
nil
9
ref
44
ref
nil
cons
cons
nil
cons
nil
cons
cons
9
ref
19
ref
5
ref
25
ref
appTerm
45
def
20
ref
appTerm
appTerm
21
ref
appTerm
absTerm
46
def
20
ref
appTerm
47
def
betaConv
nil
"Data.Bool.!"
const
48
def
0
ref
3
ref
2
ref
cons
opType
49
def
constTerm
50
def
46
ref
appTerm
51
def
axiom
nil
"p"
1
ref
var
52
def
51
remove
nil
cons
cons
"q"
1
ref
var
53
def
47
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
19
ref
5
ref
52
ref
varTerm
54
def
appTerm
55
def
53
ref
varTerm
56
def
appTerm
57
def
appTerm
refl
52
ref
53
ref
19
ref
"Data.Bool./\\"
const
4
ref
constTerm
58
def
54
ref
appTerm
59
def
56
ref
appTerm
60
def
appTerm
61
def
54
ref
appTerm
absTerm
62
def
absTerm
63
def
54
ref
appTerm
betaConv
56
ref
refl
64
def
appThm
62
remove
56
ref
appTerm
betaConv
trans
appThm
nil
18
ref
0
ref
4
ref
0
ref
4
ref
2
ref
cons
opType
65
def
nil
cons
cons
opType
constTerm
66
def
5
ref
appTerm
63
remove
appTerm
axiom
54
ref
refl
67
def
appThm
64
ref
appThm
eqMp
68
def
sym
69
def
61
remove
refl
53
ref
18
ref
0
ref
65
ref
0
ref
65
remove
2
ref
cons
opType
nil
cons
cons
opType
constTerm
70
def
"f"
4
ref
var
71
def
71
ref
varTerm
72
def
54
ref
appTerm
56
ref
appTerm
absTerm
73
def
appTerm
71
ref
72
ref
21
ref
appTerm
21
ref
appTerm
absTerm
74
def
appTerm
absTerm
75
def
56
ref
appTerm
betaConv
appThm
18
ref
0
ref
3
ref
49
remove
nil
cons
cons
opType
constTerm
76
def
59
ref
appTerm
refl
52
ref
75
remove
absTerm
77
def
54
ref
appTerm
betaConv
appThm
nil
66
remove
58
ref
appTerm
77
ref
appTerm
axiom
78
def
67
remove
appThm
eqMp
64
ref
appThm
eqMp
79
def
sym
71
ref
72
ref
refl
nil
9
ref
54
ref
nil
cons
80
def
cons
nil
cons
nil
cons
cons
23
ref
subst
54
ref
assume
81
def
eqMp
appThm
nil
9
ref
56
ref
nil
cons
82
def
cons
nil
cons
nil
cons
cons
23
ref
subst
56
ref
assume
83
def
eqMp
appThm
absThm
eqMp
84
def
nil
"P"
1
ref
var
85
def
80
ref
cons
86
def
"Q"
1
ref
var
87
def
82
ref
cons
nil
cons
88
def
cons
nil
cons
cons
19
ref
refl
89
def
71
ref
72
remove
85
ref
varTerm
90
def
appTerm
91
def
87
ref
varTerm
92
def
appTerm
absTerm
93
def
52
ref
53
ref
54
ref
absTerm
absTerm
94
def
appTerm
betaConv
94
ref
90
ref
appTerm
betaConv
92
ref
refl
95
def
appThm
53
ref
90
ref
absTerm
92
ref
appTerm
betaConv
trans
trans
appThm
74
ref
94
ref
appTerm
betaConv
94
ref
21
ref
appTerm
betaConv
21
ref
refl
96
def
appThm
53
ref
21
ref
absTerm
21
ref
appTerm
betaConv
trans
trans
appThm
19
ref
58
ref
90
ref
appTerm
97
def
92
ref
appTerm
98
def
appTerm
refl
53
ref
70
remove
71
remove
91
remove
56
ref
appTerm
absTerm
appTerm
74
ref
appTerm
absTerm
92
ref
appTerm
betaConv
appThm
76
ref
97
remove
appTerm
refl
77
remove
90
ref
appTerm
betaConv
appThm
78
remove
90
ref
refl
99
def
appThm
eqMp
95
ref
appThm
eqMp
98
remove
assume
eqMp
100
def
94
remove
refl
appThm
eqMp
sym
22
ref
eqMp
101
def
subst
deductAntisym
eqMp
68
remove
57
ref
assume
102
def
eqMp
sym
81
remove
eqMp
89
ref
73
remove
52
ref
53
ref
56
ref
absTerm
103
def
absTerm
104
def
appTerm
betaConv
104
ref
54
ref
appTerm
betaConv
64
ref
appThm
103
ref
56
ref
appTerm
betaConv
trans
trans
appThm
74
remove
104
ref
appTerm
betaConv
104
ref
21
ref
appTerm
betaConv
96
remove
appThm
103
ref
21
ref
appTerm
betaConv
trans
trans
105
def
appThm
79
remove
60
remove
assume
eqMp
104
ref
refl
106
def
appThm
eqMp
sym
22
ref
eqMp
107
def
proveHyp
deductAntisym
108
def
subst
proveHyp
"A"
2
ref
cons
nil
cons
109
def
"P"
3
remove
var
110
def
46
remove
nil
cons
cons
"x"
1
ref
var
111
def
20
ref
nil
cons
cons
nil
cons
112
def
cons
nil
cons
cons
nil
52
ref
48
ref
0
ref
26
ref
2
ref
cons
opType
113
def
constTerm
114
def
"P"
26
ref
var
115
def
varTerm
116
def
appTerm
117
def
nil
cons
118
def
cons
53
ref
116
ref
"x"
11
ref
var
119
def
varTerm
120
def
appTerm
121
def
nil
cons
122
def
cons
nil
cons
cons
nil
cons
cons
123
def
69
ref
subst
123
remove
107
remove
84
remove
deductAntisym
124
def
subst
19
ref
121
ref
appTerm
refl
119
ref
21
ref
absTerm
125
def
120
ref
appTerm
betaConv
appThm
"p"
26
ref
var
126
def
18
ref
0
ref
26
ref
113
ref
nil
cons
cons
opType
constTerm
126
ref
varTerm
127
def
appTerm
125
remove
appTerm
absTerm
128
def
116
ref
appTerm
betaConv
129
def
nil
18
ref
0
ref
113
ref
0
ref
113
ref
2
ref
cons
opType
130
def
nil
cons
cons
opType
constTerm
131
def
114
ref
appTerm
128
remove
appTerm
axiom
116
ref
refl
132
def
appThm
133
def
117
ref
assume
eqMp
eqMp
120
ref
refl
134
def
appThm
eqMp
sym
22
ref
eqMp
eqMp
nil
85
ref
118
remove
cons
87
ref
122
ref
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
135
def
subst
eqMp
eqMp
136
def
subst
trans
sym
22
ref
eqMp
nil
52
ref
5
ref
7
ref
17
remove
appTerm
appTerm
44
remove
appTerm
137
def
nil
cons
cons
53
ref
114
ref
"h"
11
ref
var
138
def
48
ref
0
ref
14
ref
2
ref
cons
opType
139
def
constTerm
140
def
"t"
13
ref
var
141
def
5
ref
5
ref
7
ref
15
ref
141
ref
varTerm
142
def
appTerm
143
def
appTerm
144
def
appTerm
145
def
28
ref
32
ref
142
ref
appTerm
146
def
37
ref
39
ref
142
ref
appTerm
147
def
appTerm
42
ref
appTerm
appTerm
148
def
appTerm
43
ref
142
ref
appTerm
149
def
appTerm
150
def
appTerm
151
def
appTerm
152
def
5
ref
7
ref
15
ref
"Data.List.::"
const
153
def
0
ref
11
ref
0
ref
13
ref
13
ref
nil
cons
154
def
cons
opType
nil
cons
155
def
cons
opType
constTerm
156
def
138
ref
varTerm
157
def
appTerm
158
def
142
ref
appTerm
159
def
appTerm
160
def
appTerm
161
def
appTerm
28
ref
32
ref
159
ref
appTerm
162
def
37
ref
39
ref
159
ref
appTerm
163
def
appTerm
42
ref
appTerm
appTerm
appTerm
43
ref
159
ref
appTerm
164
def
appTerm
appTerm
165
def
appTerm
166
def
absTerm
167
def
appTerm
168
def
absTerm
169
def
appTerm
170
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
nil
115
ref
169
remove
nil
cons
cons
nil
cons
nil
cons
cons
19
ref
117
remove
appTerm
refl
129
remove
appThm
133
remove
eqMp
sym
171
def
subst
138
ref
nil
9
ref
168
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
"P"
14
ref
var
172
def
167
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
154
ref
cons
nil
cons
173
def
nil
nil
cons
174
def
cons
175
def
171
ref
subst
176
def
subst
141
ref
nil
9
ref
166
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
52
ref
151
remove
nil
cons
177
def
cons
178
def
53
ref
165
remove
nil
cons
179
def
cons
nil
cons
cons
nil
cons
cons
180
def
69
ref
subst
180
remove
124
ref
subst
6
ref
8
ref
141
ref
161
ref
absTerm
181
def
142
ref
appTerm
182
def
betaConv
138
ref
140
ref
181
ref
appTerm
183
def
absTerm
184
def
157
ref
appTerm
185
def
betaConv
nil
114
ref
184
ref
appTerm
186
def
axiom
nil
52
ref
186
remove
nil
cons
cons
53
ref
185
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
"A"
12
ref
cons
nil
cons
187
def
115
ref
184
remove
nil
cons
cons
119
ref
157
ref
nil
cons
188
def
cons
nil
cons
189
def
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
183
remove
nil
cons
cons
53
ref
182
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
181
remove
nil
cons
cons
"x"
13
ref
var
190
def
142
ref
nil
cons
191
def
cons
nil
cons
192
def
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
161
remove
nil
cons
cons
53
ref
19
ref
160
ref
appTerm
25
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
85
ref
160
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
52
ref
7
ref
90
ref
appTerm
193
def
nil
cons
194
def
cons
53
ref
19
ref
90
ref
appTerm
25
ref
appTerm
nil
cons
195
def
cons
nil
cons
cons
nil
cons
cons
196
def
69
ref
subst
196
remove
124
ref
subst
nil
52
ref
90
ref
nil
cons
197
def
cons
53
ref
25
ref
nil
cons
198
def
cons
nil
cons
cons
nil
cons
cons
6
ref
19
ref
54
ref
appTerm
56
ref
appTerm
199
def
assume
200
def
appThm
64
remove
appThm
sym
nil
52
ref
82
ref
cons
201
def
53
ref
82
ref
cons
nil
cons
cons
nil
cons
cons
202
def
69
ref
subst
202
remove
124
ref
subst
83
remove
eqMp
nil
85
ref
82
remove
cons
88
remove
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
203
def
eqMp
204
def
nil
52
ref
57
ref
nil
cons
205
def
cons
206
def
53
ref
5
ref
56
ref
appTerm
207
def
54
ref
appTerm
nil
cons
208
def
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
207
ref
refl
200
remove
appThm
sym
203
remove
eqMp
eqMp
nil
201
ref
53
ref
80
remove
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
nil
85
ref
205
ref
cons
209
def
87
ref
208
remove
cons
nil
cons
cons
nil
cons
cons
210
def
89
ref
93
remove
104
ref
appTerm
betaConv
104
remove
90
ref
appTerm
betaConv
95
remove
appThm
103
remove
92
ref
appTerm
betaConv
trans
trans
appThm
105
remove
appThm
100
remove
106
remove
appThm
eqMp
sym
22
ref
eqMp
211
def
subst
eqMp
108
ref
210
remove
101
ref
subst
eqMp
deductAntisym
deductAntisym
212
def
subst
19
ref
193
ref
appTerm
refl
52
ref
55
remove
25
ref
appTerm
absTerm
213
def
90
ref
appTerm
betaConv
appThm
nil
76
remove
7
ref
appTerm
213
remove
appTerm
axiom
99
remove
appThm
eqMp
193
remove
assume
eqMp
nil
52
ref
5
ref
90
ref
appTerm
25
ref
appTerm
nil
cons
cons
53
ref
45
remove
90
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
nil
52
ref
198
ref
cons
53
ref
197
ref
cons
nil
cons
cons
nil
cons
cons
214
def
69
ref
subst
214
remove
124
ref
subst
52
ref
54
remove
absTerm
215
def
90
remove
appTerm
216
def
betaConv
nil
19
ref
25
ref
appTerm
50
ref
215
ref
appTerm
217
def
appTerm
axiom
25
ref
assume
eqMp
nil
52
ref
217
remove
nil
cons
cons
53
ref
216
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
109
ref
110
ref
215
remove
nil
cons
cons
111
ref
197
ref
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
eqMp
nil
85
ref
198
ref
cons
87
ref
197
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
85
ref
194
remove
cons
87
ref
195
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
218
def
subst
eqMp
appThm
nil
19
ref
7
ref
25
ref
appTerm
219
def
appTerm
21
ref
appTerm
axiom
220
def
trans
appThm
28
ref
refl
221
def
162
ref
refl
222
def
37
ref
refl
223
def
141
ref
18
ref
0
ref
30
ref
0
ref
30
ref
2
ref
cons
opType
224
def
nil
cons
225
def
cons
opType
226
def
constTerm
227
def
163
ref
appTerm
"Number.Natural.suc"
const
35
remove
constTerm
228
def
147
ref
appTerm
229
def
appTerm
absTerm
230
def
142
ref
appTerm
231
def
betaConv
138
ref
140
ref
230
ref
appTerm
232
def
absTerm
233
def
157
ref
appTerm
234
def
betaConv
nil
114
ref
233
ref
appTerm
235
def
axiom
nil
52
ref
235
remove
nil
cons
cons
53
ref
234
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
233
remove
nil
cons
cons
189
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
232
remove
nil
cons
cons
53
ref
231
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
230
remove
nil
cons
cons
192
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
236
def
appThm
42
ref
refl
237
def
appThm
appThm
appThm
141
ref
28
ref
164
remove
appTerm
"Data.Bool.cond"
const
0
ref
1
ref
0
ref
11
ref
0
ref
11
ref
12
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
238
def
143
ref
appTerm
157
ref
appTerm
149
ref
appTerm
239
def
appTerm
absTerm
240
def
142
ref
appTerm
241
def
betaConv
138
ref
140
ref
240
ref
appTerm
242
def
absTerm
243
def
157
ref
appTerm
244
def
betaConv
nil
114
ref
243
ref
appTerm
245
def
axiom
nil
52
ref
245
remove
nil
cons
cons
53
ref
244
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
243
remove
nil
cons
cons
189
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
242
remove
nil
cons
cons
53
ref
241
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
240
remove
nil
cons
cons
192
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
appThm
appThm
nil
9
ref
28
ref
162
ref
37
ref
229
ref
appTerm
42
ref
appTerm
appTerm
appTerm
246
def
239
ref
appTerm
nil
cons
247
def
cons
nil
cons
nil
cons
cons
9
ref
19
ref
5
ref
21
ref
appTerm
20
ref
appTerm
appTerm
20
ref
appTerm
absTerm
248
def
20
ref
appTerm
249
def
betaConv
nil
50
ref
248
ref
appTerm
250
def
axiom
nil
52
ref
250
remove
nil
cons
cons
53
ref
249
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
109
ref
110
ref
248
remove
nil
cons
cons
112
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
251
def
subst
trans
sym
nil
178
remove
53
ref
247
remove
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
89
ref
"_16158"
11
ref
var
252
def
152
ref
246
ref
252
remove
varTerm
appTerm
appTerm
absTerm
253
def
239
remove
appTerm
betaConv
appThm
58
ref
refl
254
def
5
ref
143
ref
appTerm
255
def
refl
253
ref
157
ref
appTerm
betaConv
appThm
appThm
145
ref
refl
253
ref
149
ref
appTerm
betaConv
appThm
appThm
appThm
nil
"_485"
11
ref
var
256
def
149
ref
nil
cons
cons
"_482"
11
ref
var
257
def
188
ref
cons
"_483"
1
ref
var
258
def
143
ref
nil
cons
259
def
cons
nil
cons
cons
cons
nil
cons
cons
nil
"_484"
26
ref
var
260
def
253
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
119
ref
257
ref
varTerm
nil
cons
cons
"c"
1
ref
var
261
def
258
ref
varTerm
nil
cons
cons
126
ref
260
ref
varTerm
nil
cons
cons
"y"
11
ref
var
262
def
256
ref
varTerm
nil
cons
cons
nil
cons
cons
cons
cons
nil
cons
cons
262
ref
19
ref
127
ref
238
ref
261
ref
varTerm
263
def
appTerm
120
ref
appTerm
262
ref
varTerm
264
def
appTerm
appTerm
appTerm
58
ref
5
ref
263
ref
appTerm
127
ref
120
ref
appTerm
265
def
appTerm
appTerm
5
ref
7
ref
263
ref
appTerm
appTerm
127
ref
264
ref
appTerm
266
def
appTerm
appTerm
appTerm
absTerm
267
def
264
ref
appTerm
268
def
betaConv
119
ref
114
ref
267
ref
appTerm
269
def
absTerm
270
def
120
ref
appTerm
271
def
betaConv
261
remove
114
ref
270
ref
appTerm
272
def
absTerm
273
def
263
ref
appTerm
274
def
betaConv
126
ref
50
ref
273
ref
appTerm
275
def
absTerm
276
def
127
ref
appTerm
277
def
betaConv
nil
48
ref
130
remove
constTerm
278
def
276
ref
appTerm
279
def
axiom
nil
52
ref
279
remove
nil
cons
cons
53
ref
277
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
"A"
27
remove
cons
nil
cons
280
def
"P"
113
ref
var
281
def
276
remove
nil
cons
cons
"x"
26
ref
var
127
ref
nil
cons
cons
nil
cons
282
def
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
275
remove
nil
cons
cons
53
ref
274
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
109
ref
110
ref
273
remove
nil
cons
cons
111
ref
263
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
272
remove
nil
cons
cons
53
ref
271
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
270
remove
nil
cons
cons
119
ref
120
ref
nil
cons
283
def
cons
nil
cons
284
def
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
269
remove
nil
cons
cons
53
ref
268
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
267
remove
nil
cons
cons
119
ref
264
ref
nil
cons
cons
nil
cons
285
def
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
286
def
subst
subst
eqMp
sym
nil
52
ref
259
ref
cons
53
ref
152
ref
246
ref
157
ref
appTerm
287
def
appTerm
288
def
nil
cons
289
def
cons
nil
cons
cons
nil
cons
cons
290
def
69
ref
subst
290
remove
124
ref
subst
19
ref
"_16160"
1
ref
var
291
def
5
ref
5
ref
7
ref
291
remove
varTerm
appTerm
appTerm
150
ref
appTerm
appTerm
287
ref
appTerm
absTerm
292
def
143
ref
appTerm
293
def
appTerm
refl
292
ref
21
ref
appTerm
betaConv
appThm
89
ref
293
remove
betaConv
appThm
5
ref
5
ref
24
remove
appTerm
150
ref
appTerm
294
def
appTerm
287
ref
appTerm
refl
appThm
trans
292
remove
refl
nil
9
ref
259
ref
cons
nil
cons
nil
cons
cons
23
ref
subst
143
ref
assume
295
def
eqMp
appThm
eqMp
sym
nil
52
ref
294
remove
nil
cons
296
def
cons
53
ref
287
remove
nil
cons
297
def
cons
nil
cons
cons
nil
cons
cons
298
def
69
ref
subst
298
remove
124
ref
subst
19
ref
"_16164"
13
ref
var
299
def
28
ref
32
ref
158
ref
299
remove
varTerm
300
def
appTerm
appTerm
37
ref
228
ref
39
ref
300
remove
appTerm
appTerm
appTerm
42
ref
appTerm
appTerm
appTerm
157
ref
appTerm
absTerm
301
def
142
ref
appTerm
302
def
appTerm
refl
301
ref
16
ref
appTerm
betaConv
appThm
89
ref
302
remove
betaConv
appThm
28
ref
32
ref
158
ref
16
ref
appTerm
appTerm
303
def
37
ref
228
ref
40
ref
appTerm
appTerm
42
ref
appTerm
appTerm
appTerm
157
ref
appTerm
refl
appThm
trans
301
remove
refl
nil
"l"
13
ref
var
304
def
191
ref
cons
nil
cons
nil
cons
cons
305
def
304
ref
19
ref
15
remove
304
ref
varTerm
306
def
appTerm
307
def
appTerm
18
ref
0
ref
13
ref
14
ref
nil
cons
308
def
cons
opType
309
def
constTerm
310
def
306
ref
appTerm
16
ref
appTerm
311
def
appTerm
absTerm
312
def
306
ref
appTerm
313
def
betaConv
nil
140
ref
312
ref
appTerm
314
def
axiom
nil
52
ref
314
remove
nil
cons
cons
53
ref
313
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
312
remove
nil
cons
cons
190
ref
306
ref
nil
cons
cons
nil
cons
315
def
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
295
remove
eqMp
appThm
eqMp
sym
303
remove
refl
nil
"n"
30
ref
var
316
def
40
ref
nil
cons
cons
nil
cons
nil
cons
cons
316
ref
227
ref
37
ref
228
ref
316
ref
varTerm
317
def
appTerm
318
def
appTerm
42
ref
appTerm
appTerm
317
ref
appTerm
absTerm
319
def
317
ref
appTerm
320
def
betaConv
nil
48
ref
0
ref
224
ref
2
ref
cons
opType
321
def
constTerm
322
def
319
ref
appTerm
323
def
axiom
nil
52
ref
323
remove
nil
cons
cons
53
ref
320
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
"A"
34
ref
cons
324
def
nil
cons
325
def
"P"
224
ref
var
326
def
319
remove
nil
cons
cons
"x"
30
ref
var
327
def
317
ref
nil
cons
cons
nil
cons
328
def
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
329
def
subst
nil
227
ref
40
ref
appTerm
330
def
41
ref
appTerm
axiom
331
def
trans
appThm
nil
141
ref
16
ref
nil
cons
cons
nil
cons
nil
cons
cons
141
ref
28
ref
162
ref
41
ref
appTerm
332
def
appTerm
157
ref
appTerm
absTerm
333
def
142
ref
appTerm
334
def
betaConv
138
ref
140
ref
333
ref
appTerm
335
def
absTerm
336
def
157
ref
appTerm
337
def
betaConv
nil
114
ref
336
ref
appTerm
338
def
axiom
nil
52
ref
338
remove
nil
cons
cons
53
ref
337
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
336
remove
nil
cons
cons
189
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
335
remove
nil
cons
cons
53
ref
334
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
333
remove
nil
cons
cons
192
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
339
def
subst
trans
eqMp
eqMp
nil
85
ref
296
remove
cons
87
ref
297
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
85
ref
259
remove
cons
340
def
87
ref
289
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
nil
52
ref
255
remove
288
remove
appTerm
nil
cons
cons
53
ref
145
remove
152
remove
246
remove
149
ref
appTerm
341
def
appTerm
342
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
nil
52
ref
144
remove
nil
cons
343
def
cons
344
def
53
ref
342
remove
nil
cons
345
def
cons
nil
cons
cons
nil
cons
cons
346
def
69
ref
subst
346
remove
124
ref
subst
19
ref
"_16162"
1
ref
var
347
def
5
ref
5
ref
7
ref
347
remove
varTerm
appTerm
appTerm
150
ref
appTerm
appTerm
341
ref
appTerm
absTerm
348
def
143
ref
appTerm
349
def
appTerm
refl
348
ref
25
ref
appTerm
betaConv
appThm
89
ref
349
remove
betaConv
appThm
5
ref
5
ref
219
remove
appTerm
150
ref
appTerm
appTerm
341
remove
appTerm
refl
appThm
trans
348
remove
refl
nil
344
remove
53
ref
19
ref
143
remove
appTerm
25
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
nil
340
remove
nil
cons
nil
cons
cons
218
ref
subst
eqMp
350
def
appThm
eqMp
sym
6
ref
6
ref
220
ref
appThm
150
ref
refl
appThm
nil
9
ref
150
ref
nil
cons
351
def
cons
nil
cons
nil
cons
cons
251
ref
subst
trans
appThm
221
ref
222
ref
nil
316
ref
147
ref
nil
cons
352
def
cons
353
def
nil
cons
354
def
nil
cons
cons
355
def
329
ref
subst
appThm
appThm
149
ref
refl
appThm
appThm
sym
nil
52
ref
351
ref
cons
53
ref
28
ref
162
ref
147
ref
appTerm
appTerm
356
def
149
ref
appTerm
nil
cons
357
def
cons
nil
cons
cons
nil
cons
cons
358
def
69
ref
subst
358
remove
124
ref
subst
19
ref
"_16166"
11
ref
var
359
def
356
ref
359
remove
varTerm
appTerm
absTerm
360
def
149
remove
appTerm
361
def
appTerm
refl
360
ref
148
ref
appTerm
betaConv
appThm
89
ref
361
remove
betaConv
appThm
356
remove
148
remove
appTerm
362
def
refl
363
def
appThm
trans
360
remove
refl
150
remove
assume
sym
appThm
eqMp
sym
"m"
30
ref
var
364
def
"Data.Bool.\\/"
const
4
remove
constTerm
365
def
227
ref
364
ref
varTerm
366
def
appTerm
367
def
41
ref
appTerm
appTerm
"Data.Bool.?"
const
368
def
321
ref
constTerm
369
def
316
ref
367
ref
318
ref
appTerm
absTerm
appTerm
appTerm
absTerm
370
def
147
ref
appTerm
371
def
betaConv
nil
322
ref
370
ref
appTerm
372
def
axiom
nil
52
ref
372
remove
nil
cons
cons
53
ref
371
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
370
remove
nil
cons
cons
327
ref
352
ref
cons
nil
cons
373
def
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
365
ref
227
ref
147
ref
appTerm
374
def
41
ref
appTerm
appTerm
369
ref
316
ref
374
remove
318
ref
appTerm
375
def
absTerm
376
def
appTerm
377
def
appTerm
nil
cons
cons
53
ref
362
ref
nil
cons
378
def
cons
nil
cons
379
def
cons
nil
cons
cons
108
ref
subst
proveHyp
6
ref
365
ref
refl
305
ref
304
ref
19
ref
227
ref
39
ref
306
ref
appTerm
380
def
appTerm
41
ref
appTerm
appTerm
381
def
307
ref
appTerm
absTerm
382
def
306
ref
appTerm
383
def
betaConv
nil
140
ref
382
ref
appTerm
384
def
axiom
nil
52
ref
384
remove
nil
cons
cons
53
ref
383
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
382
remove
nil
cons
cons
315
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
350
remove
trans
appThm
377
ref
refl
appThm
nil
9
ref
377
ref
nil
cons
cons
nil
cons
nil
cons
cons
9
ref
19
ref
365
remove
25
ref
appTerm
20
ref
appTerm
appTerm
20
ref
appTerm
absTerm
385
def
20
ref
appTerm
386
def
betaConv
nil
50
ref
385
ref
appTerm
387
def
axiom
nil
52
ref
387
remove
nil
cons
cons
53
ref
386
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
109
ref
110
ref
385
remove
nil
cons
cons
112
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
trans
appThm
363
remove
appThm
sym
nil
326
ref
316
ref
5
ref
376
ref
317
ref
appTerm
388
def
appTerm
362
ref
appTerm
389
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
325
ref
174
ref
cons
390
def
171
ref
subst
391
def
subst
316
ref
nil
9
ref
389
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
52
ref
388
ref
nil
cons
392
def
cons
379
ref
cons
nil
cons
cons
393
def
69
ref
subst
393
remove
124
ref
subst
388
ref
betaConv
388
remove
assume
eqMp
nil
52
ref
375
ref
nil
cons
394
def
cons
379
remove
cons
nil
cons
cons
395
def
108
ref
subst
proveHyp
395
ref
69
ref
subst
395
remove
124
ref
subst
221
ref
222
remove
375
remove
assume
396
def
appThm
appThm
146
ref
refl
223
remove
396
ref
appThm
237
remove
appThm
329
remove
trans
appThm
appThm
sym
"Number.Natural.<"
const
226
ref
constTerm
397
def
317
ref
appTerm
398
def
refl
396
remove
appThm
nil
9
ref
398
ref
318
ref
appTerm
399
def
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
316
ref
399
remove
absTerm
400
def
317
ref
appTerm
401
def
betaConv
nil
322
ref
400
ref
appTerm
402
def
axiom
nil
52
ref
402
remove
nil
cons
cons
53
ref
401
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
400
remove
nil
cons
cons
328
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
eqMp
trans
sym
22
ref
eqMp
nil
52
ref
398
ref
147
ref
appTerm
403
def
nil
cons
cons
53
ref
28
ref
162
ref
318
ref
appTerm
appTerm
146
ref
317
ref
appTerm
appTerm
404
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
316
ref
5
ref
403
remove
appTerm
404
remove
appTerm
absTerm
405
def
317
ref
appTerm
406
def
betaConv
141
ref
322
ref
405
ref
appTerm
407
def
absTerm
408
def
142
ref
appTerm
409
def
betaConv
138
ref
140
ref
408
ref
appTerm
410
def
absTerm
411
def
157
ref
appTerm
412
def
betaConv
nil
114
ref
411
ref
appTerm
413
def
axiom
nil
52
ref
413
remove
nil
cons
cons
53
ref
412
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
411
remove
nil
cons
cons
189
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
414
def
nil
52
ref
410
remove
nil
cons
cons
415
def
53
ref
409
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
408
ref
nil
cons
cons
416
def
192
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
407
remove
nil
cons
cons
53
ref
406
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
405
remove
nil
cons
cons
328
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
417
def
eqMp
eqMp
eqMp
nil
85
ref
394
remove
cons
87
ref
378
remove
cons
nil
cons
418
def
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
85
ref
392
remove
cons
418
ref
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
52
ref
322
ref
327
ref
5
ref
376
ref
327
ref
varTerm
419
def
appTerm
appTerm
362
ref
appTerm
absTerm
appTerm
nil
cons
cons
53
ref
5
ref
377
remove
appTerm
362
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
376
remove
nil
cons
cons
418
remove
cons
nil
cons
cons
nil
52
ref
114
ref
119
ref
5
ref
121
remove
appTerm
420
def
92
ref
appTerm
absTerm
421
def
appTerm
422
def
nil
cons
423
def
cons
424
def
53
ref
5
ref
368
ref
113
remove
constTerm
425
def
116
ref
appTerm
426
def
appTerm
427
def
92
ref
appTerm
nil
cons
428
def
cons
nil
cons
cons
nil
cons
cons
429
def
69
ref
subst
429
remove
124
ref
subst
nil
52
ref
426
ref
nil
cons
430
def
cons
431
def
53
ref
92
ref
nil
cons
432
def
cons
nil
cons
433
def
cons
nil
cons
cons
434
def
69
ref
subst
434
remove
124
ref
subst
nil
424
ref
433
ref
cons
nil
cons
cons
435
def
108
ref
subst
53
ref
5
ref
114
ref
119
ref
420
remove
56
ref
appTerm
absTerm
appTerm
appTerm
56
ref
appTerm
absTerm
436
def
92
ref
appTerm
437
def
betaConv
nil
431
remove
53
ref
50
ref
436
ref
appTerm
438
def
nil
cons
439
def
cons
nil
cons
cons
nil
cons
cons
440
def
108
ref
subst
19
ref
426
remove
appTerm
441
def
refl
126
ref
50
ref
53
ref
5
ref
114
ref
119
ref
5
ref
265
ref
appTerm
56
ref
appTerm
absTerm
appTerm
appTerm
56
remove
appTerm
absTerm
appTerm
absTerm
442
def
116
remove
appTerm
betaConv
appThm
nil
131
remove
425
ref
appTerm
442
remove
appTerm
axiom
132
remove
appThm
eqMp
443
def
nil
52
ref
441
remove
438
ref
appTerm
nil
cons
cons
53
ref
427
remove
438
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
440
remove
nil
52
ref
199
remove
nil
cons
444
def
cons
53
ref
205
ref
cons
nil
cons
cons
nil
cons
cons
445
def
69
ref
subst
445
remove
124
ref
subst
204
remove
eqMp
nil
85
ref
444
remove
cons
87
ref
205
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
52
ref
439
remove
cons
53
ref
437
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
109
ref
110
ref
436
remove
nil
cons
cons
111
ref
432
ref
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
85
ref
430
remove
cons
87
ref
432
remove
cons
nil
cons
446
def
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
nil
85
ref
423
remove
cons
447
def
87
ref
428
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
448
def
subst
eqMp
eqMp
eqMp
eqMp
eqMp
nil
85
ref
351
remove
cons
87
ref
357
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
85
ref
343
remove
cons
87
ref
345
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
nil
85
ref
177
remove
cons
87
ref
179
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
52
ref
58
ref
137
remove
appTerm
170
remove
appTerm
nil
cons
cons
53
ref
140
ref
304
ref
5
ref
7
ref
307
remove
appTerm
appTerm
28
ref
32
ref
306
ref
appTerm
449
def
37
ref
380
ref
appTerm
42
remove
appTerm
appTerm
appTerm
43
remove
306
ref
appTerm
appTerm
appTerm
absTerm
450
def
appTerm
451
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
6
ref
254
ref
450
ref
16
ref
appTerm
betaConv
appThm
114
ref
refl
452
def
138
ref
140
ref
refl
453
def
141
ref
6
ref
450
ref
142
ref
appTerm
betaConv
appThm
450
ref
159
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
453
ref
304
ref
450
ref
306
ref
appTerm
betaConv
absThm
appThm
appThm
nil
"p"
14
ref
var
454
def
450
remove
nil
cons
cons
nil
cons
nil
cons
cons
454
ref
5
ref
58
ref
454
ref
varTerm
455
def
16
ref
appTerm
appTerm
114
ref
138
ref
140
ref
141
ref
5
ref
455
ref
142
ref
appTerm
appTerm
455
ref
159
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
140
ref
304
ref
455
ref
306
ref
appTerm
absTerm
appTerm
appTerm
absTerm
456
def
455
ref
appTerm
457
def
betaConv
nil
48
ref
0
ref
139
ref
2
ref
cons
opType
constTerm
456
ref
appTerm
458
def
axiom
nil
52
ref
458
remove
nil
cons
cons
53
ref
457
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
"A"
308
ref
cons
nil
cons
"P"
139
remove
var
456
remove
nil
cons
cons
"x"
14
remove
var
455
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
459
def
subst
eqMp
eqMp
nil
451
remove
thm
278
ref
refl
460
def
126
ref
453
ref
304
ref
89
ref
304
ref
19
ref
"Data.List.all"
const
0
ref
26
ref
308
ref
cons
opType
461
def
constTerm
127
ref
appTerm
306
ref
appTerm
appTerm
462
def
114
ref
119
ref
5
ref
"Set.member"
const
463
def
0
ref
11
ref
0
ref
"Set.set"
typeOp
464
def
12
ref
opType
465
def
2
ref
cons
opType
466
def
nil
cons
467
def
cons
opType
constTerm
468
def
120
ref
appTerm
469
def
"Data.List.toSet"
const
0
ref
13
ref
465
ref
nil
cons
470
def
cons
opType
constTerm
471
def
306
ref
appTerm
472
def
appTerm
473
def
appTerm
265
ref
appTerm
absTerm
appTerm
appTerm
absTerm
474
def
306
ref
appTerm
475
def
betaConv
126
ref
140
ref
474
ref
appTerm
476
def
absTerm
477
def
127
ref
appTerm
478
def
betaConv
nil
278
ref
477
ref
appTerm
479
def
axiom
nil
52
ref
479
remove
nil
cons
cons
53
ref
478
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
280
ref
281
ref
477
remove
nil
cons
cons
282
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
476
remove
nil
cons
cons
53
ref
475
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
474
remove
nil
cons
cons
315
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
452
ref
119
ref
6
ref
469
ref
refl
304
ref
18
ref
0
ref
465
ref
467
remove
cons
opType
constTerm
480
def
472
remove
appTerm
"Set.image"
const
481
def
0
ref
31
ref
0
ref
464
ref
34
ref
opType
482
def
470
ref
cons
opType
nil
cons
cons
opType
constTerm
483
def
449
ref
appTerm
"Set.fromPredicate"
const
484
def
0
ref
224
ref
482
ref
nil
cons
485
def
cons
opType
constTerm
486
def
"v"
30
ref
var
487
def
369
ref
"i"
30
ref
var
488
def
58
ref
227
ref
487
ref
varTerm
appTerm
489
def
488
ref
varTerm
490
def
appTerm
491
def
appTerm
492
def
397
ref
490
ref
appTerm
493
def
380
ref
appTerm
494
def
appTerm
absTerm
appTerm
absTerm
appTerm
495
def
appTerm
appTerm
absTerm
496
def
306
ref
appTerm
497
def
betaConv
498
def
480
ref
refl
499
def
nil
480
ref
471
ref
16
ref
appTerm
appTerm
500
def
"Set.{}"
const
501
def
465
ref
constTerm
502
def
appTerm
axiom
appThm
483
ref
33
ref
appTerm
503
def
refl
486
ref
refl
504
def
487
ref
369
ref
refl
505
def
488
ref
492
ref
refl
506
def
493
ref
refl
507
def
331
ref
appThm
508
def
nil
364
ref
490
ref
nil
cons
509
def
cons
nil
cons
510
def
nil
cons
cons
364
ref
7
ref
397
ref
366
ref
appTerm
511
def
41
ref
appTerm
512
def
appTerm
513
def
absTerm
514
def
366
ref
appTerm
515
def
betaConv
nil
322
ref
514
ref
appTerm
516
def
axiom
nil
52
ref
516
remove
nil
cons
cons
53
ref
515
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
514
remove
nil
cons
cons
327
ref
366
ref
nil
cons
cons
nil
cons
517
def
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
513
remove
nil
cons
cons
53
ref
19
ref
512
ref
appTerm
25
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
85
ref
512
remove
nil
cons
cons
nil
cons
nil
cons
cons
218
ref
subst
eqMp
518
def
subst
trans
519
def
appThm
nil
9
ref
491
remove
nil
cons
cons
nil
cons
nil
cons
cons
9
ref
19
ref
58
ref
20
ref
appTerm
520
def
25
ref
appTerm
appTerm
25
ref
appTerm
absTerm
521
def
20
ref
appTerm
522
def
betaConv
nil
50
ref
521
ref
appTerm
523
def
axiom
nil
52
ref
523
remove
nil
cons
cons
53
ref
522
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
109
ref
110
ref
521
remove
nil
cons
cons
112
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
trans
absThm
appThm
nil
9
ref
198
remove
cons
nil
cons
nil
cons
cons
390
ref
9
ref
19
ref
425
ref
119
ref
20
ref
absTerm
524
def
appTerm
appTerm
20
ref
appTerm
absTerm
525
def
20
ref
appTerm
526
def
betaConv
nil
50
ref
525
ref
appTerm
527
def
axiom
nil
52
ref
527
remove
nil
cons
cons
53
ref
526
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
109
ref
110
ref
525
remove
nil
cons
cons
112
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
subst
trans
absThm
appThm
390
ref
nil
480
ref
484
remove
0
ref
26
remove
470
ref
cons
opType
constTerm
528
def
119
ref
25
ref
absTerm
appTerm
appTerm
502
ref
appTerm
axiom
subst
trans
appThm
nil
"f"
31
remove
var
529
def
33
ref
nil
cons
cons
nil
cons
nil
cons
cons
324
remove
"B"
12
remove
cons
nil
cons
cons
174
ref
cons
530
def
"f"
0
ref
11
ref
"B"
varType
531
def
nil
cons
532
def
cons
opType
533
def
var
534
def
18
ref
0
ref
464
remove
532
ref
opType
535
def
0
ref
535
ref
2
ref
cons
opType
nil
cons
536
def
cons
opType
constTerm
537
def
481
remove
0
ref
533
ref
0
ref
465
ref
535
ref
nil
cons
538
def
cons
opType
nil
cons
cons
opType
constTerm
534
ref
varTerm
539
def
appTerm
540
def
502
ref
appTerm
appTerm
501
remove
535
ref
constTerm
appTerm
absTerm
541
def
539
ref
appTerm
542
def
betaConv
nil
48
ref
0
ref
0
ref
533
ref
2
ref
cons
opType
543
def
2
ref
cons
opType
constTerm
544
def
541
ref
appTerm
545
def
axiom
nil
52
ref
545
remove
nil
cons
cons
53
ref
542
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
"A"
533
ref
nil
cons
cons
nil
cons
546
def
"P"
543
remove
var
547
def
541
remove
nil
cons
cons
"x"
533
ref
var
539
ref
nil
cons
cons
nil
cons
548
def
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
subst
trans
appThm
nil
"x"
465
ref
var
549
def
502
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
470
ref
cons
nil
cons
550
def
174
ref
cons
nil
9
ref
28
ref
120
ref
appTerm
551
def
120
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
134
remove
eqMp
552
def
subst
subst
trans
sym
22
ref
eqMp
nil
52
ref
500
remove
503
remove
486
ref
487
ref
369
ref
488
ref
492
ref
493
ref
40
ref
appTerm
553
def
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
554
def
nil
cons
cons
53
ref
114
ref
138
ref
140
ref
141
ref
5
ref
480
ref
471
ref
142
ref
appTerm
555
def
appTerm
483
ref
146
ref
appTerm
486
ref
487
ref
369
ref
488
ref
492
ref
493
ref
147
ref
appTerm
556
def
appTerm
absTerm
appTerm
absTerm
appTerm
557
def
appTerm
558
def
appTerm
559
def
appTerm
480
ref
471
remove
159
ref
appTerm
appTerm
560
def
483
remove
162
ref
appTerm
561
def
486
ref
487
ref
369
ref
488
ref
492
remove
493
ref
163
ref
appTerm
562
def
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
563
def
appTerm
564
def
absTerm
565
def
appTerm
566
def
absTerm
567
def
appTerm
568
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
nil
115
ref
567
remove
nil
cons
cons
nil
cons
nil
cons
cons
171
ref
subst
138
ref
nil
9
ref
566
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
172
ref
565
remove
nil
cons
cons
nil
cons
nil
cons
cons
176
ref
subst
141
ref
nil
9
ref
564
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
52
ref
559
ref
nil
cons
569
def
cons
53
ref
563
remove
nil
cons
570
def
cons
nil
cons
cons
nil
cons
cons
571
def
69
ref
subst
571
remove
124
ref
subst
499
remove
141
ref
560
remove
"Set.insert"
const
572
def
0
ref
11
ref
0
ref
465
ref
470
remove
cons
opType
nil
cons
cons
opType
constTerm
573
def
157
ref
appTerm
574
def
555
remove
appTerm
appTerm
absTerm
575
def
142
ref
appTerm
576
def
betaConv
138
ref
140
ref
575
ref
appTerm
577
def
absTerm
578
def
157
ref
appTerm
579
def
betaConv
nil
114
ref
578
ref
appTerm
580
def
axiom
nil
52
ref
580
remove
nil
cons
cons
53
ref
579
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
578
remove
nil
cons
cons
189
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
577
remove
nil
cons
cons
53
ref
576
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
575
remove
nil
cons
cons
192
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
574
remove
refl
581
def
559
remove
assume
appThm
trans
appThm
561
ref
refl
504
ref
487
ref
505
ref
488
ref
506
ref
507
ref
236
ref
appThm
582
def
appThm
absThm
appThm
absThm
appThm
355
ref
316
ref
18
ref
0
ref
482
ref
0
ref
482
ref
2
ref
cons
opType
nil
cons
583
def
cons
opType
constTerm
486
ref
487
ref
369
ref
364
ref
58
ref
489
ref
366
ref
appTerm
appTerm
511
ref
318
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
572
ref
0
ref
30
ref
0
ref
482
ref
485
remove
cons
opType
nil
cons
cons
opType
constTerm
41
ref
appTerm
486
ref
487
ref
369
ref
364
ref
58
ref
489
ref
228
ref
366
ref
appTerm
584
def
appTerm
appTerm
511
remove
317
ref
appTerm
585
def
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
absTerm
586
def
317
ref
appTerm
587
def
betaConv
nil
322
ref
586
ref
appTerm
588
def
axiom
nil
52
ref
588
remove
nil
cons
cons
53
ref
587
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
586
remove
nil
cons
cons
328
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
trans
appThm
nil
"s"
482
remove
var
589
def
486
remove
487
ref
369
ref
488
ref
58
ref
489
remove
228
ref
490
ref
appTerm
590
def
appTerm
appTerm
556
ref
appTerm
absTerm
appTerm
absTerm
591
def
appTerm
592
def
nil
cons
cons
593
def
327
ref
41
ref
nil
cons
594
def
cons
595
def
529
ref
162
ref
nil
cons
cons
596
def
nil
cons
597
def
cons
cons
nil
cons
cons
530
ref
"s"
465
ref
var
598
def
537
remove
540
ref
573
ref
120
ref
appTerm
598
ref
varTerm
599
def
appTerm
appTerm
appTerm
572
remove
0
ref
531
ref
0
ref
535
remove
538
remove
cons
opType
nil
cons
cons
opType
constTerm
539
ref
120
ref
appTerm
600
def
appTerm
540
remove
599
ref
appTerm
601
def
appTerm
appTerm
absTerm
602
def
599
ref
appTerm
603
def
betaConv
119
ref
48
ref
0
ref
466
ref
2
ref
cons
opType
constTerm
604
def
602
ref
appTerm
605
def
absTerm
606
def
120
ref
appTerm
607
def
betaConv
534
ref
114
ref
606
ref
appTerm
608
def
absTerm
609
def
539
ref
appTerm
610
def
betaConv
nil
544
ref
609
ref
appTerm
611
def
axiom
nil
52
ref
611
remove
nil
cons
cons
53
ref
610
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
546
ref
547
ref
609
remove
nil
cons
cons
548
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
608
remove
nil
cons
cons
53
ref
607
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
606
remove
nil
cons
cons
284
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
605
remove
nil
cons
cons
53
ref
603
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
550
ref
"P"
466
remove
var
612
def
602
remove
nil
cons
cons
549
ref
599
ref
nil
cons
cons
nil
cons
613
def
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
subst
573
remove
refl
339
ref
appThm
561
remove
592
ref
appTerm
614
def
refl
appThm
trans
trans
appThm
sym
581
remove
nil
"t"
465
remove
var
615
def
614
ref
nil
cons
cons
598
ref
558
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
615
ref
19
ref
480
remove
599
ref
appTerm
615
ref
varTerm
616
def
appTerm
617
def
appTerm
114
ref
119
ref
19
ref
469
ref
599
ref
appTerm
618
def
appTerm
469
ref
616
ref
appTerm
appTerm
absTerm
appTerm
619
def
appTerm
absTerm
620
def
616
ref
appTerm
621
def
betaConv
598
ref
604
ref
620
ref
appTerm
622
def
absTerm
623
def
599
ref
appTerm
624
def
betaConv
604
ref
refl
625
def
598
ref
625
remove
615
ref
nil
"y"
1
ref
var
619
ref
nil
cons
cons
111
ref
617
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
109
ref
174
ref
cons
626
def
262
ref
19
ref
551
ref
264
ref
appTerm
627
def
appTerm
28
ref
264
ref
appTerm
120
ref
appTerm
628
def
appTerm
absTerm
629
def
264
ref
appTerm
630
def
betaConv
119
ref
114
ref
629
ref
appTerm
631
def
absTerm
632
def
120
ref
appTerm
633
def
betaConv
nil
114
ref
632
ref
appTerm
634
def
axiom
nil
52
ref
634
remove
nil
cons
cons
53
ref
633
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
632
remove
nil
cons
cons
284
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
631
remove
nil
cons
cons
53
ref
630
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
629
remove
nil
cons
cons
285
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
subst
absThm
appThm
absThm
appThm
sym
nil
604
ref
598
ref
604
ref
615
remove
19
ref
619
remove
appTerm
617
remove
appTerm
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
52
ref
604
ref
623
ref
appTerm
nil
cons
cons
53
ref
624
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
550
ref
612
ref
623
remove
nil
cons
cons
613
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
622
remove
nil
cons
cons
53
ref
621
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
550
ref
612
ref
620
remove
nil
cons
cons
549
remove
616
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
sym
nil
115
ref
119
ref
19
ref
469
ref
558
ref
appTerm
635
def
appTerm
469
ref
614
ref
appTerm
636
def
appTerm
637
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
171
ref
subst
119
ref
nil
9
ref
637
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
52
ref
635
ref
nil
cons
cons
53
ref
636
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
212
remove
subst
119
ref
5
ref
635
ref
appTerm
638
def
636
ref
appTerm
639
def
absTerm
640
def
120
ref
appTerm
641
def
betaConv
89
ref
452
ref
119
ref
638
remove
refl
119
ref
636
ref
absTerm
642
def
120
ref
appTerm
betaConv
appThm
absThm
appThm
appThm
322
ref
refl
643
def
327
ref
5
ref
463
ref
0
ref
30
ref
583
remove
cons
opType
constTerm
644
def
419
ref
appTerm
645
def
557
ref
appTerm
646
def
appTerm
refl
642
ref
146
ref
419
ref
appTerm
647
def
appTerm
betaConv
appThm
absThm
appThm
appThm
nil
126
ref
642
remove
nil
cons
cons
589
ref
557
remove
nil
cons
cons
648
def
529
ref
146
ref
nil
cons
cons
649
def
nil
cons
cons
cons
nil
cons
cons
530
ref
598
ref
19
ref
48
ref
0
ref
0
ref
531
ref
2
ref
cons
opType
650
def
2
ref
cons
opType
651
def
constTerm
652
def
"y"
531
ref
var
653
def
5
ref
463
remove
0
ref
531
ref
536
remove
cons
opType
constTerm
653
ref
varTerm
654
def
appTerm
601
remove
appTerm
655
def
appTerm
"p"
650
ref
var
656
def
varTerm
657
def
654
ref
appTerm
658
def
appTerm
absTerm
appTerm
appTerm
114
ref
119
ref
5
ref
618
ref
appTerm
657
ref
600
ref
appTerm
659
def
appTerm
absTerm
appTerm
appTerm
absTerm
660
def
599
ref
appTerm
661
def
betaConv
534
ref
604
ref
660
ref
appTerm
662
def
absTerm
663
def
539
ref
appTerm
664
def
betaConv
656
ref
544
ref
663
ref
appTerm
665
def
absTerm
666
def
657
ref
appTerm
667
def
betaConv
nil
48
ref
0
ref
651
ref
2
ref
cons
opType
constTerm
668
def
666
ref
appTerm
669
def
axiom
nil
52
ref
669
remove
nil
cons
cons
53
ref
667
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
"A"
650
ref
nil
cons
670
def
cons
nil
cons
671
def
"P"
651
ref
var
672
def
666
remove
nil
cons
cons
"x"
650
ref
var
657
ref
nil
cons
cons
nil
cons
673
def
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
665
remove
nil
cons
cons
53
ref
664
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
546
ref
547
ref
663
remove
nil
cons
cons
548
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
662
remove
nil
cons
cons
53
ref
661
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
550
ref
612
ref
660
remove
nil
cons
cons
613
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
674
def
subst
eqMp
643
ref
327
ref
6
ref
89
ref
645
ref
refl
675
def
504
ref
487
ref
505
ref
488
ref
506
ref
488
ref
556
ref
absTerm
676
def
490
ref
appTerm
betaConv
677
def
appThm
absThm
appThm
absThm
appThm
678
def
appThm
appThm
676
ref
419
ref
appTerm
betaConv
appThm
nil
"p"
224
ref
var
679
def
676
remove
nil
cons
cons
680
def
nil
cons
nil
cons
cons
390
ref
119
ref
19
ref
469
ref
528
ref
"v"
11
ref
var
681
def
425
ref
262
ref
58
ref
28
ref
681
remove
varTerm
appTerm
264
ref
appTerm
appTerm
266
remove
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
265
ref
appTerm
absTerm
682
def
120
ref
appTerm
683
def
betaConv
126
ref
114
ref
682
ref
appTerm
684
def
absTerm
685
def
127
ref
appTerm
686
def
betaConv
nil
278
ref
685
ref
appTerm
687
def
axiom
nil
52
ref
687
remove
nil
cons
cons
53
ref
686
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
280
ref
281
ref
685
remove
nil
cons
cons
282
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
684
remove
nil
cons
cons
53
ref
683
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
682
remove
nil
cons
cons
284
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
688
def
subst
eqMp
appThm
468
ref
647
ref
appTerm
614
remove
appTerm
689
def
refl
appThm
absThm
appThm
trans
sym
nil
326
ref
327
ref
5
ref
397
ref
419
ref
appTerm
690
def
147
ref
appTerm
691
def
appTerm
689
ref
appTerm
692
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
391
ref
subst
327
ref
nil
9
ref
692
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
52
ref
691
ref
nil
cons
693
def
cons
694
def
53
ref
689
remove
nil
cons
695
def
cons
nil
cons
cons
nil
cons
cons
696
def
69
ref
subst
696
remove
124
ref
subst
nil
593
ref
596
remove
262
ref
647
ref
nil
cons
cons
nil
cons
697
def
cons
cons
nil
cons
cons
530
ref
534
ref
19
ref
655
ref
appTerm
425
ref
119
ref
58
ref
18
ref
0
ref
531
ref
670
ref
cons
opType
constTerm
698
def
654
ref
appTerm
600
remove
appTerm
appTerm
618
ref
appTerm
absTerm
appTerm
appTerm
absTerm
699
def
539
ref
appTerm
700
def
betaConv
598
ref
544
ref
699
ref
appTerm
701
def
absTerm
702
def
599
ref
appTerm
703
def
betaConv
653
ref
604
ref
702
ref
appTerm
704
def
absTerm
705
def
654
ref
appTerm
706
def
betaConv
nil
652
ref
705
ref
appTerm
707
def
axiom
nil
52
ref
707
remove
nil
cons
cons
53
ref
706
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
"A"
532
ref
cons
nil
cons
708
def
"P"
650
remove
var
705
remove
nil
cons
cons
"x"
531
ref
var
709
def
654
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
704
remove
nil
cons
cons
53
ref
703
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
550
ref
612
ref
702
remove
nil
cons
cons
613
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
701
remove
nil
cons
cons
53
ref
700
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
546
ref
547
ref
699
remove
nil
cons
cons
548
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
710
def
subst
sym
"x'"
30
ref
var
711
def
58
ref
28
ref
647
ref
appTerm
712
def
162
ref
711
ref
varTerm
713
def
appTerm
appTerm
appTerm
644
ref
713
ref
appTerm
592
ref
appTerm
appTerm
absTerm
714
def
228
ref
419
ref
appTerm
715
def
appTerm
betaConv
sym
nil
694
remove
53
ref
28
ref
162
ref
715
ref
appTerm
716
def
appTerm
647
ref
appTerm
nil
cons
717
def
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
nil
316
ref
419
ref
nil
cons
718
def
cons
nil
cons
nil
cons
cons
417
ref
subst
eqMp
nil
52
ref
717
remove
cons
53
ref
712
remove
716
ref
appTerm
nil
cons
719
def
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
119
ref
716
remove
nil
cons
cons
697
remove
cons
nil
cons
cons
119
ref
5
ref
627
remove
appTerm
628
remove
appTerm
720
def
absTerm
721
def
120
ref
appTerm
722
def
betaConv
262
ref
114
ref
721
ref
appTerm
723
def
absTerm
724
def
264
ref
appTerm
725
def
betaConv
nil
114
ref
119
ref
114
ref
262
ref
720
ref
absTerm
726
def
appTerm
727
def
absTerm
728
def
appTerm
729
def
axiom
nil
52
ref
729
remove
nil
cons
730
def
cons
731
def
53
ref
114
ref
724
ref
appTerm
nil
cons
732
def
cons
nil
cons
cons
nil
cons
cons
733
def
108
ref
subst
proveHyp
733
ref
69
ref
subst
733
remove
124
ref
subst
nil
115
ref
724
remove
nil
cons
cons
734
def
nil
cons
nil
cons
cons
171
ref
subst
262
ref
nil
9
ref
723
remove
nil
cons
735
def
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
115
ref
721
remove
nil
cons
cons
736
def
nil
cons
nil
cons
cons
171
ref
subst
119
ref
nil
9
ref
720
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
726
ref
264
remove
appTerm
737
def
betaConv
728
ref
120
ref
appTerm
738
def
betaConv
nil
731
remove
53
ref
738
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
187
ref
115
ref
728
remove
nil
cons
cons
284
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
727
remove
nil
cons
cons
53
ref
737
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
726
remove
nil
cons
cons
285
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
85
ref
730
remove
cons
87
ref
732
ref
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
nil
52
ref
732
remove
cons
53
ref
725
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
734
remove
285
remove
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
735
remove
cons
53
ref
722
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
736
remove
284
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
739
def
subst
eqMp
nil
52
ref
719
remove
cons
53
ref
644
ref
715
ref
appTerm
592
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
nil
679
ref
591
ref
nil
cons
cons
740
def
327
ref
715
ref
nil
cons
cons
nil
cons
741
def
cons
nil
cons
cons
390
ref
119
ref
19
ref
469
remove
528
remove
127
ref
appTerm
appTerm
appTerm
265
ref
appTerm
absTerm
742
def
120
ref
appTerm
743
def
betaConv
126
ref
114
ref
742
ref
appTerm
744
def
absTerm
745
def
127
ref
appTerm
746
def
betaConv
nil
278
ref
745
ref
appTerm
747
def
axiom
nil
52
ref
747
remove
nil
cons
cons
53
ref
746
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
280
ref
281
ref
745
remove
nil
cons
cons
282
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
744
remove
nil
cons
cons
53
ref
743
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
742
remove
nil
cons
cons
284
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
748
def
subst
591
ref
715
ref
appTerm
betaConv
trans
sym
488
ref
58
ref
227
ref
715
remove
appTerm
590
ref
appTerm
appTerm
556
ref
appTerm
absTerm
749
def
419
ref
appTerm
betaConv
sym
254
ref
nil
741
ref
nil
cons
cons
390
ref
552
ref
subst
750
def
subst
appThm
nil
9
ref
693
ref
cons
nil
cons
nil
cons
cons
23
ref
subst
691
remove
assume
eqMp
appThm
nil
9
ref
21
ref
nil
cons
cons
nil
cons
nil
cons
cons
751
def
9
ref
19
ref
58
ref
21
ref
appTerm
20
ref
appTerm
appTerm
20
ref
appTerm
absTerm
752
def
20
ref
appTerm
753
def
betaConv
nil
50
ref
752
ref
appTerm
754
def
axiom
nil
52
ref
754
remove
nil
cons
cons
53
ref
753
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
109
ref
110
ref
752
remove
nil
cons
cons
112
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
755
def
subst
trans
sym
22
ref
eqMp
eqMp
325
ref
326
ref
749
remove
nil
cons
cons
327
ref
718
remove
cons
nil
cons
cons
nil
cons
cons
443
remove
sym
nil
110
ref
87
ref
5
ref
422
remove
appTerm
92
remove
appTerm
756
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
626
ref
171
ref
subst
subst
87
ref
nil
9
ref
756
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
435
ref
69
ref
subst
435
remove
124
ref
subst
nil
52
ref
122
remove
cons
433
remove
cons
nil
cons
cons
108
ref
subst
421
ref
120
ref
appTerm
757
def
betaConv
nil
424
remove
53
ref
757
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
187
ref
115
ref
421
remove
nil
cons
cons
284
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
447
remove
446
remove
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
758
def
subst
proveHyp
eqMp
eqMp
eqMp
325
ref
326
ref
714
remove
nil
cons
cons
741
remove
cons
nil
cons
cons
758
ref
subst
proveHyp
eqMp
eqMp
nil
85
ref
693
remove
cons
87
ref
695
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
52
ref
114
ref
640
ref
appTerm
nil
cons
cons
53
ref
641
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
640
remove
nil
cons
cons
284
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
639
remove
nil
cons
cons
53
ref
5
ref
636
remove
appTerm
759
def
635
ref
appTerm
760
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
119
ref
760
remove
absTerm
761
def
120
ref
appTerm
762
def
betaConv
89
ref
452
ref
119
ref
759
remove
refl
119
ref
635
remove
absTerm
763
def
120
ref
appTerm
betaConv
appThm
absThm
appThm
appThm
643
ref
327
ref
5
ref
645
remove
592
remove
appTerm
appTerm
refl
763
ref
162
ref
419
ref
appTerm
764
def
appTerm
betaConv
appThm
absThm
appThm
appThm
nil
126
ref
763
remove
nil
cons
cons
593
remove
597
remove
cons
cons
nil
cons
cons
674
ref
subst
eqMp
643
ref
327
ref
6
ref
nil
740
remove
nil
cons
nil
cons
cons
748
remove
subst
591
remove
419
ref
appTerm
betaConv
trans
appThm
468
ref
764
remove
appTerm
558
ref
appTerm
765
def
refl
appThm
absThm
appThm
trans
sym
nil
326
ref
327
ref
5
ref
369
ref
488
ref
58
ref
227
ref
419
ref
appTerm
590
ref
appTerm
766
def
appTerm
556
ref
appTerm
767
def
absTerm
768
def
appTerm
appTerm
765
ref
appTerm
769
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
391
ref
subst
327
ref
nil
9
ref
769
remove
nil
cons
770
def
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
326
ref
488
ref
5
ref
768
ref
490
ref
appTerm
771
def
appTerm
765
ref
appTerm
772
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
391
ref
subst
488
ref
nil
9
ref
772
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
52
ref
771
ref
nil
cons
773
def
cons
53
ref
765
ref
nil
cons
774
def
cons
nil
cons
775
def
cons
nil
cons
cons
776
def
69
ref
subst
776
remove
124
ref
subst
771
ref
betaConv
771
remove
assume
eqMp
nil
52
ref
767
remove
nil
cons
777
def
cons
775
remove
cons
nil
cons
cons
778
def
108
ref
subst
proveHyp
778
ref
69
ref
subst
778
remove
124
ref
subst
nil
85
ref
766
ref
nil
cons
cons
87
ref
556
ref
nil
cons
779
def
cons
nil
cons
cons
nil
cons
cons
780
def
101
ref
subst
780
remove
211
ref
subst
19
ref
"_16168"
30
ref
var
781
def
468
ref
162
ref
781
remove
varTerm
appTerm
appTerm
558
ref
appTerm
absTerm
782
def
419
ref
appTerm
783
def
appTerm
refl
782
ref
590
ref
appTerm
betaConv
appThm
89
ref
783
remove
betaConv
appThm
468
remove
162
ref
590
ref
appTerm
784
def
appTerm
558
remove
appTerm
refl
appThm
trans
782
remove
refl
766
remove
assume
appThm
eqMp
sym
nil
648
remove
649
remove
262
ref
784
ref
nil
cons
785
def
cons
nil
cons
cons
cons
nil
cons
cons
710
ref
subst
sym
327
ref
58
ref
28
ref
784
ref
appTerm
786
def
647
remove
appTerm
appTerm
646
remove
appTerm
absTerm
787
def
490
ref
appTerm
betaConv
sym
58
ref
786
remove
146
ref
490
ref
appTerm
788
def
appTerm
789
def
appTerm
refl
89
ref
644
remove
490
ref
appTerm
refl
678
remove
appThm
appThm
677
remove
appThm
nil
680
remove
327
ref
509
ref
cons
nil
cons
790
def
cons
nil
cons
cons
688
ref
subst
eqMp
nil
9
ref
779
ref
cons
nil
cons
nil
cons
cons
23
ref
subst
556
ref
assume
eqMp
791
def
trans
appThm
nil
9
ref
789
remove
nil
cons
792
def
cons
nil
cons
nil
cons
cons
9
ref
19
ref
520
remove
21
ref
appTerm
appTerm
20
ref
appTerm
absTerm
793
def
20
ref
appTerm
794
def
betaConv
nil
50
ref
793
ref
appTerm
795
def
axiom
nil
52
ref
795
remove
nil
cons
cons
53
ref
794
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
109
ref
110
ref
793
remove
nil
cons
cons
112
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
trans
sym
nil
52
ref
779
ref
cons
796
def
53
ref
792
ref
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
nil
316
ref
509
remove
cons
797
def
nil
cons
nil
cons
cons
417
ref
subst
eqMp
798
def
eqMp
eqMp
325
ref
326
ref
787
remove
nil
cons
cons
790
ref
cons
nil
cons
cons
758
remove
subst
proveHyp
eqMp
eqMp
proveHyp
proveHyp
eqMp
nil
85
ref
777
remove
cons
87
ref
774
remove
cons
nil
cons
799
def
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
85
ref
773
remove
cons
799
ref
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
52
ref
322
ref
711
remove
5
ref
768
ref
713
remove
appTerm
appTerm
765
remove
appTerm
absTerm
appTerm
nil
cons
cons
53
ref
770
remove
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
768
remove
nil
cons
cons
799
remove
cons
nil
cons
cons
448
remove
subst
eqMp
eqMp
absThm
eqMp
eqMp
nil
52
ref
114
ref
761
ref
appTerm
nil
cons
cons
53
ref
762
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
761
remove
nil
cons
cons
284
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
appThm
eqMp
eqMp
nil
85
ref
569
remove
cons
87
ref
570
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
52
ref
58
ref
554
remove
appTerm
568
remove
appTerm
nil
cons
cons
53
ref
140
ref
496
ref
appTerm
800
def
nil
cons
801
def
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
6
ref
254
ref
496
ref
16
ref
appTerm
betaConv
appThm
452
ref
138
ref
453
ref
141
ref
6
ref
496
ref
142
ref
appTerm
betaConv
appThm
496
ref
159
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
453
ref
304
ref
498
remove
absThm
appThm
appThm
nil
454
ref
496
remove
nil
cons
802
def
cons
nil
cons
nil
cons
cons
459
ref
subst
eqMp
eqMp
803
def
nil
52
ref
801
remove
cons
53
ref
497
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
802
remove
cons
315
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
appThm
804
def
appThm
265
ref
refl
805
def
appThm
absThm
appThm
nil
589
remove
495
remove
nil
cons
cons
806
def
529
remove
449
ref
nil
cons
cons
807
def
nil
cons
cons
nil
cons
cons
808
def
674
remove
subst
643
ref
327
ref
6
ref
89
ref
675
remove
504
remove
487
remove
505
ref
488
ref
506
remove
488
ref
494
ref
absTerm
809
def
490
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
809
ref
419
ref
appTerm
betaConv
appThm
nil
679
ref
809
remove
nil
cons
cons
nil
cons
nil
cons
cons
688
remove
subst
eqMp
810
def
appThm
127
ref
449
ref
419
remove
appTerm
811
def
appTerm
812
def
refl
813
def
appThm
absThm
appThm
trans
trans
trans
appThm
322
ref
488
ref
5
ref
494
ref
appTerm
814
def
127
ref
449
remove
490
ref
appTerm
815
def
appTerm
816
def
appTerm
absTerm
appTerm
817
def
refl
appThm
nil
111
ref
322
ref
327
ref
5
ref
690
remove
380
ref
appTerm
818
def
appTerm
812
ref
appTerm
absTerm
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
626
remove
552
ref
subst
819
def
subst
trans
absThm
appThm
751
ref
175
remove
9
ref
19
ref
114
ref
524
remove
appTerm
appTerm
20
ref
appTerm
absTerm
820
def
20
ref
appTerm
821
def
betaConv
nil
50
ref
820
ref
appTerm
822
def
axiom
nil
52
ref
822
remove
nil
cons
cons
53
ref
821
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
109
ref
110
ref
820
remove
nil
cons
cons
112
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
823
def
subst
subst
824
def
trans
absThm
appThm
751
ref
280
ref
174
ref
cons
823
ref
subst
subst
825
def
trans
sym
22
ref
eqMp
nil
278
ref
126
ref
140
ref
304
ref
462
remove
817
remove
appTerm
absTerm
appTerm
absTerm
appTerm
thm
460
remove
126
ref
453
ref
304
ref
89
ref
304
ref
19
ref
"Data.List.any"
const
461
remove
constTerm
127
ref
appTerm
306
ref
appTerm
appTerm
826
def
425
ref
119
ref
58
ref
473
ref
appTerm
265
remove
appTerm
absTerm
appTerm
appTerm
absTerm
827
def
306
ref
appTerm
828
def
betaConv
126
ref
140
ref
827
ref
appTerm
829
def
absTerm
830
def
127
remove
appTerm
831
def
betaConv
nil
278
ref
830
ref
appTerm
832
def
axiom
nil
52
ref
832
remove
nil
cons
cons
53
ref
831
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
280
remove
281
remove
830
remove
nil
cons
cons
282
remove
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
829
remove
nil
cons
cons
53
ref
828
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
827
remove
nil
cons
cons
315
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
425
ref
refl
119
ref
254
ref
804
ref
appThm
805
remove
appThm
absThm
appThm
808
remove
530
remove
598
remove
19
ref
368
remove
651
remove
constTerm
653
ref
58
ref
655
remove
appTerm
658
remove
appTerm
absTerm
appTerm
appTerm
425
remove
119
ref
58
ref
618
remove
appTerm
659
remove
appTerm
absTerm
appTerm
appTerm
absTerm
833
def
599
remove
appTerm
834
def
betaConv
534
ref
604
remove
833
ref
appTerm
835
def
absTerm
836
def
539
ref
appTerm
837
def
betaConv
656
remove
544
ref
836
ref
appTerm
838
def
absTerm
839
def
657
remove
appTerm
840
def
betaConv
nil
668
remove
839
ref
appTerm
841
def
axiom
nil
52
ref
841
remove
nil
cons
cons
53
ref
840
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
671
remove
672
remove
839
remove
nil
cons
cons
673
remove
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
838
remove
nil
cons
cons
53
ref
837
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
546
ref
547
ref
836
remove
nil
cons
cons
548
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
835
remove
nil
cons
cons
53
ref
834
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
550
remove
612
remove
833
remove
nil
cons
cons
613
remove
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
subst
505
ref
327
ref
254
ref
810
ref
appThm
813
remove
appThm
absThm
appThm
trans
trans
trans
appThm
369
ref
488
ref
58
ref
494
ref
appTerm
842
def
816
remove
appTerm
absTerm
appTerm
843
def
refl
appThm
nil
111
ref
369
ref
327
ref
58
ref
818
remove
appTerm
812
remove
appTerm
absTerm
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
819
remove
subst
trans
absThm
appThm
824
remove
trans
absThm
appThm
825
remove
trans
sym
22
ref
eqMp
nil
278
remove
126
remove
140
ref
304
ref
826
remove
843
remove
appTerm
absTerm
appTerm
absTerm
appTerm
thm
nil
172
ref
304
ref
114
ref
119
ref
19
ref
"Data.List.member"
const
0
ref
11
ref
308
remove
cons
opType
constTerm
120
ref
appTerm
306
ref
appTerm
appTerm
844
def
369
remove
488
ref
842
remove
551
ref
815
ref
appTerm
845
def
appTerm
absTerm
appTerm
appTerm
846
def
absTerm
847
def
appTerm
848
def
absTerm
849
def
nil
cons
cons
nil
cons
nil
cons
cons
176
ref
subst
304
ref
nil
9
ref
848
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
115
ref
847
remove
nil
cons
cons
nil
cons
nil
cons
cons
171
ref
subst
119
ref
nil
9
ref
846
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
844
ref
refl
505
ref
488
ref
nil
"t2"
1
ref
var
850
def
845
remove
nil
cons
cons
"t1"
1
ref
var
851
def
494
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
850
ref
19
ref
58
ref
851
ref
varTerm
852
def
appTerm
850
remove
varTerm
853
def
appTerm
appTerm
58
ref
853
ref
appTerm
852
ref
appTerm
appTerm
absTerm
854
def
853
ref
appTerm
855
def
betaConv
851
remove
50
ref
854
ref
appTerm
856
def
absTerm
857
def
852
ref
appTerm
858
def
betaConv
nil
50
ref
857
ref
appTerm
859
def
axiom
nil
52
ref
859
remove
nil
cons
cons
53
ref
858
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
109
ref
110
ref
857
remove
nil
cons
cons
111
ref
852
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
856
remove
nil
cons
cons
53
ref
855
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
109
ref
110
ref
854
remove
nil
cons
cons
111
remove
853
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
absThm
appThm
appThm
sym
119
ref
844
remove
473
remove
appTerm
absTerm
860
def
120
ref
appTerm
861
def
betaConv
304
ref
114
ref
860
ref
appTerm
862
def
absTerm
863
def
306
ref
appTerm
864
def
betaConv
nil
140
ref
863
ref
appTerm
865
def
axiom
nil
52
ref
865
remove
nil
cons
cons
53
ref
864
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
863
remove
nil
cons
cons
315
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
862
remove
nil
cons
cons
53
ref
861
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
860
remove
nil
cons
cons
284
remove
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
804
remove
nil
806
remove
807
remove
262
ref
283
remove
cons
nil
cons
cons
cons
nil
cons
cons
710
remove
subst
505
remove
327
ref
58
ref
551
remove
811
remove
appTerm
appTerm
refl
810
remove
appThm
absThm
appThm
trans
trans
trans
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
140
ref
849
remove
appTerm
thm
803
remove
nil
800
remove
thm
nil
547
ref
534
ref
140
ref
304
ref
322
ref
488
ref
814
remove
698
ref
29
remove
0
ref
10
remove
532
ref
opType
866
def
0
ref
30
ref
532
remove
cons
opType
nil
cons
cons
opType
constTerm
867
def
"Data.List.map"
const
0
ref
533
remove
0
ref
13
ref
866
ref
nil
cons
868
def
cons
opType
nil
cons
cons
opType
constTerm
539
ref
appTerm
869
def
306
ref
appTerm
870
def
appTerm
490
ref
appTerm
appTerm
539
ref
815
remove
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
871
def
appTerm
872
def
absTerm
873
def
nil
cons
cons
nil
cons
nil
cons
cons
546
ref
174
ref
cons
171
ref
subst
subst
534
ref
nil
9
ref
872
remove
nil
cons
874
def
cons
nil
cons
nil
cons
cons
23
ref
subst
643
ref
488
ref
6
ref
519
remove
appThm
698
ref
867
ref
869
ref
16
ref
appTerm
appTerm
490
ref
appTerm
appTerm
539
ref
33
ref
490
ref
appTerm
875
def
appTerm
appTerm
876
def
refl
appThm
nil
9
ref
876
ref
nil
cons
cons
nil
cons
nil
cons
cons
136
ref
subst
trans
absThm
appThm
751
remove
390
ref
823
remove
subst
subst
trans
sym
22
ref
eqMp
nil
52
ref
322
ref
488
ref
5
ref
553
remove
appTerm
877
def
876
remove
appTerm
absTerm
appTerm
878
def
nil
cons
cons
53
ref
114
ref
138
ref
140
ref
141
ref
5
ref
322
ref
488
ref
5
ref
556
remove
appTerm
879
def
698
ref
867
ref
869
ref
142
ref
appTerm
880
def
appTerm
490
ref
appTerm
881
def
appTerm
539
ref
788
ref
appTerm
882
def
appTerm
883
def
appTerm
884
def
absTerm
885
def
appTerm
886
def
appTerm
322
ref
488
ref
5
ref
562
remove
appTerm
698
ref
867
ref
869
remove
159
ref
appTerm
887
def
appTerm
490
ref
appTerm
appTerm
539
ref
162
ref
490
ref
appTerm
888
def
appTerm
889
def
appTerm
appTerm
absTerm
appTerm
890
def
appTerm
891
def
absTerm
892
def
appTerm
893
def
absTerm
894
def
appTerm
895
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
nil
115
ref
894
remove
nil
cons
cons
nil
cons
nil
cons
cons
171
ref
subst
138
ref
nil
9
ref
893
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
172
ref
892
remove
nil
cons
cons
nil
cons
nil
cons
cons
176
ref
subst
141
ref
nil
9
ref
891
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
52
ref
886
remove
nil
cons
896
def
cons
897
def
53
ref
890
remove
nil
cons
898
def
cons
nil
cons
cons
nil
cons
cons
899
def
69
ref
subst
899
remove
124
ref
subst
643
ref
488
ref
6
ref
582
remove
appThm
698
ref
refl
900
def
867
ref
refl
141
ref
18
remove
0
ref
866
ref
0
ref
866
ref
2
ref
cons
opType
nil
cons
cons
opType
constTerm
887
remove
appTerm
153
remove
0
ref
531
ref
0
ref
866
ref
868
remove
cons
opType
nil
cons
cons
opType
constTerm
539
ref
157
ref
appTerm
901
def
appTerm
880
ref
appTerm
902
def
appTerm
absTerm
903
def
142
ref
appTerm
904
def
betaConv
138
ref
140
ref
903
ref
appTerm
905
def
absTerm
906
def
157
ref
appTerm
907
def
betaConv
534
ref
114
ref
906
ref
appTerm
908
def
absTerm
909
def
539
ref
appTerm
910
def
betaConv
nil
544
ref
909
ref
appTerm
911
def
axiom
nil
52
ref
911
remove
nil
cons
cons
53
ref
910
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
546
ref
547
ref
909
remove
nil
cons
cons
548
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
908
remove
nil
cons
cons
53
ref
907
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
906
remove
nil
cons
cons
189
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
905
remove
nil
cons
cons
53
ref
904
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
903
remove
nil
cons
cons
192
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
appThm
490
ref
refl
appThm
appThm
889
ref
refl
appThm
appThm
absThm
appThm
sym
5
ref
397
ref
41
ref
appTerm
912
def
229
ref
appTerm
913
def
appTerm
914
def
refl
900
remove
nil
"t"
866
ref
var
880
ref
nil
cons
cons
"h"
531
ref
var
901
remove
nil
cons
915
def
cons
nil
cons
cons
916
def
nil
cons
cons
708
remove
174
ref
cons
917
def
339
ref
subst
subst
appThm
539
ref
refl
918
def
339
ref
appThm
appThm
nil
709
remove
915
remove
cons
nil
cons
nil
cons
cons
917
ref
552
ref
subst
subst
trans
appThm
nil
9
ref
913
remove
nil
cons
cons
nil
cons
nil
cons
cons
9
ref
19
ref
5
ref
20
ref
appTerm
919
def
21
ref
appTerm
appTerm
21
ref
appTerm
absTerm
920
def
20
ref
appTerm
921
def
betaConv
nil
50
ref
920
ref
appTerm
922
def
axiom
nil
52
ref
922
remove
nil
cons
cons
53
ref
921
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
109
ref
110
ref
920
remove
nil
cons
cons
112
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
923
def
subst
trans
sym
22
ref
eqMp
nil
52
ref
914
remove
698
ref
867
remove
902
remove
appTerm
924
def
41
ref
appTerm
appTerm
539
ref
332
ref
appTerm
appTerm
appTerm
925
def
nil
cons
cons
53
ref
322
ref
488
ref
5
ref
5
ref
493
ref
229
ref
appTerm
appTerm
698
ref
924
ref
490
ref
appTerm
appTerm
889
remove
appTerm
appTerm
926
def
appTerm
5
ref
397
ref
590
ref
appTerm
927
def
229
ref
appTerm
appTerm
698
ref
924
remove
590
ref
appTerm
928
def
appTerm
929
def
539
ref
784
ref
appTerm
930
def
appTerm
931
def
appTerm
932
def
appTerm
933
def
absTerm
934
def
appTerm
935
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
nil
326
ref
934
remove
nil
cons
cons
nil
cons
nil
cons
cons
391
ref
subst
488
ref
nil
9
ref
933
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
52
ref
926
ref
nil
cons
936
def
cons
53
ref
932
remove
nil
cons
937
def
cons
nil
cons
cons
nil
cons
cons
938
def
69
ref
subst
938
remove
124
ref
subst
6
ref
nil
353
ref
510
ref
cons
nil
cons
cons
316
ref
19
ref
397
ref
584
ref
appTerm
318
ref
appTerm
appTerm
585
ref
appTerm
absTerm
939
def
317
ref
appTerm
940
def
betaConv
364
ref
322
ref
939
ref
appTerm
941
def
absTerm
942
def
366
ref
appTerm
943
def
betaConv
nil
322
ref
942
ref
appTerm
944
def
axiom
nil
52
ref
944
remove
nil
cons
cons
53
ref
943
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
942
remove
nil
cons
cons
517
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
941
remove
nil
cons
cons
53
ref
940
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
939
remove
nil
cons
cons
328
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
945
def
subst
appThm
931
ref
refl
946
def
appThm
sym
nil
796
ref
53
ref
931
ref
nil
cons
947
def
cons
nil
cons
948
def
cons
nil
cons
cons
949
def
69
ref
subst
949
remove
124
ref
subst
885
ref
490
ref
appTerm
950
def
betaConv
nil
897
remove
53
ref
950
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
325
ref
326
ref
885
remove
nil
cons
cons
790
remove
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
884
remove
nil
cons
cons
948
remove
cons
nil
cons
cons
108
ref
subst
proveHyp
6
ref
6
ref
791
ref
appThm
883
ref
refl
appThm
nil
9
ref
883
ref
nil
cons
cons
nil
cons
nil
cons
cons
251
ref
subst
trans
appThm
946
remove
appThm
sym
507
ref
305
remove
304
ref
227
ref
38
remove
0
ref
866
remove
34
remove
cons
opType
constTerm
951
def
870
remove
appTerm
appTerm
380
remove
appTerm
absTerm
952
def
306
ref
appTerm
953
def
betaConv
534
remove
140
ref
952
ref
appTerm
954
def
absTerm
955
def
539
remove
appTerm
956
def
betaConv
nil
544
ref
955
ref
appTerm
957
def
axiom
nil
52
ref
957
remove
nil
cons
cons
53
ref
956
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
546
remove
547
remove
955
remove
nil
cons
cons
548
remove
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
954
remove
nil
cons
cons
53
ref
953
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
952
remove
nil
cons
cons
315
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
appThm
791
ref
trans
sym
22
ref
eqMp
nil
52
ref
493
ref
951
remove
880
remove
appTerm
appTerm
nil
cons
cons
53
ref
929
remove
881
ref
appTerm
958
def
nil
cons
959
def
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
797
ref
916
remove
cons
nil
cons
cons
917
ref
417
ref
subst
subst
eqMp
nil
52
ref
959
remove
cons
53
ref
698
remove
930
ref
appTerm
882
ref
appTerm
960
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
918
remove
798
ref
appThm
eqMp
nil
52
ref
58
ref
958
remove
appTerm
960
remove
appTerm
nil
cons
cons
53
ref
5
ref
883
remove
appTerm
931
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
"d"
531
ref
var
930
remove
nil
cons
cons
"c"
531
ref
var
928
remove
nil
cons
cons
"b"
531
ref
var
882
remove
nil
cons
cons
"a"
531
remove
var
881
remove
nil
cons
cons
nil
cons
cons
cons
cons
nil
cons
cons
917
remove
nil
52
ref
58
ref
28
ref
"c"
11
ref
var
961
def
varTerm
appTerm
962
def
"a"
11
ref
var
963
def
varTerm
964
def
appTerm
965
def
appTerm
28
ref
"d"
11
ref
var
966
def
varTerm
967
def
appTerm
"b"
11
ref
var
968
def
varTerm
969
def
appTerm
970
def
appTerm
nil
cons
971
def
cons
53
ref
5
ref
28
ref
964
remove
appTerm
969
remove
appTerm
972
def
appTerm
973
def
962
remove
967
remove
appTerm
appTerm
nil
cons
974
def
cons
nil
cons
cons
nil
cons
cons
975
def
69
ref
subst
975
remove
124
ref
subst
nil
85
ref
965
ref
nil
cons
cons
87
ref
970
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
976
def
101
ref
subst
976
remove
211
ref
subst
973
remove
refl
221
ref
965
remove
assume
appThm
970
remove
assume
appThm
appThm
nil
9
ref
972
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
9
ref
919
remove
20
ref
appTerm
977
def
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
9
ref
977
remove
absTerm
978
def
20
ref
appTerm
979
def
betaConv
nil
50
ref
978
ref
appTerm
980
def
axiom
nil
52
ref
980
remove
nil
cons
cons
53
ref
979
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
109
ref
110
ref
978
remove
nil
cons
cons
112
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
eqMp
981
def
subst
trans
sym
22
ref
eqMp
proveHyp
proveHyp
eqMp
nil
85
ref
971
remove
cons
87
ref
974
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
982
def
subst
subst
eqMp
eqMp
eqMp
eqMp
nil
85
ref
779
remove
cons
983
def
87
ref
947
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
85
ref
936
remove
cons
87
ref
937
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
52
ref
58
ref
925
remove
appTerm
935
remove
appTerm
nil
cons
cons
53
ref
322
ref
488
ref
926
remove
absTerm
984
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
6
ref
254
ref
984
ref
41
ref
appTerm
betaConv
appThm
643
ref
488
ref
6
ref
984
ref
490
ref
appTerm
betaConv
985
def
appThm
984
ref
590
ref
appTerm
betaConv
appThm
absThm
appThm
appThm
appThm
643
ref
488
ref
985
remove
absThm
appThm
appThm
nil
679
ref
984
remove
nil
cons
cons
nil
cons
nil
cons
cons
679
ref
5
ref
58
ref
679
ref
varTerm
986
def
41
ref
appTerm
appTerm
322
ref
316
ref
5
ref
986
ref
317
ref
appTerm
987
def
appTerm
986
ref
318
ref
appTerm
appTerm
absTerm
appTerm
appTerm
appTerm
322
ref
316
ref
987
remove
absTerm
appTerm
appTerm
absTerm
988
def
986
ref
appTerm
989
def
betaConv
nil
48
ref
0
ref
321
ref
2
ref
cons
opType
constTerm
988
ref
appTerm
990
def
axiom
nil
52
ref
990
remove
nil
cons
cons
53
ref
989
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
"A"
225
remove
cons
nil
cons
"P"
321
remove
var
988
remove
nil
cons
cons
"x"
224
remove
var
986
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
991
def
subst
eqMp
eqMp
eqMp
eqMp
nil
85
ref
896
remove
cons
87
ref
898
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
52
ref
58
ref
878
remove
appTerm
895
remove
appTerm
nil
cons
cons
53
ref
874
remove
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
6
ref
254
ref
871
ref
16
ref
appTerm
betaConv
appThm
452
ref
138
ref
453
ref
141
ref
6
ref
871
ref
142
ref
appTerm
betaConv
appThm
871
ref
159
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
453
ref
304
ref
871
ref
306
ref
appTerm
betaConv
absThm
appThm
appThm
nil
454
ref
871
remove
nil
cons
cons
nil
cons
nil
cons
cons
459
ref
subst
eqMp
eqMp
eqMp
absThm
eqMp
nil
544
remove
873
remove
appTerm
thm
89
ref
453
ref
"l1"
13
ref
var
992
def
453
ref
"l2"
13
ref
var
993
def
992
ref
993
ref
5
ref
58
ref
227
ref
39
ref
992
ref
varTerm
994
def
appTerm
995
def
appTerm
996
def
39
ref
993
ref
varTerm
997
def
appTerm
998
def
appTerm
appTerm
322
ref
488
ref
5
ref
493
ref
995
ref
appTerm
appTerm
999
def
28
ref
32
ref
994
ref
appTerm
1000
def
490
ref
appTerm
appTerm
1001
def
32
ref
997
ref
appTerm
1002
def
490
ref
appTerm
appTerm
appTerm
absTerm
appTerm
appTerm
appTerm
310
ref
994
ref
appTerm
1003
def
997
ref
appTerm
appTerm
1004
def
absTerm
1005
def
absTerm
1006
def
994
ref
appTerm
betaConv
997
ref
refl
appThm
1005
ref
997
ref
appTerm
betaConv
trans
1007
def
absThm
appThm
absThm
appThm
appThm
453
ref
993
ref
453
ref
992
ref
1007
remove
absThm
appThm
absThm
appThm
appThm
nil
"p"
309
remove
var
1006
remove
nil
cons
cons
nil
cons
nil
cons
cons
"B"
154
remove
cons
173
ref
cons
174
remove
cons
"p"
0
ref
11
ref
670
remove
cons
opType
1008
def
var
1009
def
19
ref
114
ref
119
ref
652
ref
653
ref
1009
remove
varTerm
1010
def
120
remove
appTerm
654
remove
appTerm
1011
def
absTerm
appTerm
absTerm
appTerm
appTerm
652
remove
653
remove
114
ref
119
ref
1011
remove
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
1012
def
1010
ref
appTerm
1013
def
betaConv
nil
48
remove
0
ref
0
ref
1008
ref
2
ref
cons
opType
1014
def
2
remove
cons
opType
constTerm
1012
ref
appTerm
1015
def
axiom
nil
52
ref
1015
remove
nil
cons
cons
53
ref
1013
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
"A"
1008
ref
nil
cons
cons
nil
cons
"P"
1014
remove
var
1012
remove
nil
cons
cons
"x"
1008
remove
var
1010
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
subst
eqMp
sym
453
ref
992
ref
6
ref
254
ref
996
ref
refl
331
ref
appThm
nil
304
ref
994
ref
nil
cons
1016
def
cons
nil
cons
nil
cons
cons
304
ref
381
remove
311
remove
appTerm
absTerm
1017
def
306
ref
appTerm
1018
def
betaConv
nil
140
ref
1017
ref
appTerm
1019
def
axiom
nil
52
ref
1019
remove
nil
cons
cons
53
ref
1018
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
1017
remove
nil
cons
cons
315
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
trans
appThm
322
ref
488
ref
999
ref
1001
ref
875
ref
appTerm
appTerm
absTerm
appTerm
1020
def
refl
appThm
appThm
1003
ref
16
ref
appTerm
1021
def
refl
appThm
absThm
appThm
sym
nil
172
ref
992
ref
5
ref
58
ref
1021
ref
appTerm
1020
ref
appTerm
1022
def
appTerm
1021
ref
appTerm
1023
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
176
ref
subst
992
ref
nil
9
ref
1023
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
52
ref
1022
remove
nil
cons
1024
def
cons
53
ref
1021
ref
nil
cons
1025
def
cons
nil
cons
cons
nil
cons
cons
1026
def
69
ref
subst
1026
remove
124
ref
subst
nil
85
ref
1025
ref
cons
87
ref
1020
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
eqMp
nil
85
ref
1024
remove
cons
87
ref
1025
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
52
ref
140
ref
992
ref
5
ref
58
ref
996
ref
40
ref
appTerm
appTerm
1020
remove
appTerm
appTerm
1021
remove
appTerm
absTerm
appTerm
1027
def
nil
cons
cons
53
ref
114
ref
138
ref
140
ref
141
ref
5
ref
140
ref
992
ref
5
ref
58
ref
996
ref
147
ref
appTerm
appTerm
322
ref
488
ref
999
ref
1001
ref
788
ref
appTerm
appTerm
absTerm
appTerm
appTerm
appTerm
1003
ref
142
ref
appTerm
appTerm
absTerm
1028
def
appTerm
1029
def
appTerm
140
ref
992
ref
5
ref
58
ref
996
remove
163
ref
appTerm
appTerm
322
ref
488
ref
999
remove
1001
remove
888
ref
appTerm
appTerm
absTerm
appTerm
appTerm
appTerm
1003
remove
159
ref
appTerm
appTerm
absTerm
1030
def
appTerm
1031
def
appTerm
1032
def
absTerm
1033
def
appTerm
1034
def
absTerm
1035
def
appTerm
1036
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
nil
115
ref
1035
remove
nil
cons
cons
nil
cons
nil
cons
cons
171
ref
subst
138
ref
nil
9
ref
1034
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
172
ref
1033
remove
nil
cons
cons
nil
cons
nil
cons
cons
176
ref
subst
141
ref
nil
9
ref
1032
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
52
ref
1029
remove
nil
cons
1037
def
cons
1038
def
53
ref
1031
remove
nil
cons
1039
def
cons
nil
cons
1040
def
cons
nil
cons
cons
1041
def
69
ref
subst
1041
remove
124
ref
subst
6
ref
254
ref
227
ref
refl
1042
def
331
ref
appThm
236
ref
appThm
355
ref
8
ref
227
ref
41
ref
appTerm
318
ref
appTerm
1043
def
assume
sym
227
ref
318
ref
appTerm
41
ref
appTerm
1044
def
assume
sym
deductAntisym
appThm
316
ref
7
ref
1044
remove
appTerm
absTerm
1045
def
317
ref
appTerm
1046
def
betaConv
nil
322
ref
1045
ref
appTerm
1047
def
axiom
nil
52
ref
1047
remove
nil
cons
cons
53
ref
1046
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
1045
remove
nil
cons
cons
328
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
eqMp
nil
52
ref
7
ref
1043
ref
appTerm
nil
cons
cons
53
ref
19
ref
1043
ref
appTerm
25
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
85
ref
1043
remove
nil
cons
cons
nil
cons
nil
cons
cons
218
ref
subst
eqMp
subst
trans
appThm
643
ref
488
ref
6
ref
508
remove
appThm
28
ref
875
remove
appTerm
888
ref
appTerm
1048
def
refl
appThm
absThm
appThm
appThm
nil
9
ref
322
ref
488
ref
5
ref
493
ref
41
ref
appTerm
appTerm
1048
ref
appTerm
absTerm
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
9
ref
19
ref
58
ref
25
ref
appTerm
20
ref
appTerm
appTerm
25
ref
appTerm
absTerm
1049
def
20
remove
appTerm
1050
def
betaConv
nil
50
remove
1049
ref
appTerm
1051
def
axiom
nil
52
ref
1051
remove
nil
cons
cons
53
ref
1050
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
109
remove
110
remove
1049
remove
nil
cons
cons
112
remove
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
trans
appThm
310
ref
16
ref
appTerm
159
ref
appTerm
1052
def
refl
appThm
nil
9
ref
1052
ref
nil
cons
cons
nil
cons
nil
cons
cons
136
remove
subst
trans
sym
22
ref
eqMp
nil
52
ref
5
ref
58
ref
330
remove
163
ref
appTerm
appTerm
322
ref
488
ref
877
remove
1048
remove
appTerm
absTerm
appTerm
appTerm
appTerm
1052
remove
appTerm
1053
def
nil
cons
cons
53
ref
114
ref
"h'"
11
ref
var
1054
def
140
ref
"t'"
13
ref
var
1055
def
5
ref
5
ref
58
ref
227
ref
39
ref
1055
ref
varTerm
1056
def
appTerm
1057
def
appTerm
1058
def
163
ref
appTerm
appTerm
322
ref
488
ref
5
ref
493
ref
1057
ref
appTerm
1059
def
appTerm
1060
def
28
ref
32
ref
1056
ref
appTerm
490
ref
appTerm
1061
def
appTerm
1062
def
888
ref
appTerm
appTerm
absTerm
appTerm
appTerm
appTerm
310
ref
1056
ref
appTerm
1063
def
159
ref
appTerm
appTerm
1064
def
appTerm
5
ref
58
ref
227
ref
39
ref
156
ref
1054
ref
varTerm
1065
def
appTerm
1056
ref
appTerm
1066
def
appTerm
1067
def
appTerm
163
ref
appTerm
appTerm
322
ref
488
ref
5
ref
493
ref
1067
remove
appTerm
appTerm
28
ref
32
ref
1066
ref
appTerm
1068
def
490
remove
appTerm
appTerm
888
remove
appTerm
1069
def
appTerm
absTerm
appTerm
appTerm
appTerm
310
ref
1066
ref
appTerm
159
ref
appTerm
appTerm
1070
def
appTerm
1071
def
absTerm
1072
def
appTerm
1073
def
absTerm
1074
def
appTerm
1075
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
nil
115
ref
1074
remove
nil
cons
cons
nil
cons
nil
cons
cons
171
ref
subst
1054
ref
nil
9
ref
1073
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
172
ref
1072
remove
nil
cons
cons
nil
cons
nil
cons
cons
176
ref
subst
1055
ref
nil
9
ref
1071
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
52
ref
1064
remove
nil
cons
1076
def
cons
53
ref
1070
remove
nil
cons
1077
def
cons
nil
cons
cons
nil
cons
cons
1078
def
69
ref
subst
1078
remove
124
ref
subst
6
ref
254
ref
1042
ref
nil
141
ref
1056
ref
nil
cons
1079
def
cons
138
ref
1065
ref
nil
cons
1080
def
cons
nil
cons
cons
1081
def
nil
cons
cons
1082
def
236
ref
subst
1083
def
appThm
236
ref
appThm
nil
353
ref
364
ref
1057
ref
nil
cons
1084
def
cons
nil
cons
cons
nil
cons
cons
316
ref
19
ref
227
ref
584
ref
appTerm
318
ref
appTerm
appTerm
367
remove
317
ref
appTerm
appTerm
absTerm
1085
def
317
ref
appTerm
1086
def
betaConv
364
ref
322
ref
1085
ref
appTerm
1087
def
absTerm
1088
def
366
ref
appTerm
1089
def
betaConv
nil
322
ref
1088
ref
appTerm
1090
def
axiom
nil
52
ref
1090
remove
nil
cons
cons
53
ref
1089
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
1088
remove
nil
cons
cons
517
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
1087
remove
nil
cons
cons
53
ref
1086
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
1085
remove
nil
cons
cons
328
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
trans
appThm
643
ref
488
ref
6
ref
507
ref
1083
remove
appThm
appThm
1069
ref
refl
appThm
absThm
appThm
appThm
appThm
nil
"t2"
13
ref
var
1091
def
191
ref
cons
"h2"
11
ref
var
1092
def
188
ref
cons
"t1"
13
ref
var
1093
def
1079
ref
cons
"h1"
11
ref
var
1094
def
1080
remove
cons
nil
cons
cons
cons
cons
nil
cons
cons
1091
ref
19
ref
310
ref
156
ref
1094
ref
varTerm
1095
def
appTerm
1093
ref
varTerm
1096
def
appTerm
appTerm
156
remove
1092
ref
varTerm
1097
def
appTerm
1091
remove
varTerm
1098
def
appTerm
appTerm
appTerm
58
ref
28
ref
1095
ref
appTerm
1097
ref
appTerm
appTerm
310
ref
1096
ref
appTerm
1098
ref
appTerm
appTerm
appTerm
absTerm
1099
def
1098
ref
appTerm
1100
def
betaConv
1093
remove
140
ref
1099
ref
appTerm
1101
def
absTerm
1102
def
1096
ref
appTerm
1103
def
betaConv
1092
remove
140
ref
1102
ref
appTerm
1104
def
absTerm
1105
def
1097
ref
appTerm
1106
def
betaConv
1094
remove
114
ref
1105
ref
appTerm
1107
def
absTerm
1108
def
1095
ref
appTerm
1109
def
betaConv
nil
114
ref
1108
ref
appTerm
1110
def
axiom
nil
52
ref
1110
remove
nil
cons
cons
53
ref
1109
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
1108
remove
nil
cons
cons
119
ref
1095
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
1107
remove
nil
cons
cons
53
ref
1106
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
1105
remove
nil
cons
cons
119
ref
1097
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
1104
remove
nil
cons
cons
53
ref
1103
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
1102
remove
nil
cons
cons
190
ref
1096
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
1101
remove
nil
cons
cons
53
ref
1100
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
1099
remove
nil
cons
cons
190
ref
1098
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
appThm
sym
nil
52
ref
58
ref
1058
remove
147
ref
appTerm
1111
def
appTerm
1112
def
322
ref
488
ref
5
ref
493
remove
228
ref
1057
remove
appTerm
1113
def
appTerm
appTerm
1069
remove
appTerm
absTerm
1114
def
appTerm
1115
def
appTerm
nil
cons
1116
def
cons
53
ref
58
ref
28
ref
1065
remove
appTerm
157
ref
appTerm
1117
def
appTerm
1063
remove
142
ref
appTerm
1118
def
appTerm
nil
cons
1119
def
cons
nil
cons
cons
nil
cons
cons
1120
def
69
ref
subst
1120
remove
124
ref
subst
nil
85
ref
1111
ref
nil
cons
cons
87
ref
1115
remove
nil
cons
1121
def
cons
nil
cons
cons
nil
cons
cons
1122
def
101
ref
subst
1122
remove
211
ref
subst
1114
ref
41
ref
appTerm
1123
def
betaConv
nil
52
ref
1121
remove
cons
1124
def
53
ref
1123
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
325
ref
326
ref
1114
ref
nil
cons
cons
1125
def
595
remove
nil
cons
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
5
ref
912
ref
1113
ref
appTerm
appTerm
28
ref
1068
ref
41
ref
appTerm
appTerm
332
ref
appTerm
appTerm
nil
cons
cons
53
ref
1117
ref
nil
cons
1126
def
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
6
ref
6
ref
nil
316
ref
1084
remove
cons
1127
def
nil
cons
nil
cons
cons
nil
9
ref
912
ref
318
ref
appTerm
1128
def
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
316
ref
1128
remove
absTerm
1129
def
317
ref
appTerm
1130
def
betaConv
nil
322
ref
1129
ref
appTerm
1131
def
axiom
nil
52
ref
1131
remove
nil
cons
cons
53
ref
1130
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
1129
remove
nil
cons
cons
328
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
eqMp
1132
def
subst
appThm
221
ref
1082
remove
339
ref
subst
appThm
339
ref
appThm
appThm
nil
9
ref
1126
ref
cons
nil
cons
nil
cons
cons
1133
def
251
ref
subst
trans
appThm
1117
remove
refl
appThm
1133
remove
981
remove
subst
trans
sym
22
ref
eqMp
eqMp
nil
52
ref
1126
remove
cons
53
ref
1118
remove
nil
cons
cons
nil
cons
1134
def
cons
nil
cons
cons
124
ref
subst
proveHyp
254
ref
1042
remove
1111
remove
assume
1135
def
appThm
147
ref
refl
appThm
nil
373
remove
nil
cons
cons
750
remove
subst
trans
appThm
643
ref
488
ref
6
ref
507
remove
1135
remove
appThm
1136
def
appThm
1062
ref
788
ref
appTerm
1137
def
refl
1138
def
appThm
absThm
appThm
appThm
nil
9
ref
322
ref
488
ref
879
remove
1137
ref
appTerm
1139
def
absTerm
1140
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
755
remove
subst
trans
sym
nil
326
ref
1140
remove
nil
cons
cons
nil
cons
nil
cons
cons
391
ref
subst
488
ref
nil
9
ref
1139
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
796
remove
53
ref
1137
ref
nil
cons
1141
def
cons
nil
cons
1142
def
cons
nil
cons
cons
1143
def
69
ref
subst
1143
remove
124
ref
subst
1114
remove
590
ref
appTerm
1144
def
betaConv
nil
1124
remove
53
ref
1144
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
325
ref
1125
remove
327
ref
590
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
5
ref
927
remove
1113
remove
appTerm
appTerm
28
ref
1068
remove
590
remove
appTerm
1145
def
appTerm
1146
def
784
ref
appTerm
1147
def
appTerm
nil
cons
cons
1142
remove
cons
nil
cons
cons
108
ref
subst
proveHyp
6
ref
6
ref
nil
1127
remove
510
remove
cons
nil
cons
cons
945
ref
subst
1136
remove
791
remove
trans
1148
def
trans
appThm
1147
ref
refl
appThm
nil
9
ref
1147
ref
nil
cons
cons
nil
cons
nil
cons
cons
251
remove
subst
trans
appThm
1138
remove
appThm
sym
1148
remove
sym
22
ref
eqMp
nil
52
ref
1059
remove
nil
cons
cons
53
ref
1146
remove
1061
ref
appTerm
nil
cons
1149
def
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
797
remove
1081
remove
cons
nil
cons
cons
417
ref
subst
eqMp
nil
52
ref
1149
remove
cons
53
ref
1062
remove
1145
ref
appTerm
1150
def
nil
cons
1151
def
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
119
ref
1145
remove
nil
cons
1152
def
cons
262
ref
1061
remove
nil
cons
1153
def
cons
nil
cons
cons
nil
cons
cons
739
ref
subst
eqMp
nil
52
ref
1151
remove
cons
53
ref
28
ref
788
ref
appTerm
784
remove
appTerm
1154
def
nil
cons
cons
nil
cons
1155
def
cons
nil
cons
cons
124
ref
subst
proveHyp
798
remove
nil
52
ref
792
remove
cons
1155
remove
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
119
ref
785
ref
cons
262
ref
788
remove
nil
cons
1156
def
cons
nil
cons
cons
nil
cons
cons
739
ref
subst
eqMp
eqMp
nil
52
ref
58
ref
1150
remove
appTerm
1154
remove
appTerm
nil
cons
cons
53
ref
5
ref
1147
remove
appTerm
1137
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
966
remove
1156
remove
cons
961
remove
1153
remove
cons
968
remove
785
remove
cons
963
remove
1152
remove
cons
nil
cons
cons
cons
cons
nil
cons
cons
982
remove
subst
eqMp
eqMp
eqMp
eqMp
nil
983
remove
87
ref
1141
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
52
ref
1112
remove
322
ref
488
remove
1060
remove
1137
remove
appTerm
absTerm
appTerm
appTerm
nil
cons
cons
1134
remove
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
992
ref
1079
remove
cons
nil
cons
nil
cons
cons
1028
ref
994
ref
appTerm
1157
def
betaConv
nil
1038
remove
53
ref
1157
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
173
ref
172
ref
1028
remove
nil
cons
cons
190
ref
1016
remove
cons
nil
cons
1158
def
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
proveHyp
proveHyp
eqMp
nil
85
ref
1116
remove
cons
87
ref
1119
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
85
ref
1076
remove
cons
87
ref
1077
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
52
ref
58
ref
1053
remove
appTerm
1075
remove
appTerm
nil
cons
cons
1040
remove
cons
nil
cons
cons
108
ref
subst
proveHyp
6
ref
254
ref
1030
ref
16
ref
appTerm
betaConv
appThm
452
ref
1054
remove
453
ref
1055
remove
6
ref
1030
ref
1056
remove
appTerm
betaConv
appThm
1030
ref
1066
remove
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
453
ref
992
ref
1030
ref
994
ref
appTerm
betaConv
absThm
appThm
appThm
nil
454
ref
1030
remove
nil
cons
cons
nil
cons
nil
cons
cons
459
ref
subst
eqMp
eqMp
eqMp
nil
85
ref
1037
remove
cons
87
ref
1039
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
52
ref
58
ref
1027
remove
appTerm
1036
remove
appTerm
nil
cons
cons
53
ref
140
ref
993
ref
140
ref
992
ref
1004
remove
absTerm
appTerm
absTerm
1159
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
6
ref
254
ref
1159
ref
16
ref
appTerm
betaConv
appThm
452
ref
138
ref
453
ref
141
ref
6
ref
1159
ref
142
ref
appTerm
betaConv
appThm
1159
ref
159
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
453
ref
993
ref
1159
ref
997
ref
appTerm
betaConv
absThm
appThm
appThm
nil
454
ref
1159
remove
nil
cons
cons
nil
cons
nil
cons
cons
459
ref
subst
eqMp
eqMp
eqMp
nil
140
ref
992
ref
140
ref
1005
remove
appTerm
absTerm
appTerm
thm
nil
172
ref
992
ref
140
ref
993
ref
322
ref
"k"
30
ref
var
1160
def
5
ref
397
ref
1160
ref
varTerm
1161
def
appTerm
1162
def
"Number.Natural.+"
const
36
remove
constTerm
1163
def
995
ref
appTerm
998
ref
appTerm
1164
def
appTerm
appTerm
28
ref
32
ref
"Data.List.@"
const
0
remove
13
remove
155
remove
cons
opType
constTerm
1165
def
994
ref
appTerm
997
ref
appTerm
1166
def
appTerm
1167
def
1161
ref
appTerm
appTerm
238
ref
1162
ref
995
ref
appTerm
appTerm
1000
ref
1161
ref
appTerm
appTerm
1002
ref
37
ref
1161
ref
appTerm
1168
def
995
ref
appTerm
appTerm
appTerm
appTerm
appTerm
1169
def
absTerm
1170
def
appTerm
1171
def
absTerm
1172
def
appTerm
1173
def
absTerm
1174
def
nil
cons
cons
nil
cons
nil
cons
cons
176
ref
subst
992
ref
nil
9
ref
1173
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
172
ref
1172
remove
nil
cons
cons
nil
cons
nil
cons
cons
176
ref
subst
993
ref
nil
9
ref
1171
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
326
ref
1170
remove
nil
cons
cons
nil
cons
nil
cons
cons
391
ref
subst
1160
ref
nil
9
ref
1169
ref
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
992
ref
1169
remove
absTerm
1175
def
994
ref
appTerm
1176
def
betaConv
1160
ref
140
ref
1175
ref
appTerm
1177
def
absTerm
1178
def
1161
ref
appTerm
1179
def
betaConv
1180
def
6
ref
912
ref
refl
1181
def
1163
ref
refl
1182
def
331
ref
appThm
998
ref
refl
1183
def
appThm
1184
def
appThm
appThm
221
ref
32
ref
refl
1185
def
nil
304
ref
997
ref
nil
cons
1186
def
cons
nil
cons
nil
cons
cons
1187
def
304
ref
310
ref
1165
ref
16
ref
appTerm
1188
def
306
ref
appTerm
appTerm
306
ref
appTerm
absTerm
1189
def
306
ref
appTerm
1190
def
betaConv
nil
140
ref
1189
ref
appTerm
1191
def
axiom
nil
52
ref
1191
remove
nil
cons
cons
53
ref
1190
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
1189
remove
nil
cons
cons
315
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
appThm
1192
def
nil
316
ref
594
ref
cons
nil
cons
nil
cons
cons
1193
def
317
ref
refl
subst
1194
def
appThm
appThm
238
ref
refl
1195
def
1181
ref
331
ref
appThm
1193
remove
316
ref
7
ref
398
ref
317
ref
appTerm
1196
def
appTerm
1197
def
absTerm
1198
def
317
ref
appTerm
1199
def
betaConv
nil
322
ref
1198
ref
appTerm
1200
def
axiom
nil
52
ref
1200
remove
nil
cons
cons
53
ref
1199
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
1198
remove
nil
cons
cons
328
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
1197
remove
nil
cons
cons
53
ref
19
ref
1196
ref
appTerm
25
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
85
ref
1196
remove
nil
cons
cons
nil
cons
nil
cons
cons
218
ref
subst
eqMp
subst
trans
appThm
33
ref
41
ref
appTerm
1201
def
refl
appThm
1002
ref
refl
1202
def
37
ref
41
ref
appTerm
1203
def
refl
1204
def
331
ref
appThm
nil
364
ref
594
remove
cons
nil
cons
nil
cons
cons
364
ref
227
ref
37
ref
366
ref
appTerm
1205
def
41
ref
appTerm
appTerm
366
ref
appTerm
absTerm
1206
def
366
ref
appTerm
1207
def
betaConv
nil
322
ref
1206
ref
appTerm
1208
def
axiom
nil
52
ref
1208
remove
nil
cons
cons
53
ref
1207
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
1206
remove
nil
cons
cons
517
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
1209
def
subst
trans
appThm
appThm
nil
"t2"
11
ref
var
1210
def
1002
ref
41
ref
appTerm
nil
cons
1211
def
cons
"t1"
11
ref
var
1212
def
1201
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
1210
ref
28
ref
238
ref
25
ref
appTerm
1213
def
1212
ref
varTerm
1214
def
appTerm
1210
ref
varTerm
1215
def
appTerm
appTerm
1215
ref
appTerm
absTerm
1216
def
1215
ref
appTerm
1217
def
betaConv
1212
ref
114
ref
1216
ref
appTerm
1218
def
absTerm
1219
def
1214
ref
appTerm
1220
def
betaConv
nil
114
ref
1219
ref
appTerm
1221
def
axiom
nil
52
ref
1221
remove
nil
cons
cons
53
ref
1220
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
1219
remove
nil
cons
cons
119
ref
1214
ref
nil
cons
cons
nil
cons
1222
def
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
1218
remove
nil
cons
cons
53
ref
1217
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
1216
remove
nil
cons
cons
119
ref
1215
ref
nil
cons
cons
nil
cons
1223
def
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
1224
def
subst
trans
appThm
nil
119
ref
1211
remove
cons
nil
cons
nil
cons
cons
552
ref
subst
trans
appThm
nil
9
ref
912
ref
1163
ref
41
ref
appTerm
998
ref
appTerm
1225
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
923
ref
subst
trans
sym
22
ref
eqMp
nil
52
ref
5
ref
912
ref
1163
ref
40
ref
appTerm
998
ref
appTerm
1226
def
appTerm
appTerm
28
ref
32
ref
1188
remove
997
ref
appTerm
appTerm
1227
def
41
ref
appTerm
appTerm
238
ref
912
ref
40
ref
appTerm
appTerm
1201
remove
appTerm
1002
ref
1203
ref
40
ref
appTerm
appTerm
appTerm
appTerm
appTerm
1228
def
nil
cons
cons
53
ref
114
ref
138
ref
140
ref
141
ref
5
ref
5
ref
912
ref
1163
ref
147
ref
appTerm
998
ref
appTerm
1229
def
appTerm
appTerm
28
ref
32
ref
1165
ref
142
ref
appTerm
1230
def
997
ref
appTerm
1231
def
appTerm
1232
def
41
ref
appTerm
appTerm
238
ref
912
ref
147
ref
appTerm
appTerm
146
ref
41
ref
appTerm
appTerm
1002
ref
1203
ref
147
ref
appTerm
appTerm
appTerm
appTerm
appTerm
1233
def
appTerm
5
ref
912
ref
1163
ref
163
ref
appTerm
998
ref
appTerm
1234
def
appTerm
appTerm
28
ref
32
ref
1165
remove
159
ref
appTerm
1235
def
997
ref
appTerm
appTerm
1236
def
41
ref
appTerm
appTerm
238
ref
912
ref
163
ref
appTerm
appTerm
332
remove
appTerm
1002
ref
1203
ref
163
ref
appTerm
appTerm
appTerm
appTerm
appTerm
1237
def
appTerm
1238
def
absTerm
1239
def
appTerm
1240
def
absTerm
1241
def
appTerm
1242
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
nil
115
ref
1241
remove
nil
cons
cons
nil
cons
nil
cons
cons
171
ref
subst
138
ref
nil
9
ref
1240
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
172
ref
1239
remove
nil
cons
cons
nil
cons
nil
cons
cons
176
ref
subst
141
ref
nil
9
ref
1238
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
52
ref
1233
remove
nil
cons
1243
def
cons
53
ref
1237
remove
nil
cons
1244
def
cons
nil
cons
cons
nil
cons
cons
1245
def
69
ref
subst
1245
remove
124
ref
subst
6
ref
1181
ref
1182
remove
236
ref
appThm
1183
remove
appThm
1246
def
appThm
appThm
221
ref
1185
remove
1187
remove
141
ref
310
remove
1235
remove
306
ref
appTerm
appTerm
158
ref
1230
remove
306
ref
appTerm
appTerm
appTerm
absTerm
1247
def
142
ref
appTerm
1248
def
betaConv
138
ref
140
ref
1247
ref
appTerm
1249
def
absTerm
1250
def
157
remove
appTerm
1251
def
betaConv
304
remove
114
ref
1250
ref
appTerm
1252
def
absTerm
1253
def
306
remove
appTerm
1254
def
betaConv
nil
140
ref
1253
ref
appTerm
1255
def
axiom
nil
52
ref
1255
remove
nil
cons
cons
53
ref
1254
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
1253
remove
nil
cons
cons
315
remove
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
1252
remove
nil
cons
cons
53
ref
1251
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
1250
remove
nil
cons
cons
189
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
1249
remove
nil
cons
cons
53
ref
1248
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
1247
remove
nil
cons
cons
192
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
appThm
1256
def
1194
remove
appThm
nil
141
ref
1231
ref
nil
cons
1257
def
cons
nil
cons
nil
cons
cons
339
ref
subst
trans
appThm
1195
ref
1181
remove
236
ref
appThm
355
remove
1132
remove
subst
trans
appThm
339
remove
appThm
1202
ref
1204
remove
236
ref
appThm
appThm
appThm
nil
1210
ref
1002
ref
1203
ref
229
ref
appTerm
appTerm
nil
cons
cons
1212
ref
188
remove
cons
nil
cons
cons
nil
cons
cons
1210
ref
28
ref
238
ref
21
ref
appTerm
1258
def
1214
ref
appTerm
1215
ref
appTerm
appTerm
1214
ref
appTerm
absTerm
1259
def
1215
remove
appTerm
1260
def
betaConv
1212
ref
114
ref
1259
ref
appTerm
1261
def
absTerm
1262
def
1214
remove
appTerm
1263
def
betaConv
nil
114
ref
1262
ref
appTerm
1264
def
axiom
nil
52
ref
1264
remove
nil
cons
cons
53
ref
1263
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
ref
115
ref
1262
remove
nil
cons
cons
1222
remove
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
1261
remove
nil
cons
cons
53
ref
1260
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
187
remove
115
ref
1259
remove
nil
cons
cons
1223
remove
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
1265
def
subst
trans
appThm
nil
189
remove
nil
cons
cons
552
ref
subst
trans
appThm
nil
9
ref
912
ref
1163
ref
229
ref
appTerm
998
ref
appTerm
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
923
ref
subst
trans
sym
22
ref
eqMp
eqMp
nil
85
ref
1243
remove
cons
87
ref
1244
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
52
ref
58
ref
1228
remove
appTerm
1242
remove
appTerm
nil
cons
cons
53
ref
140
ref
992
ref
5
ref
912
ref
1164
ref
appTerm
appTerm
28
ref
1167
ref
41
ref
appTerm
appTerm
238
ref
912
remove
995
ref
appTerm
appTerm
1000
ref
41
ref
appTerm
appTerm
1002
ref
1203
remove
995
ref
appTerm
appTerm
appTerm
appTerm
appTerm
absTerm
1266
def
appTerm
1267
def
nil
cons
1268
def
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
6
ref
254
ref
1266
ref
16
ref
appTerm
betaConv
appThm
452
ref
138
ref
453
ref
141
ref
6
ref
1266
ref
142
ref
appTerm
betaConv
appThm
1266
ref
159
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
453
ref
992
ref
1266
ref
994
ref
appTerm
betaConv
absThm
appThm
appThm
nil
454
ref
1266
remove
nil
cons
cons
nil
cons
nil
cons
cons
459
ref
subst
eqMp
eqMp
nil
52
ref
1268
remove
cons
53
ref
322
ref
1160
ref
5
ref
1177
ref
appTerm
140
ref
992
ref
5
ref
397
remove
228
ref
1161
ref
appTerm
1269
def
appTerm
1270
def
1164
ref
appTerm
appTerm
28
ref
1167
remove
1269
ref
appTerm
appTerm
238
ref
1270
ref
995
ref
appTerm
appTerm
1000
remove
1269
ref
appTerm
appTerm
1002
ref
37
ref
1269
ref
appTerm
1271
def
995
remove
appTerm
appTerm
appTerm
appTerm
appTerm
absTerm
1272
def
appTerm
1273
def
appTerm
1274
def
absTerm
1275
def
appTerm
1276
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
nil
326
ref
1275
remove
nil
cons
cons
nil
cons
nil
cons
cons
391
remove
subst
1160
ref
nil
9
ref
1274
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
52
ref
1177
remove
nil
cons
1277
def
cons
1278
def
53
ref
1273
remove
nil
cons
1279
def
cons
nil
cons
1280
def
cons
nil
cons
cons
1281
def
69
ref
subst
1281
remove
124
ref
subst
6
ref
1270
ref
refl
1282
def
1184
remove
appThm
appThm
221
ref
1192
remove
1269
ref
refl
1283
def
appThm
appThm
1195
ref
1282
ref
331
ref
appThm
nil
364
ref
1269
ref
nil
cons
cons
nil
cons
nil
cons
cons
1284
def
518
remove
subst
trans
appThm
33
remove
1269
ref
appTerm
1285
def
refl
appThm
1202
ref
1271
ref
refl
1286
def
331
remove
appThm
1284
remove
1209
remove
subst
trans
appThm
appThm
nil
1210
ref
1002
ref
1269
ref
appTerm
nil
cons
1287
def
cons
1212
ref
1285
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
1224
ref
subst
trans
appThm
nil
119
ref
1287
remove
cons
nil
cons
nil
cons
cons
552
remove
subst
trans
appThm
nil
9
ref
1270
ref
1225
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
923
remove
subst
trans
sym
22
ref
eqMp
nil
52
ref
5
ref
1270
ref
1226
remove
appTerm
appTerm
28
ref
1227
remove
1269
ref
appTerm
appTerm
238
ref
1270
ref
40
ref
appTerm
appTerm
1285
remove
appTerm
1002
ref
1271
ref
40
remove
appTerm
appTerm
appTerm
appTerm
appTerm
1288
def
nil
cons
cons
53
ref
114
remove
138
ref
140
ref
141
ref
5
ref
5
ref
1270
ref
1229
ref
appTerm
appTerm
28
ref
1232
ref
1269
ref
appTerm
appTerm
238
ref
1270
ref
147
ref
appTerm
appTerm
146
ref
1269
ref
appTerm
appTerm
1002
ref
1271
ref
147
ref
appTerm
appTerm
appTerm
appTerm
appTerm
1289
def
appTerm
5
ref
1270
ref
1234
remove
appTerm
appTerm
28
ref
1236
remove
1269
ref
appTerm
appTerm
238
ref
1270
remove
163
ref
appTerm
appTerm
162
remove
1269
ref
appTerm
1290
def
appTerm
1002
ref
1271
ref
163
remove
appTerm
appTerm
appTerm
appTerm
appTerm
1291
def
appTerm
1292
def
absTerm
1293
def
appTerm
1294
def
absTerm
1295
def
appTerm
1296
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
nil
115
remove
1295
remove
nil
cons
cons
nil
cons
nil
cons
cons
171
remove
subst
138
ref
nil
9
ref
1294
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
172
ref
1293
remove
nil
cons
cons
nil
cons
nil
cons
cons
176
remove
subst
141
ref
nil
9
ref
1292
remove
nil
cons
cons
nil
cons
nil
cons
cons
23
ref
subst
nil
52
ref
1289
remove
nil
cons
1297
def
cons
53
ref
1291
remove
nil
cons
1298
def
cons
nil
cons
cons
nil
cons
cons
1299
def
69
ref
subst
1299
remove
124
ref
subst
6
ref
1282
ref
1246
remove
nil
316
ref
998
remove
nil
cons
cons
364
ref
352
remove
cons
nil
cons
cons
nil
cons
cons
316
ref
227
ref
1163
ref
584
ref
appTerm
317
ref
appTerm
appTerm
228
remove
1163
remove
366
ref
appTerm
317
ref
appTerm
appTerm
appTerm
absTerm
1300
def
317
ref
appTerm
1301
def
betaConv
364
ref
322
ref
1300
ref
appTerm
1302
def
absTerm
1303
def
366
ref
appTerm
1304
def
betaConv
nil
322
ref
1303
ref
appTerm
1305
def
axiom
nil
52
ref
1305
remove
nil
cons
cons
53
ref
1304
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
1303
remove
nil
cons
cons
517
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
1302
remove
nil
cons
cons
53
ref
1301
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
1300
remove
nil
cons
cons
328
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
trans
appThm
nil
316
ref
1229
ref
nil
cons
cons
364
ref
1161
ref
nil
cons
1306
def
cons
1307
def
nil
cons
1308
def
cons
nil
cons
cons
945
ref
subst
trans
appThm
221
remove
1256
remove
1283
remove
appThm
appThm
1195
remove
1282
remove
236
ref
appThm
nil
353
remove
1308
remove
cons
nil
cons
cons
1309
def
945
remove
subst
trans
appThm
1290
ref
refl
appThm
1202
ref
1286
remove
236
remove
appThm
appThm
appThm
appThm
appThm
sym
nil
52
ref
1162
ref
1229
remove
appTerm
1310
def
nil
cons
1311
def
cons
1312
def
53
ref
28
ref
32
remove
158
remove
1231
ref
appTerm
appTerm
1313
def
1269
ref
appTerm
1314
def
appTerm
1315
def
238
ref
1162
ref
147
ref
appTerm
1316
def
appTerm
1317
def
1290
ref
appTerm
1002
ref
1271
remove
229
remove
appTerm
1318
def
appTerm
1319
def
appTerm
1320
def
appTerm
1321
def
nil
cons
1322
def
cons
nil
cons
1323
def
cons
nil
cons
cons
1324
def
69
ref
subst
1324
remove
124
ref
subst
316
ref
5
ref
398
remove
39
ref
1231
ref
appTerm
1325
def
appTerm
appTerm
28
ref
1313
remove
318
ref
appTerm
appTerm
1232
ref
317
ref
appTerm
appTerm
appTerm
absTerm
1326
def
1161
ref
appTerm
1327
def
betaConv
408
remove
1231
remove
appTerm
1328
def
betaConv
414
remove
nil
415
remove
53
ref
1328
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
416
remove
190
ref
1257
remove
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
322
ref
1326
ref
appTerm
nil
cons
cons
53
ref
1327
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
1326
remove
nil
cons
cons
327
ref
1306
ref
cons
nil
cons
1329
def
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
5
ref
1162
ref
1325
remove
appTerm
1330
def
appTerm
1315
remove
1232
remove
1161
ref
appTerm
1331
def
appTerm
1332
def
appTerm
1333
def
nil
cons
cons
1323
ref
cons
nil
cons
cons
108
ref
subst
proveHyp
1162
remove
refl
nil
992
ref
191
remove
cons
nil
cons
nil
cons
cons
993
remove
227
ref
39
remove
1166
remove
appTerm
appTerm
1164
remove
appTerm
absTerm
1334
def
997
remove
appTerm
1335
def
betaConv
992
ref
140
ref
1334
ref
appTerm
1336
def
absTerm
1337
def
994
ref
appTerm
1338
def
betaConv
nil
140
ref
1337
ref
appTerm
1339
def
axiom
nil
52
ref
1339
remove
nil
cons
cons
53
ref
1338
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
1337
remove
nil
cons
cons
1158
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
1336
remove
nil
cons
cons
53
ref
1335
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
173
ref
172
ref
1334
remove
nil
cons
cons
190
remove
1186
remove
cons
nil
cons
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
appThm
nil
9
ref
1311
ref
cons
nil
cons
nil
cons
cons
23
ref
subst
1310
ref
assume
eqMp
trans
sym
22
ref
eqMp
nil
52
ref
1330
ref
nil
cons
cons
1340
def
53
ref
5
ref
1332
ref
appTerm
1321
ref
appTerm
1341
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
nil
52
ref
1332
ref
nil
cons
1342
def
cons
1323
remove
cons
nil
cons
cons
1343
def
69
ref
subst
1343
remove
124
ref
subst
19
ref
"_16148"
11
ref
var
1344
def
28
ref
1344
remove
varTerm
appTerm
1320
ref
appTerm
absTerm
1345
def
1314
remove
appTerm
1346
def
appTerm
refl
1345
ref
1331
ref
appTerm
betaConv
1347
def
appThm
89
ref
1346
remove
betaConv
appThm
28
ref
1331
ref
appTerm
1348
def
1320
ref
appTerm
1349
def
refl
appThm
trans
1345
remove
refl
1350
def
1332
remove
assume
appThm
eqMp
sym
1175
ref
142
ref
appTerm
1351
def
betaConv
nil
1278
ref
53
ref
1351
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
173
ref
172
remove
1175
remove
nil
cons
cons
1352
def
192
remove
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
5
ref
1310
ref
appTerm
1348
remove
1317
remove
146
remove
1161
ref
appTerm
1353
def
appTerm
1002
remove
1168
remove
147
ref
appTerm
1354
def
appTerm
1355
def
appTerm
1356
def
appTerm
1357
def
appTerm
1358
def
nil
cons
cons
53
ref
1349
ref
nil
cons
1359
def
cons
nil
cons
1360
def
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
1312
ref
53
ref
5
ref
1357
ref
appTerm
1349
ref
appTerm
1361
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
nil
52
ref
1357
ref
nil
cons
1362
def
cons
1360
remove
cons
nil
cons
cons
1363
def
69
ref
subst
1363
remove
124
ref
subst
19
ref
"_16150"
11
ref
var
1364
def
28
ref
1364
remove
varTerm
appTerm
1320
ref
appTerm
absTerm
1365
def
1331
remove
appTerm
appTerm
refl
1365
remove
1356
ref
appTerm
betaConv
1366
def
appThm
89
ref
1347
remove
appThm
28
ref
1356
remove
appTerm
1320
ref
appTerm
refl
appThm
trans
1350
remove
1357
remove
assume
appThm
eqMp
sym
89
ref
1366
remove
appThm
254
ref
5
ref
1316
ref
appTerm
1367
def
refl
"_16152"
11
remove
var
1368
def
28
ref
1368
remove
varTerm
appTerm
1320
ref
appTerm
absTerm
1369
def
1353
ref
appTerm
betaConv
appThm
appThm
5
ref
7
ref
1316
ref
appTerm
1370
def
appTerm
1371
def
refl
1369
ref
1355
ref
appTerm
betaConv
appThm
appThm
appThm
nil
256
remove
1355
ref
nil
cons
cons
257
remove
1353
ref
nil
cons
1372
def
cons
258
remove
1316
ref
nil
cons
1373
def
cons
nil
cons
cons
cons
nil
cons
cons
nil
260
remove
1369
remove
nil
cons
cons
nil
cons
nil
cons
cons
286
remove
subst
subst
eqMp
sym
nil
52
ref
1373
ref
cons
1374
def
53
ref
28
ref
1353
ref
appTerm
1375
def
1320
ref
appTerm
1376
def
nil
cons
1377
def
cons
nil
cons
cons
nil
cons
cons
1378
def
69
ref
subst
1378
remove
124
ref
subst
19
ref
"_16154"
1
ref
var
1379
def
1375
ref
238
ref
1379
remove
varTerm
appTerm
1290
ref
appTerm
1319
ref
appTerm
appTerm
absTerm
1380
def
1316
ref
appTerm
1381
def
appTerm
refl
1380
ref
21
remove
appTerm
betaConv
appThm
89
ref
1381
remove
betaConv
appThm
1375
ref
1258
remove
1290
ref
appTerm
1319
ref
appTerm
appTerm
refl
appThm
trans
1380
remove
refl
nil
9
remove
1373
ref
cons
nil
cons
nil
cons
cons
23
remove
subst
1316
ref
assume
eqMp
appThm
eqMp
sym
1375
ref
refl
nil
1210
remove
1319
ref
nil
cons
cons
1212
remove
1290
ref
nil
cons
1382
def
cons
nil
cons
cons
nil
cons
cons
1383
def
1265
remove
subst
appThm
sym
nil
1374
remove
53
ref
28
ref
1290
ref
appTerm
1353
remove
appTerm
nil
cons
1384
def
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
nil
316
ref
1306
remove
cons
nil
cons
nil
cons
cons
417
remove
subst
eqMp
nil
52
ref
1384
remove
cons
53
ref
1375
remove
1290
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
119
remove
1382
remove
cons
262
remove
1372
remove
cons
nil
cons
cons
nil
cons
cons
739
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
85
ref
1373
remove
cons
1385
def
87
ref
1377
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
nil
52
ref
1367
remove
1376
remove
appTerm
nil
cons
cons
53
ref
1371
remove
28
remove
1355
remove
appTerm
1386
def
1320
remove
appTerm
1387
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
124
ref
subst
proveHyp
nil
52
ref
1370
remove
nil
cons
1388
def
cons
1389
def
53
ref
1387
remove
nil
cons
1390
def
cons
nil
cons
cons
nil
cons
cons
1391
def
69
ref
subst
1391
remove
124
ref
subst
19
ref
"_16156"
1
ref
var
1392
def
1386
ref
238
remove
1392
remove
varTerm
appTerm
1290
ref
appTerm
1319
ref
appTerm
appTerm
absTerm
1393
def
1316
ref
appTerm
1394
def
appTerm
refl
1393
ref
25
ref
appTerm
betaConv
appThm
89
remove
1394
remove
betaConv
appThm
1386
ref
1213
remove
1290
remove
appTerm
1319
remove
appTerm
appTerm
refl
appThm
trans
1393
remove
refl
nil
1389
remove
53
ref
19
ref
1316
remove
appTerm
25
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
nil
1385
remove
nil
cons
nil
cons
cons
218
remove
subst
eqMp
1395
def
appThm
eqMp
sym
1386
remove
refl
1383
remove
1224
remove
subst
appThm
sym
1202
remove
nil
1307
remove
354
remove
cons
nil
cons
cons
316
ref
19
ref
"Number.Natural.<="
const
226
remove
constTerm
1396
def
317
ref
appTerm
366
ref
appTerm
1397
def
appTerm
7
remove
585
remove
appTerm
1398
def
appTerm
1399
def
absTerm
1400
def
317
ref
appTerm
1401
def
betaConv
364
ref
322
ref
1400
ref
appTerm
1402
def
absTerm
1403
def
366
ref
appTerm
1404
def
betaConv
643
ref
364
ref
643
ref
316
ref
1399
remove
assume
sym
19
remove
1398
remove
appTerm
1397
ref
appTerm
1405
def
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
nil
322
ref
364
ref
322
ref
316
ref
1405
remove
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
52
ref
322
ref
1403
ref
appTerm
nil
cons
cons
53
ref
1404
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
1403
remove
nil
cons
cons
517
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
1402
remove
nil
cons
cons
53
ref
1401
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
1400
remove
nil
cons
cons
328
ref
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
8
remove
1395
remove
appThm
220
remove
trans
trans
sym
22
remove
eqMp
nil
52
ref
1396
remove
147
remove
appTerm
1161
remove
appTerm
nil
cons
cons
53
ref
227
ref
1318
ref
appTerm
1354
ref
appTerm
nil
cons
1406
def
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
1309
remove
316
remove
5
ref
1397
remove
appTerm
227
ref
37
remove
584
remove
appTerm
318
remove
appTerm
appTerm
1205
remove
317
ref
appTerm
appTerm
appTerm
absTerm
1407
def
317
remove
appTerm
1408
def
betaConv
364
remove
322
ref
1407
ref
appTerm
1409
def
absTerm
1410
def
366
remove
appTerm
1411
def
betaConv
nil
322
ref
1410
ref
appTerm
1412
def
axiom
nil
52
ref
1412
remove
nil
cons
cons
53
ref
1411
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
1410
remove
nil
cons
cons
517
remove
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
52
ref
1409
remove
nil
cons
cons
53
ref
1408
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
ref
326
ref
1407
remove
nil
cons
cons
328
remove
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
subst
eqMp
nil
52
ref
1406
remove
cons
53
ref
227
remove
1354
ref
appTerm
1318
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
327
remove
1318
remove
nil
cons
cons
"y"
30
remove
var
1354
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
390
remove
739
remove
subst
subst
eqMp
appThm
eqMp
eqMp
eqMp
nil
85
ref
1388
remove
cons
87
ref
1390
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
nil
85
ref
1362
ref
cons
87
ref
1359
ref
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
nil
52
ref
58
ref
1310
remove
appTerm
1361
remove
appTerm
nil
cons
cons
53
ref
5
ref
1358
remove
appTerm
1349
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
"r"
1
remove
var
1413
def
1359
remove
cons
53
ref
1362
remove
cons
1312
remove
nil
cons
cons
cons
nil
cons
cons
nil
52
ref
59
remove
207
remove
1413
ref
varTerm
1414
def
appTerm
1415
def
appTerm
nil
cons
1416
def
cons
53
ref
5
ref
57
remove
appTerm
1414
ref
appTerm
nil
cons
1417
def
cons
nil
cons
cons
nil
cons
cons
1418
def
69
ref
subst
1418
remove
124
ref
subst
nil
206
remove
53
ref
1414
remove
nil
cons
1419
def
cons
nil
cons
1420
def
cons
nil
cons
cons
1421
def
69
remove
subst
1421
remove
124
remove
subst
nil
86
remove
87
ref
1415
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
1422
def
101
ref
subst
108
ref
proveHyp
102
remove
eqMp
nil
201
remove
1420
remove
cons
nil
cons
cons
108
ref
subst
proveHyp
1422
remove
211
remove
subst
eqMp
eqMp
nil
209
remove
87
ref
1419
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
nil
85
ref
1416
remove
cons
87
ref
1417
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
1423
def
subst
eqMp
eqMp
eqMp
eqMp
nil
85
ref
1342
ref
cons
87
ref
1322
ref
cons
nil
cons
1424
def
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
nil
52
ref
58
ref
1330
remove
appTerm
1341
remove
appTerm
nil
cons
cons
53
ref
5
remove
1333
remove
appTerm
1321
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
1413
remove
1322
remove
cons
53
ref
1342
remove
cons
1340
remove
nil
cons
cons
cons
nil
cons
cons
1423
remove
subst
eqMp
eqMp
eqMp
nil
85
ref
1311
remove
cons
1424
remove
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
85
ref
1297
remove
cons
87
ref
1298
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
52
ref
58
ref
1288
remove
appTerm
1296
remove
appTerm
nil
cons
cons
1280
remove
cons
nil
cons
cons
108
ref
subst
proveHyp
6
ref
254
ref
1272
ref
16
remove
appTerm
betaConv
appThm
452
remove
138
remove
453
ref
141
remove
6
ref
1272
ref
142
remove
appTerm
betaConv
appThm
1272
ref
159
remove
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
453
remove
992
remove
1272
ref
994
remove
appTerm
betaConv
absThm
appThm
appThm
nil
454
remove
1272
remove
nil
cons
cons
nil
cons
nil
cons
cons
459
remove
subst
eqMp
eqMp
eqMp
nil
85
remove
1277
remove
cons
87
remove
1279
remove
cons
nil
cons
cons
nil
cons
cons
101
remove
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
52
ref
58
remove
1267
remove
appTerm
1276
remove
appTerm
nil
cons
cons
53
ref
322
remove
1178
ref
appTerm
nil
cons
1425
def
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
6
ref
254
remove
1178
ref
41
remove
appTerm
betaConv
appThm
643
ref
1160
ref
6
remove
1180
ref
appThm
1178
ref
1269
remove
appTerm
betaConv
appThm
absThm
appThm
appThm
appThm
643
remove
1160
remove
1180
remove
absThm
appThm
appThm
nil
679
remove
1178
remove
nil
cons
1426
def
cons
nil
cons
nil
cons
cons
991
remove
subst
eqMp
eqMp
nil
52
remove
1425
remove
cons
53
ref
1179
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
325
remove
326
remove
1426
remove
cons
1329
remove
cons
nil
cons
cons
135
ref
subst
eqMp
eqMp
nil
1278
remove
53
remove
1176
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
remove
subst
proveHyp
173
remove
1352
remove
1158
remove
cons
nil
cons
cons
135
remove
subst
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
140
remove
1174
remove
appTerm
thm