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