6
version
"Data.Bool./\\"
const
"->"
typeOp
0
def
"bool"
typeOp
nil
opType
1
def
0
ref
1
ref
1
ref
nil
cons
2
def
cons
opType
3
def
nil
cons
cons
opType
4
def
constTerm
5
def
refl
"="
const
6
def
0
ref
"Number.Natural.natural"
typeOp
nil
opType
7
def
0
ref
7
ref
2
ref
cons
opType
8
def
nil
cons
cons
opType
constTerm
9
def
refl
10
def
6
ref
0
ref
0
ref
7
ref
7
ref
nil
cons
11
def
cons
opType
12
def
0
ref
12
ref
2
ref
cons
opType
13
def
nil
cons
cons
opType
constTerm
14
def
"select"
const
15
def
0
ref
13
ref
12
ref
nil
cons
16
def
cons
opType
constTerm
"fn"
12
ref
var
17
def
5
ref
9
ref
17
ref
varTerm
18
def
"Number.Natural.zero"
const
7
ref
constTerm
19
def
appTerm
appTerm
20
def
19
ref
appTerm
appTerm
21
def
"Data.Bool.!"
const
22
def
0
ref
8
ref
2
ref
cons
opType
constTerm
23
def
"n"
7
ref
var
24
def
9
ref
18
ref
"Number.Natural.suc"
const
12
ref
constTerm
25
def
24
ref
varTerm
26
def
appTerm
27
def
appTerm
appTerm
28
def
25
ref
25
ref
18
remove
26
ref
appTerm
29
def
appTerm
appTerm
30
def
appTerm
absTerm
appTerm
appTerm
absTerm
31
def
appTerm
32
def
appTerm
"Number.Natural.bit0"
32
ref
defineConst
33
def
pop
12
ref
constTerm
34
def
appTerm
assume
sym
14
remove
34
ref
appTerm
32
ref
appTerm
assume
sym
deductAntisym
33
remove
eqMp
35
def
19
ref
refl
36
def
appThm
appThm
36
remove
appThm
appThm
23
ref
refl
37
def
24
ref
10
remove
35
ref
27
ref
refl
appThm
appThm
25
ref
refl
38
def
38
remove
35
remove
26
ref
refl
39
def
appThm
appThm
appThm
appThm
absThm
appThm
appThm
31
ref
32
remove
appTerm
40
def
betaConv
"Data.Bool.?"
const
41
def
0
ref
13
ref
2
ref
cons
opType
constTerm
42
def
refl
17
ref
21
ref
refl
37
remove
24
ref
28
ref
refl
"m"
7
ref
var
43
def
24
ref
25
ref
25
ref
43
remove
varTerm
appTerm
appTerm
absTerm
absTerm
44
def
29
ref
appTerm
betaConv
39
remove
appThm
"n'"
7
ref
var
30
remove
absTerm
26
ref
appTerm
betaConv
trans
appThm
absThm
appThm
appThm
absThm
appThm
"f"
0
ref
7
ref
16
ref
cons
opType
45
def
var
46
def
42
ref
17
ref
21
remove
23
ref
24
ref
28
remove
46
ref
varTerm
29
remove
appTerm
26
ref
appTerm
appTerm
absTerm
appTerm
47
def
appTerm
absTerm
appTerm
absTerm
48
def
44
ref
appTerm
49
def
betaConv
"e"
7
ref
var
50
def
22
ref
0
ref
0
ref
45
ref
2
ref
cons
opType
51
def
2
ref
cons
opType
constTerm
52
def
46
remove
42
ref
17
remove
5
ref
20
remove
50
remove
varTerm
appTerm
appTerm
47
remove
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
53
def
19
ref
appTerm
54
def
betaConv
"A"
11
remove
cons
nil
cons
55
def
nil
nil
cons
56
def
cons
57
def
nil
"P"
0
ref
"A"
varType
58
def
2
ref
cons
opType
59
def
var
60
def
"e"
58
ref
var
61
def
22
ref
0
ref
0
ref
0
ref
58
ref
0
ref
7
ref
58
ref
nil
cons
62
def
cons
opType
63
def
nil
cons
64
def
cons
opType
65
def
2
ref
cons
opType
66
def
2
ref
cons
opType
constTerm
67
def
"f"
65
ref
var
68
def
41
ref
0
ref
0
ref
63
ref
2
ref
cons
opType
69
def
2
ref
cons
opType
70
def
constTerm
"fn"
63
remove
var
71
def
5
ref
6
ref
0
ref
58
ref
59
ref
nil
cons
72
def
cons
opType
constTerm
73
def
71
remove
varTerm
74
def
19
ref
appTerm
appTerm
61
ref
varTerm
75
def
appTerm
appTerm
23
ref
24
ref
73
ref
74
ref
27
ref
appTerm
appTerm
68
ref
varTerm
76
def
74
remove
26
ref
appTerm
appTerm
26
ref
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
77
def
appTerm
78
def
absTerm
79
def
appTerm
80
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
6
ref
4
ref
constTerm
81
def
22
ref
0
ref
59
ref
2
ref
cons
opType
82
def
constTerm
83
def
60
ref
varTerm
84
def
appTerm
85
def
appTerm
refl
"p"
59
ref
var
86
def
6
ref
0
ref
59
ref
82
ref
nil
cons
cons
opType
constTerm
86
ref
varTerm
87
def
appTerm
"x"
58
ref
var
88
def
"Data.Bool.T"
const
1
ref
constTerm
89
def
absTerm
90
def
appTerm
absTerm
91
def
84
ref
appTerm
betaConv
92
def
appThm
nil
6
ref
0
ref
82
ref
0
ref
82
ref
2
ref
cons
opType
93
def
nil
cons
cons
opType
constTerm
94
def
83
ref
appTerm
91
remove
appTerm
axiom
84
ref
refl
95
def
appThm
96
def
eqMp
sym
97
def
subst
61
ref
nil
"t"
1
ref
var
98
def
80
remove
nil
cons
cons
nil
cons
nil
cons
cons
81
ref
98
ref
varTerm
99
def
appTerm
89
ref
appTerm
assume
sym
nil
89
ref
axiom
100
def
eqMp
99
ref
assume
100
ref
deductAntisym
deductAntisym
101
def
subst
nil
"P"
66
remove
var
102
def
79
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
65
ref
nil
cons
cons
nil
cons
103
def
56
ref
cons
97
ref
subst
subst
68
ref
nil
98
ref
78
remove
nil
cons
104
def
cons
nil
cons
nil
cons
cons
101
ref
subst
68
remove
"Data.Bool.?!"
const
105
def
70
remove
constTerm
77
ref
appTerm
106
def
absTerm
107
def
76
ref
appTerm
108
def
betaConv
61
remove
67
remove
107
ref
appTerm
109
def
absTerm
110
def
75
ref
appTerm
111
def
betaConv
nil
83
ref
110
ref
appTerm
112
def
axiom
nil
"p"
1
ref
var
113
def
112
remove
nil
cons
cons
"q"
1
ref
var
114
def
111
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
81
ref
"Data.Bool.==>"
const
4
ref
constTerm
115
def
113
ref
varTerm
116
def
appTerm
117
def
114
ref
varTerm
118
def
appTerm
119
def
appTerm
120
def
refl
113
ref
114
ref
81
ref
5
ref
116
ref
appTerm
121
def
118
ref
appTerm
122
def
appTerm
123
def
116
ref
appTerm
absTerm
124
def
absTerm
125
def
116
ref
appTerm
betaConv
118
ref
refl
126
def
appThm
124
remove
118
ref
appTerm
betaConv
trans
appThm
nil
6
ref
0
ref
4
ref
0
ref
4
ref
2
ref
cons
opType
127
def
nil
cons
cons
opType
constTerm
128
def
115
ref
appTerm
125
remove
appTerm
axiom
116
ref
refl
129
def
appThm
126
ref
appThm
eqMp
130
def
sym
131
def
123
remove
refl
114
ref
6
ref
0
ref
127
ref
0
ref
127
remove
2
ref
cons
opType
nil
cons
cons
opType
constTerm
132
def
"f"
4
remove
var
133
def
133
ref
varTerm
134
def
116
ref
appTerm
118
ref
appTerm
absTerm
135
def
appTerm
133
ref
134
ref
89
ref
appTerm
89
ref
appTerm
absTerm
136
def
appTerm
absTerm
137
def
118
ref
appTerm
betaConv
appThm
6
ref
0
ref
3
ref
0
ref
3
ref
2
ref
cons
opType
138
def
nil
cons
cons
opType
constTerm
139
def
121
remove
appTerm
refl
113
ref
137
remove
absTerm
140
def
116
ref
appTerm
betaConv
appThm
nil
128
remove
5
ref
appTerm
140
ref
appTerm
axiom
141
def
129
remove
appThm
eqMp
126
ref
appThm
eqMp
142
def
sym
133
ref
134
ref
refl
nil
98
ref
116
ref
nil
cons
143
def
cons
nil
cons
nil
cons
cons
101
ref
subst
116
ref
assume
144
def
eqMp
appThm
nil
98
ref
118
ref
nil
cons
145
def
cons
nil
cons
nil
cons
cons
101
ref
subst
118
ref
assume
146
def
eqMp
appThm
absThm
eqMp
147
def
nil
"P"
1
ref
var
148
def
143
ref
cons
"Q"
1
ref
var
149
def
145
ref
cons
nil
cons
150
def
cons
nil
cons
cons
81
ref
refl
151
def
133
ref
134
remove
148
ref
varTerm
152
def
appTerm
153
def
149
ref
varTerm
154
def
appTerm
absTerm
155
def
113
ref
114
ref
116
ref
absTerm
absTerm
156
def
appTerm
betaConv
156
ref
152
ref
appTerm
betaConv
154
ref
refl
157
def
appThm
114
ref
152
ref
absTerm
154
ref
appTerm
betaConv
trans
trans
appThm
136
ref
156
ref
appTerm
betaConv
156
ref
89
ref
appTerm
betaConv
89
ref
refl
158
def
appThm
114
ref
89
ref
absTerm
89
ref
appTerm
betaConv
trans
trans
appThm
81
ref
5
ref
152
ref
appTerm
159
def
154
ref
appTerm
160
def
appTerm
refl
114
ref
132
remove
133
remove
153
remove
118
ref
appTerm
absTerm
appTerm
136
ref
appTerm
absTerm
154
ref
appTerm
betaConv
appThm
139
remove
159
remove
appTerm
refl
140
remove
152
ref
appTerm
betaConv
appThm
141
remove
152
ref
refl
appThm
eqMp
157
ref
appThm
eqMp
160
remove
assume
eqMp
161
def
156
remove
refl
appThm
eqMp
sym
100
ref
eqMp
162
def
subst
163
def
deductAntisym
eqMp
130
remove
119
ref
assume
eqMp
sym
144
ref
eqMp
151
ref
135
remove
113
ref
114
ref
118
ref
absTerm
164
def
absTerm
165
def
appTerm
betaConv
165
ref
116
ref
appTerm
betaConv
126
remove
appThm
164
ref
118
ref
appTerm
betaConv
trans
trans
appThm
136
remove
165
ref
appTerm
betaConv
165
ref
89
ref
appTerm
betaConv
158
remove
appThm
164
ref
89
ref
appTerm
betaConv
trans
trans
166
def
appThm
142
remove
122
remove
assume
eqMp
165
ref
refl
167
def
appThm
eqMp
sym
100
ref
eqMp
168
def
proveHyp
169
def
deductAntisym
170
def
subst
proveHyp
"A"
62
ref
cons
171
def
nil
cons
172
def
60
ref
110
remove
nil
cons
cons
88
ref
75
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
113
ref
85
ref
nil
cons
173
def
cons
114
ref
84
ref
88
ref
varTerm
174
def
appTerm
175
def
nil
cons
176
def
cons
nil
cons
cons
nil
cons
cons
177
def
131
ref
subst
177
remove
168
remove
147
remove
deductAntisym
178
def
subst
81
ref
175
ref
appTerm
refl
90
remove
174
ref
appTerm
betaConv
appThm
92
remove
96
remove
85
remove
assume
eqMp
eqMp
174
ref
refl
appThm
eqMp
sym
100
ref
eqMp
eqMp
nil
148
ref
173
remove
cons
149
ref
176
ref
cons
nil
cons
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
179
def
subst
eqMp
eqMp
nil
113
ref
109
remove
nil
cons
cons
114
ref
108
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
proveHyp
103
remove
102
remove
107
remove
nil
cons
cons
"x"
65
remove
var
76
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
179
ref
subst
eqMp
eqMp
nil
113
ref
106
remove
nil
cons
cons
114
ref
104
remove
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
proveHyp
"A"
64
remove
cons
nil
cons
"P"
69
remove
var
77
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
113
ref
105
remove
82
ref
constTerm
180
def
84
ref
appTerm
181
def
nil
cons
182
def
cons
183
def
114
ref
41
remove
82
ref
constTerm
184
def
84
ref
appTerm
185
def
nil
cons
186
def
cons
nil
cons
cons
nil
cons
cons
187
def
131
ref
subst
187
remove
178
ref
subst
nil
183
remove
114
ref
5
ref
185
ref
appTerm
83
ref
88
ref
83
ref
"y"
58
ref
var
188
def
115
ref
5
ref
175
ref
appTerm
84
ref
188
ref
varTerm
189
def
appTerm
appTerm
appTerm
73
remove
174
ref
appTerm
189
ref
appTerm
190
def
appTerm
absTerm
appTerm
absTerm
appTerm
191
def
appTerm
192
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
193
def
170
ref
subst
81
ref
181
ref
appTerm
194
def
refl
86
ref
5
ref
184
ref
87
ref
appTerm
195
def
appTerm
83
ref
88
ref
83
ref
188
remove
115
ref
5
remove
87
ref
174
ref
appTerm
196
def
appTerm
87
ref
189
remove
appTerm
appTerm
appTerm
190
remove
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
197
def
84
ref
appTerm
betaConv
appThm
nil
94
ref
180
remove
appTerm
197
remove
appTerm
axiom
95
ref
appThm
eqMp
nil
113
ref
194
remove
192
ref
appTerm
nil
cons
cons
114
ref
115
ref
181
remove
appTerm
192
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
proveHyp
193
remove
nil
113
ref
81
ref
116
ref
appTerm
198
def
118
ref
appTerm
199
def
nil
cons
200
def
cons
201
def
114
ref
119
ref
nil
cons
202
def
cons
nil
cons
203
def
cons
nil
cons
cons
204
def
131
ref
subst
204
remove
178
ref
subst
131
ref
178
ref
199
remove
assume
205
def
144
remove
eqMp
eqMp
163
ref
deductAntisym
eqMp
206
def
eqMp
nil
148
ref
200
remove
cons
207
def
149
ref
202
ref
cons
nil
cons
208
def
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
209
def
subst
eqMp
eqMp
nil
148
ref
186
ref
cons
210
def
149
ref
191
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
162
ref
subst
proveHyp
eqMp
nil
148
ref
182
remove
cons
149
ref
186
ref
cons
nil
cons
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
subst
nil
113
ref
23
ref
53
ref
appTerm
nil
cons
cons
114
ref
54
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
proveHyp
55
remove
"P"
8
remove
var
211
def
53
remove
nil
cons
cons
"x"
7
ref
var
19
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
179
ref
subst
eqMp
eqMp
nil
113
ref
52
remove
48
ref
appTerm
nil
cons
cons
114
ref
49
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
proveHyp
"A"
45
ref
nil
cons
cons
nil
cons
"P"
51
remove
var
48
remove
nil
cons
cons
"x"
45
remove
var
44
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
179
ref
subst
eqMp
eqMp
eqMp
nil
113
ref
42
remove
31
ref
appTerm
nil
cons
cons
114
ref
40
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
proveHyp
"A"
16
remove
cons
nil
cons
"p"
13
remove
var
31
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
113
ref
195
ref
nil
cons
212
def
cons
213
def
114
ref
81
ref
87
ref
15
remove
0
ref
59
ref
62
remove
cons
opType
constTerm
87
ref
appTerm
appTerm
214
def
appTerm
215
def
89
ref
appTerm
216
def
nil
cons
217
def
cons
nil
cons
218
def
cons
nil
cons
cons
219
def
131
ref
subst
219
remove
178
ref
subst
184
ref
refl
nil
"t"
59
ref
var
87
ref
nil
cons
220
def
cons
nil
cons
nil
cons
cons
171
remove
"B"
2
ref
cons
nil
cons
cons
56
ref
cons
"t"
0
ref
58
ref
"B"
varType
nil
cons
cons
opType
221
def
var
222
def
6
remove
0
ref
221
ref
0
ref
221
ref
2
ref
cons
opType
223
def
nil
cons
cons
opType
constTerm
88
ref
222
remove
varTerm
224
def
174
ref
appTerm
absTerm
appTerm
224
ref
appTerm
absTerm
225
def
224
ref
appTerm
226
def
betaConv
nil
22
ref
0
remove
223
ref
2
ref
cons
opType
constTerm
225
ref
appTerm
227
def
axiom
nil
113
ref
227
remove
nil
cons
cons
114
ref
226
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
proveHyp
"A"
221
ref
nil
cons
cons
nil
cons
"P"
223
remove
var
225
remove
nil
cons
cons
"x"
221
remove
var
224
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
179
ref
subst
eqMp
eqMp
subst
subst
appThm
nil
98
ref
212
ref
cons
nil
cons
nil
cons
cons
228
def
101
ref
subst
195
ref
assume
eqMp
trans
sym
100
ref
eqMp
nil
113
ref
184
ref
88
ref
196
ref
absTerm
appTerm
nil
cons
cons
218
ref
cons
nil
cons
cons
170
ref
subst
proveHyp
nil
60
ref
220
ref
cons
149
ref
217
remove
cons
nil
cons
229
def
cons
nil
cons
cons
nil
113
ref
83
ref
88
ref
115
ref
175
ref
appTerm
230
def
154
ref
appTerm
231
def
absTerm
232
def
appTerm
233
def
nil
cons
234
def
cons
235
def
114
ref
115
ref
184
ref
88
ref
175
ref
absTerm
236
def
appTerm
237
def
appTerm
154
ref
appTerm
238
def
nil
cons
239
def
cons
nil
cons
240
def
cons
nil
cons
cons
241
def
206
remove
nil
113
ref
202
ref
cons
242
def
114
ref
115
ref
118
ref
appTerm
243
def
116
ref
appTerm
nil
cons
244
def
cons
nil
cons
245
def
cons
nil
cons
cons
178
ref
subst
proveHyp
243
ref
refl
205
remove
appThm
sym
nil
113
ref
145
ref
cons
246
def
114
ref
145
ref
cons
nil
cons
247
def
cons
nil
cons
cons
248
def
131
ref
subst
248
remove
178
ref
subst
146
remove
eqMp
nil
148
ref
145
remove
cons
150
ref
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
249
def
eqMp
nil
246
ref
114
ref
143
ref
cons
nil
cons
250
def
cons
nil
cons
cons
170
ref
subst
nil
148
ref
202
remove
cons
251
def
149
ref
244
remove
cons
nil
cons
252
def
cons
nil
cons
cons
253
def
151
remove
155
remove
165
ref
appTerm
betaConv
165
remove
152
remove
appTerm
betaConv
157
remove
appThm
164
remove
154
ref
appTerm
betaConv
trans
trans
appThm
166
remove
appThm
161
remove
167
remove
appThm
eqMp
sym
100
ref
eqMp
254
def
subst
eqMp
170
ref
253
remove
162
ref
subst
eqMp
deductAntisym
deductAntisym
255
def
subst
241
ref
131
ref
subst
241
remove
178
ref
subst
nil
60
ref
88
ref
115
ref
236
ref
174
ref
appTerm
256
def
appTerm
154
ref
appTerm
257
def
absTerm
258
def
nil
cons
cons
nil
cons
nil
cons
cons
97
ref
subst
88
ref
nil
98
ref
257
remove
nil
cons
cons
nil
cons
nil
cons
cons
101
ref
subst
nil
113
ref
256
ref
nil
cons
259
def
cons
114
ref
154
ref
nil
cons
260
def
cons
nil
cons
261
def
cons
nil
cons
cons
262
def
131
ref
subst
262
remove
178
ref
subst
256
ref
betaConv
263
def
256
remove
assume
eqMp
nil
113
ref
176
ref
cons
261
ref
cons
nil
cons
cons
264
def
170
ref
subst
265
def
proveHyp
nil
"_8"
58
remove
var
266
def
174
ref
nil
cons
267
def
cons
nil
cons
nil
cons
cons
232
ref
266
remove
varTerm
268
def
appTerm
269
def
betaConv
nil
235
ref
114
ref
269
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
172
ref
60
ref
232
remove
nil
cons
cons
270
def
88
ref
268
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
179
ref
subst
eqMp
eqMp
subst
271
def
eqMp
eqMp
nil
148
ref
259
remove
cons
149
ref
260
ref
cons
nil
cons
272
def
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
113
ref
83
ref
258
remove
appTerm
nil
cons
cons
240
remove
cons
nil
cons
cons
170
ref
subst
proveHyp
172
ref
60
ref
236
remove
nil
cons
cons
273
def
272
ref
cons
nil
cons
cons
nil
235
ref
114
ref
115
ref
185
ref
appTerm
274
def
154
ref
appTerm
nil
cons
275
def
cons
nil
cons
cons
nil
cons
cons
276
def
131
ref
subst
276
remove
178
ref
subst
nil
113
ref
186
remove
cons
277
def
261
ref
cons
nil
cons
cons
278
def
131
ref
subst
278
remove
178
ref
subst
nil
235
remove
261
ref
cons
nil
cons
cons
279
def
170
ref
subst
114
ref
115
ref
83
ref
88
ref
230
remove
118
ref
appTerm
absTerm
appTerm
appTerm
118
ref
appTerm
absTerm
280
def
154
ref
appTerm
281
def
betaConv
nil
277
remove
114
ref
22
ref
138
remove
constTerm
282
def
280
ref
appTerm
283
def
nil
cons
284
def
cons
nil
cons
cons
nil
cons
cons
285
def
170
ref
subst
81
ref
185
remove
appTerm
286
def
refl
86
ref
282
ref
114
ref
115
ref
83
ref
88
ref
115
ref
196
ref
appTerm
287
def
118
ref
appTerm
absTerm
appTerm
appTerm
118
ref
appTerm
absTerm
appTerm
absTerm
288
def
84
remove
appTerm
betaConv
appThm
nil
94
remove
184
remove
appTerm
288
remove
appTerm
axiom
95
remove
appThm
eqMp
289
def
nil
113
ref
286
remove
283
ref
appTerm
nil
cons
cons
114
ref
274
remove
283
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
proveHyp
285
remove
209
ref
subst
eqMp
eqMp
nil
113
ref
284
remove
cons
114
ref
281
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
proveHyp
"A"
2
remove
cons
nil
cons
290
def
"P"
3
remove
var
291
def
280
remove
nil
cons
cons
"x"
1
ref
var
292
def
260
remove
cons
nil
cons
cons
nil
cons
cons
179
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
210
remove
272
ref
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
nil
148
ref
234
ref
cons
293
def
149
ref
275
remove
cons
nil
cons
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
293
ref
149
ref
239
ref
cons
nil
cons
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
nil
113
ref
115
ref
233
ref
appTerm
294
def
238
ref
appTerm
nil
cons
cons
114
ref
115
ref
238
ref
appTerm
233
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
178
ref
subst
proveHyp
nil
113
ref
239
ref
cons
114
ref
234
ref
cons
nil
cons
cons
nil
cons
cons
295
def
131
ref
subst
295
remove
178
ref
subst
nil
270
remove
nil
cons
nil
cons
cons
97
ref
subst
88
ref
nil
98
ref
231
remove
nil
cons
cons
nil
cons
nil
cons
cons
101
ref
subst
264
ref
131
ref
subst
264
remove
178
ref
subst
263
remove
sym
175
remove
assume
eqMp
172
ref
273
remove
88
ref
267
remove
cons
nil
cons
296
def
cons
nil
cons
cons
289
remove
sym
nil
291
ref
149
ref
294
remove
154
remove
appTerm
297
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
290
ref
56
remove
cons
97
ref
subst
298
def
subst
149
ref
nil
98
ref
297
remove
nil
cons
cons
nil
cons
nil
cons
cons
101
ref
subst
279
ref
131
ref
subst
279
remove
178
ref
subst
265
remove
271
remove
eqMp
eqMp
nil
293
remove
272
ref
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
subst
proveHyp
nil
113
ref
237
remove
nil
cons
cons
261
remove
cons
nil
cons
cons
170
ref
subst
238
remove
assume
eqMp
proveHyp
eqMp
nil
148
ref
176
remove
cons
272
remove
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
148
ref
239
remove
cons
149
ref
234
remove
cons
nil
cons
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
eqMp
subst
nil
60
ref
88
ref
287
ref
216
ref
appTerm
299
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
97
ref
subst
88
ref
nil
98
ref
299
remove
nil
cons
cons
nil
cons
nil
cons
cons
101
ref
subst
nil
113
ref
196
remove
nil
cons
300
def
cons
301
def
218
remove
cons
nil
cons
cons
302
def
131
ref
subst
302
remove
178
ref
subst
nil
98
ref
214
ref
nil
cons
303
def
cons
nil
cons
nil
cons
cons
101
ref
subst
nil
301
remove
114
ref
303
remove
cons
304
def
nil
cons
cons
nil
cons
cons
170
ref
subst
88
remove
287
remove
214
ref
appTerm
absTerm
305
def
174
remove
appTerm
306
def
betaConv
86
remove
83
remove
305
ref
appTerm
307
def
absTerm
308
def
87
remove
appTerm
309
def
betaConv
nil
22
remove
93
remove
constTerm
308
ref
appTerm
310
def
axiom
nil
113
ref
310
remove
nil
cons
cons
114
ref
309
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
proveHyp
"A"
72
remove
cons
nil
cons
"P"
82
remove
var
308
remove
nil
cons
cons
"x"
59
remove
var
220
remove
cons
nil
cons
cons
nil
cons
cons
179
ref
subst
eqMp
eqMp
nil
113
ref
307
remove
nil
cons
cons
114
ref
306
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
proveHyp
172
remove
60
remove
305
remove
nil
cons
cons
296
remove
cons
nil
cons
cons
179
ref
subst
eqMp
eqMp
eqMp
eqMp
eqMp
nil
148
ref
300
remove
cons
229
ref
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
eqMp
eqMp
nil
148
ref
212
ref
cons
229
remove
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
nil
113
ref
115
ref
195
ref
appTerm
311
def
216
remove
appTerm
nil
cons
cons
114
ref
81
ref
311
ref
214
remove
appTerm
appTerm
312
def
311
ref
89
ref
appTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
proveHyp
nil
"q'"
1
ref
var
313
def
89
ref
nil
cons
cons
nil
cons
nil
cons
cons
195
ref
refl
nil
113
ref
81
ref
195
ref
appTerm
314
def
195
remove
appTerm
nil
cons
cons
114
ref
115
ref
311
ref
215
remove
313
ref
varTerm
315
def
appTerm
316
def
appTerm
appTerm
312
ref
311
remove
315
ref
appTerm
appTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
proveHyp
nil
"p'"
1
remove
var
317
def
212
remove
cons
nil
cons
nil
cons
cons
313
ref
115
ref
314
remove
317
ref
varTerm
318
def
appTerm
appTerm
115
ref
115
ref
318
ref
appTerm
319
def
316
remove
appTerm
appTerm
312
remove
319
ref
315
ref
appTerm
320
def
appTerm
appTerm
appTerm
absTerm
321
def
315
ref
appTerm
322
def
betaConv
317
ref
282
ref
321
ref
appTerm
323
def
absTerm
324
def
318
ref
appTerm
325
def
betaConv
nil
304
remove
213
remove
nil
cons
cons
nil
cons
cons
nil
291
ref
317
ref
282
ref
313
ref
115
ref
198
remove
318
ref
appTerm
326
def
appTerm
115
ref
319
ref
81
ref
118
ref
appTerm
315
ref
appTerm
327
def
appTerm
328
def
appTerm
120
remove
320
ref
appTerm
329
def
appTerm
330
def
appTerm
331
def
absTerm
332
def
appTerm
333
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
298
ref
subst
317
remove
nil
98
ref
333
remove
nil
cons
cons
nil
cons
nil
cons
cons
101
ref
subst
nil
291
ref
332
remove
nil
cons
cons
nil
cons
nil
cons
cons
298
remove
subst
313
remove
nil
98
ref
331
remove
nil
cons
cons
nil
cons
nil
cons
cons
101
ref
subst
nil
113
ref
326
remove
nil
cons
334
def
cons
335
def
114
ref
330
remove
nil
cons
336
def
cons
nil
cons
cons
nil
cons
cons
337
def
131
ref
subst
337
remove
178
ref
subst
nil
113
ref
328
ref
nil
cons
338
def
cons
114
ref
329
remove
nil
cons
339
def
cons
nil
cons
cons
nil
cons
cons
340
def
131
ref
subst
340
remove
178
ref
subst
nil
242
remove
114
ref
320
ref
nil
cons
341
def
cons
nil
cons
cons
nil
cons
cons
342
def
255
remove
subst
342
ref
131
ref
subst
342
remove
178
ref
subst
nil
113
ref
318
ref
nil
cons
343
def
cons
344
def
114
ref
315
ref
nil
cons
345
def
cons
nil
cons
346
def
cons
nil
cons
cons
347
def
131
ref
subst
347
ref
178
ref
subst
nil
335
ref
114
ref
117
remove
318
remove
appTerm
348
def
nil
cons
349
def
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
nil
113
ref
143
remove
cons
114
ref
343
ref
cons
nil
cons
cons
nil
cons
cons
350
def
209
ref
subst
eqMp
351
def
nil
113
ref
349
ref
cons
352
def
346
ref
cons
nil
cons
cons
353
def
170
ref
subst
proveHyp
nil
335
remove
114
ref
319
remove
116
remove
appTerm
354
def
nil
cons
355
def
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
350
ref
nil
201
remove
245
remove
cons
nil
cons
cons
356
def
131
ref
subst
356
remove
178
ref
subst
249
remove
eqMp
nil
207
remove
252
remove
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
357
def
subst
eqMp
358
def
nil
113
ref
355
ref
cons
359
def
114
ref
115
ref
348
ref
appTerm
360
def
315
ref
appTerm
nil
cons
361
def
cons
nil
cons
cons
nil
cons
cons
362
def
170
ref
subst
proveHyp
362
ref
131
ref
subst
362
remove
178
ref
subst
353
ref
131
ref
subst
353
remove
178
ref
subst
nil
344
ref
250
remove
cons
nil
cons
cons
170
ref
subst
354
remove
assume
eqMp
363
def
350
remove
170
ref
subst
348
remove
assume
eqMp
364
def
363
remove
proveHyp
proveHyp
nil
344
remove
114
ref
327
remove
nil
cons
365
def
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
328
remove
assume
eqMp
366
def
nil
113
ref
365
remove
cons
367
def
114
ref
243
remove
315
ref
appTerm
368
def
nil
cons
369
def
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
proveHyp
nil
246
remove
346
ref
cons
nil
cons
cons
370
def
209
remove
subst
eqMp
371
def
nil
113
ref
369
ref
cons
372
def
346
remove
cons
nil
cons
cons
373
def
170
ref
subst
proveHyp
366
remove
nil
367
remove
114
ref
115
ref
315
ref
appTerm
118
ref
appTerm
374
def
nil
cons
375
def
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
proveHyp
370
ref
357
remove
subst
eqMp
376
def
nil
113
ref
375
ref
cons
377
def
114
ref
115
ref
368
ref
appTerm
378
def
315
remove
appTerm
nil
cons
379
def
cons
nil
cons
cons
nil
cons
cons
380
def
170
ref
subst
proveHyp
380
ref
131
ref
subst
380
remove
178
ref
subst
373
ref
131
ref
subst
373
remove
178
ref
subst
169
remove
370
remove
170
ref
subst
368
remove
assume
eqMp
proveHyp
eqMp
nil
148
ref
369
remove
cons
381
def
149
ref
345
ref
cons
nil
cons
382
def
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
nil
148
ref
375
remove
cons
383
def
149
ref
379
remove
cons
nil
cons
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
eqMp
proveHyp
eqMp
nil
148
ref
349
remove
cons
384
def
382
ref
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
nil
148
ref
355
remove
cons
385
def
149
ref
361
remove
cons
nil
cons
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
148
ref
343
ref
cons
382
remove
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
nil
251
remove
149
ref
341
ref
cons
nil
cons
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
nil
113
ref
115
ref
119
ref
appTerm
320
ref
appTerm
nil
cons
cons
114
ref
115
ref
320
ref
appTerm
119
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
178
ref
subst
proveHyp
nil
113
ref
341
ref
cons
203
remove
cons
nil
cons
cons
386
def
131
ref
subst
386
remove
178
ref
subst
131
ref
178
ref
351
remove
nil
352
remove
247
ref
cons
nil
cons
cons
387
def
170
ref
subst
proveHyp
358
remove
nil
359
remove
114
ref
360
remove
118
ref
appTerm
nil
cons
388
def
cons
nil
cons
cons
nil
cons
cons
389
def
170
ref
subst
proveHyp
389
ref
131
ref
subst
389
remove
178
ref
subst
387
ref
131
ref
subst
387
remove
178
ref
subst
364
remove
371
remove
nil
372
remove
247
ref
cons
nil
cons
cons
390
def
170
ref
subst
proveHyp
376
remove
nil
377
remove
114
ref
378
remove
118
remove
appTerm
nil
cons
391
def
cons
nil
cons
cons
nil
cons
cons
392
def
170
ref
subst
proveHyp
392
ref
131
ref
subst
392
remove
178
ref
subst
390
ref
131
remove
subst
390
remove
178
remove
subst
347
remove
170
ref
subst
320
remove
assume
eqMp
nil
113
ref
345
ref
cons
247
remove
cons
nil
cons
cons
170
ref
subst
374
remove
assume
eqMp
proveHyp
eqMp
nil
381
remove
150
ref
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
nil
383
remove
149
ref
391
remove
cons
nil
cons
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
eqMp
proveHyp
eqMp
nil
384
remove
150
remove
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
nil
385
remove
149
ref
388
remove
cons
nil
cons
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
163
remove
deductAntisym
eqMp
eqMp
nil
148
ref
341
remove
cons
208
remove
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
148
ref
338
remove
cons
149
ref
339
remove
cons
nil
cons
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
nil
148
ref
334
remove
cons
149
ref
336
remove
cons
nil
cons
cons
nil
cons
cons
162
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
subst
nil
113
ref
282
ref
324
ref
appTerm
nil
cons
cons
114
ref
325
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
proveHyp
290
ref
291
ref
324
remove
nil
cons
cons
292
ref
343
remove
cons
nil
cons
cons
nil
cons
cons
179
ref
subst
eqMp
eqMp
nil
113
ref
323
remove
nil
cons
cons
114
ref
322
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
ref
subst
proveHyp
290
ref
291
ref
321
remove
nil
cons
cons
292
ref
345
remove
cons
nil
cons
cons
nil
cons
cons
179
ref
subst
eqMp
eqMp
subst
eqMp
subst
eqMp
228
remove
98
ref
81
remove
115
remove
99
ref
appTerm
89
ref
appTerm
appTerm
89
remove
appTerm
absTerm
393
def
99
ref
appTerm
394
def
betaConv
nil
282
remove
393
ref
appTerm
395
def
axiom
nil
113
remove
395
remove
nil
cons
cons
114
remove
394
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
170
remove
subst
proveHyp
290
remove
291
remove
393
remove
nil
cons
cons
292
remove
99
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
179
remove
subst
eqMp
eqMp
subst
trans
sym
100
remove
eqMp
subst
eqMp
eqMp
eqMp
396
def
nil
148
remove
9
ref
34
ref
19
ref
appTerm
appTerm
19
remove
appTerm
397
def
nil
cons
cons
149
remove
23
ref
24
ref
9
ref
34
ref
27
remove
appTerm
appTerm
25
ref
25
ref
34
ref
26
ref
appTerm
appTerm
398
def
appTerm
appTerm
absTerm
appTerm
399
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
400
def
162
remove
subst
proveHyp
nil
397
remove
thm
396
remove
400
remove
254
remove
subst
proveHyp
nil
399
remove
thm
nil
211
remove
24
remove
9
ref
"Number.Natural.bit1"
"_1935"
7
remove
var
401
def
25
remove
34
remove
401
ref
varTerm
402
def
appTerm
appTerm
403
def
absTerm
404
def
defineConst
405
def
pop
12
remove
constTerm
406
def
26
remove
appTerm
appTerm
398
remove
appTerm
absTerm
407
def
nil
cons
cons
nil
cons
nil
cons
cons
57
remove
97
remove
subst
subst
401
remove
nil
98
remove
9
remove
406
remove
402
ref
appTerm
appTerm
403
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
101
remove
subst
405
remove
402
ref
refl
appThm
404
remove
402
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
23
remove
407
remove
appTerm
thm