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