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