6
version
"Data.Bool.!"
const
0
def
"->"
typeOp
1
def
1
ref
"A"
varType
2
def
"bool"
typeOp
nil
opType
3
def
nil
cons
4
def
cons
opType
5
def
4
ref
cons
opType
6
def
constTerm
7
def
refl
8
def
"a'"
2
ref
var
9
def
"Data.Bool.~"
const
1
ref
3
ref
4
ref
cons
opType
10
def
constTerm
11
def
refl
12
def
"="
const
13
def
1
ref
"Data.Option.option"
typeOp
2
ref
nil
cons
14
def
opType
15
def
1
ref
15
ref
4
ref
cons
opType
16
def
nil
cons
17
def
cons
opType
constTerm
18
def
"Data.Option.some"
const
1
ref
2
ref
15
ref
nil
cons
cons
opType
constTerm
19
def
9
ref
varTerm
20
def
appTerm
21
def
appTerm
"Data.Option.none"
const
15
ref
constTerm
22
def
appTerm
assume
sym
18
ref
22
ref
appTerm
23
def
21
ref
appTerm
24
def
assume
25
def
sym
deductAntisym
appThm
absThm
appThm
"Data.Bool.?"
const
26
def
1
ref
1
ref
1
ref
15
ref
"Number.Natural.natural"
typeOp
nil
opType
27
def
nil
cons
28
def
cons
opType
29
def
4
ref
cons
opType
30
def
4
ref
cons
opType
31
def
constTerm
32
def
refl
"fn"
29
ref
var
33
def
"Data.Bool./\\"
const
1
ref
3
ref
10
ref
nil
cons
cons
opType
34
def
constTerm
35
def
13
ref
1
ref
27
ref
1
ref
27
ref
4
ref
cons
opType
36
def
nil
cons
37
def
cons
opType
38
def
constTerm
39
def
33
remove
varTerm
40
def
22
ref
appTerm
appTerm
"Number.Natural.zero"
const
27
ref
constTerm
41
def
appTerm
appTerm
refl
8
ref
"a"
2
ref
var
42
def
39
ref
40
remove
19
ref
42
ref
varTerm
43
def
appTerm
44
def
appTerm
appTerm
refl
42
ref
"Number.Natural.bit1"
const
1
ref
27
ref
28
ref
cons
opType
45
def
constTerm
46
def
41
ref
appTerm
47
def
absTerm
48
def
43
ref
appTerm
betaConv
appThm
absThm
appThm
appThm
absThm
appThm
nil
"f"
1
ref
2
ref
28
ref
cons
opType
var
48
remove
nil
cons
cons
"b"
27
ref
var
41
ref
nil
cons
49
def
cons
nil
cons
cons
nil
cons
cons
"A"
14
ref
cons
50
def
"B"
28
ref
cons
nil
cons
cons
nil
nil
cons
51
def
cons
"f"
1
ref
2
ref
"B"
varType
52
def
nil
cons
53
def
cons
opType
54
def
var
55
def
26
ref
1
ref
1
ref
1
ref
15
ref
53
ref
cons
opType
56
def
4
ref
cons
opType
4
ref
cons
opType
constTerm
"fn"
56
remove
var
57
def
35
ref
13
ref
1
ref
52
ref
1
ref
52
ref
4
ref
cons
opType
58
def
nil
cons
cons
opType
constTerm
59
def
57
remove
varTerm
60
def
22
ref
appTerm
appTerm
"b"
52
ref
var
61
def
varTerm
62
def
appTerm
appTerm
7
ref
42
ref
59
ref
60
remove
44
ref
appTerm
appTerm
55
ref
varTerm
63
def
43
ref
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
appTerm
absTerm
64
def
63
ref
appTerm
65
def
betaConv
61
remove
0
ref
1
ref
1
ref
54
ref
4
ref
cons
opType
66
def
4
ref
cons
opType
constTerm
67
def
64
ref
appTerm
68
def
absTerm
69
def
62
ref
appTerm
70
def
betaConv
nil
0
ref
1
ref
58
ref
4
ref
cons
opType
constTerm
69
ref
appTerm
71
def
axiom
nil
"p"
3
ref
var
72
def
71
remove
nil
cons
cons
"q"
3
ref
var
73
def
70
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
13
ref
34
ref
constTerm
74
def
"Data.Bool.==>"
const
34
ref
constTerm
75
def
72
ref
varTerm
76
def
appTerm
77
def
73
ref
varTerm
78
def
appTerm
79
def
appTerm
refl
72
ref
73
ref
74
ref
35
ref
76
ref
appTerm
80
def
78
ref
appTerm
81
def
appTerm
82
def
76
ref
appTerm
absTerm
83
def
absTerm
84
def
76
ref
appTerm
betaConv
78
ref
refl
85
def
appThm
83
remove
78
ref
appTerm
betaConv
trans
appThm
nil
13
ref
1
ref
34
ref
1
ref
34
ref
4
ref
cons
opType
86
def
nil
cons
cons
opType
constTerm
87
def
75
ref
appTerm
84
remove
appTerm
axiom
76
ref
refl
88
def
appThm
85
ref
appThm
eqMp
89
def
sym
90
def
82
remove
refl
73
ref
13
ref
1
ref
86
ref
1
ref
86
remove
4
ref
cons
opType
nil
cons
cons
opType
constTerm
91
def
"f"
34
ref
var
92
def
92
ref
varTerm
93
def
76
ref
appTerm
78
ref
appTerm
absTerm
94
def
appTerm
92
ref
93
ref
"Data.Bool.T"
const
3
ref
constTerm
95
def
appTerm
95
ref
appTerm
absTerm
96
def
appTerm
absTerm
97
def
78
ref
appTerm
betaConv
appThm
13
ref
1
ref
10
ref
1
ref
10
ref
4
ref
cons
opType
98
def
nil
cons
cons
opType
constTerm
99
def
80
remove
appTerm
refl
72
ref
97
remove
absTerm
100
def
76
ref
appTerm
betaConv
appThm
nil
87
ref
35
ref
appTerm
100
ref
appTerm
axiom
101
def
88
remove
appThm
eqMp
85
ref
appThm
eqMp
102
def
sym
92
ref
93
ref
refl
nil
"t"
3
ref
var
103
def
76
ref
nil
cons
104
def
cons
nil
cons
nil
cons
cons
105
def
74
ref
103
ref
varTerm
106
def
appTerm
107
def
95
ref
appTerm
108
def
assume
sym
nil
95
ref
axiom
109
def
eqMp
106
ref
assume
109
ref
deductAntisym
deductAntisym
110
def
subst
76
ref
assume
111
def
eqMp
appThm
nil
103
ref
78
ref
nil
cons
112
def
cons
nil
cons
nil
cons
cons
113
def
110
ref
subst
78
ref
assume
114
def
eqMp
appThm
absThm
eqMp
115
def
nil
"P"
3
ref
var
116
def
104
ref
cons
"Q"
3
ref
var
117
def
112
ref
cons
nil
cons
118
def
cons
nil
cons
cons
74
ref
refl
119
def
92
ref
93
remove
116
ref
varTerm
120
def
appTerm
121
def
117
ref
varTerm
122
def
appTerm
absTerm
123
def
72
ref
73
ref
76
ref
absTerm
absTerm
124
def
appTerm
betaConv
124
ref
120
ref
appTerm
betaConv
122
ref
refl
125
def
appThm
73
ref
120
ref
absTerm
122
ref
appTerm
betaConv
trans
trans
appThm
96
ref
124
ref
appTerm
betaConv
124
ref
95
ref
appTerm
betaConv
95
ref
refl
126
def
appThm
73
ref
95
ref
absTerm
95
ref
appTerm
betaConv
trans
trans
appThm
74
ref
35
ref
120
ref
appTerm
127
def
122
ref
appTerm
128
def
appTerm
refl
73
ref
91
remove
92
remove
121
remove
78
ref
appTerm
absTerm
appTerm
96
ref
appTerm
absTerm
122
ref
appTerm
betaConv
appThm
99
ref
127
remove
appTerm
refl
100
remove
120
ref
appTerm
betaConv
appThm
101
remove
120
ref
refl
129
def
appThm
eqMp
125
ref
appThm
eqMp
128
remove
assume
eqMp
130
def
124
remove
refl
appThm
eqMp
sym
109
ref
eqMp
131
def
subst
132
def
deductAntisym
eqMp
89
remove
79
ref
assume
eqMp
sym
111
ref
eqMp
119
ref
94
remove
72
ref
73
ref
78
ref
absTerm
133
def
absTerm
134
def
appTerm
betaConv
134
ref
76
ref
appTerm
betaConv
85
remove
appThm
133
ref
78
ref
appTerm
betaConv
trans
trans
appThm
96
remove
134
ref
appTerm
betaConv
134
ref
95
ref
appTerm
betaConv
126
remove
appThm
133
ref
95
ref
appTerm
betaConv
trans
trans
135
def
appThm
102
remove
81
remove
assume
eqMp
134
ref
refl
136
def
appThm
eqMp
sym
109
ref
eqMp
137
def
proveHyp
deductAntisym
138
def
subst
proveHyp
"A"
53
remove
cons
nil
cons
"P"
58
remove
var
69
remove
nil
cons
cons
"x"
52
remove
var
62
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
72
ref
7
ref
"P"
5
ref
var
139
def
varTerm
140
def
appTerm
141
def
nil
cons
142
def
cons
73
ref
140
ref
"x"
2
ref
var
143
def
varTerm
144
def
appTerm
145
def
nil
cons
146
def
cons
nil
cons
cons
nil
cons
cons
147
def
90
ref
subst
147
remove
137
remove
115
remove
deductAntisym
148
def
subst
74
ref
145
ref
appTerm
refl
143
ref
95
ref
absTerm
149
def
144
ref
appTerm
betaConv
appThm
"p"
5
ref
var
150
def
13
ref
1
ref
5
ref
6
ref
nil
cons
cons
opType
constTerm
150
ref
varTerm
151
def
appTerm
149
remove
appTerm
absTerm
152
def
140
ref
appTerm
betaConv
153
def
nil
13
ref
1
ref
6
ref
1
ref
6
ref
4
ref
cons
opType
154
def
nil
cons
cons
opType
constTerm
155
def
7
ref
appTerm
152
remove
appTerm
axiom
140
ref
refl
156
def
appThm
157
def
141
ref
assume
eqMp
eqMp
144
ref
refl
158
def
appThm
eqMp
sym
109
ref
eqMp
eqMp
nil
116
ref
142
remove
cons
117
ref
146
ref
cons
nil
cons
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
159
def
subst
eqMp
eqMp
nil
72
ref
68
remove
nil
cons
cons
73
ref
65
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
"A"
54
ref
nil
cons
cons
nil
cons
160
def
"P"
66
ref
var
161
def
64
remove
nil
cons
cons
"x"
54
ref
var
162
def
63
ref
nil
cons
cons
nil
cons
163
def
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
164
def
subst
subst
eqMp
nil
72
ref
32
remove
"_28100"
29
ref
var
165
def
35
ref
39
ref
165
ref
varTerm
166
def
22
ref
appTerm
appTerm
41
ref
appTerm
167
def
appTerm
7
ref
42
ref
39
ref
166
ref
44
ref
appTerm
appTerm
47
ref
appTerm
absTerm
168
def
appTerm
169
def
appTerm
170
def
absTerm
171
def
appTerm
172
def
nil
cons
cons
73
ref
7
ref
9
ref
11
ref
24
ref
appTerm
173
def
absTerm
174
def
appTerm
175
def
nil
cons
176
def
cons
nil
cons
177
def
cons
nil
cons
cons
138
ref
subst
nil
"P"
30
remove
var
178
def
165
ref
75
ref
171
ref
166
ref
appTerm
179
def
appTerm
175
ref
appTerm
180
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
29
ref
nil
cons
cons
nil
cons
181
def
51
ref
cons
74
ref
141
remove
appTerm
refl
153
remove
appThm
157
remove
eqMp
sym
182
def
subst
subst
165
remove
nil
103
ref
180
remove
nil
cons
cons
nil
cons
nil
cons
cons
110
ref
subst
nil
72
ref
179
ref
nil
cons
183
def
cons
177
ref
cons
nil
cons
cons
184
def
90
ref
subst
184
remove
148
ref
subst
179
ref
betaConv
179
remove
assume
eqMp
nil
72
ref
170
remove
nil
cons
185
def
cons
177
remove
cons
nil
cons
cons
186
def
138
ref
subst
proveHyp
186
ref
90
ref
subst
186
remove
148
ref
subst
nil
139
ref
174
remove
nil
cons
cons
nil
cons
nil
cons
cons
182
ref
subst
9
ref
nil
103
ref
173
remove
nil
cons
cons
nil
cons
nil
cons
cons
110
ref
subst
nil
"a"
3
ref
var
187
def
24
remove
nil
cons
188
def
cons
nil
cons
nil
cons
cons
nil
103
ref
187
remove
varTerm
nil
cons
cons
nil
cons
nil
cons
cons
103
ref
74
ref
75
ref
106
ref
appTerm
"Data.Bool.F"
const
3
ref
constTerm
189
def
appTerm
appTerm
11
ref
106
ref
appTerm
190
def
appTerm
absTerm
191
def
106
ref
appTerm
192
def
betaConv
nil
0
ref
98
remove
constTerm
193
def
191
ref
appTerm
194
def
axiom
nil
72
ref
194
remove
nil
cons
cons
73
ref
192
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
"A"
4
ref
cons
nil
cons
195
def
"P"
10
remove
var
196
def
191
remove
nil
cons
cons
"x"
3
ref
var
197
def
106
ref
nil
cons
198
def
cons
nil
cons
199
def
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
200
def
subst
subst
nil
72
ref
188
ref
cons
73
ref
189
ref
nil
cons
201
def
cons
nil
cons
202
def
cons
nil
cons
cons
203
def
90
ref
subst
203
remove
148
ref
subst
"Number.Natural.suc"
const
45
ref
constTerm
204
def
refl
205
def
nil
"n"
27
ref
var
206
def
49
ref
cons
207
def
nil
cons
nil
cons
cons
208
def
206
ref
39
ref
"Number.Natural.+"
const
1
ref
27
ref
45
ref
nil
cons
cons
opType
constTerm
209
def
41
ref
appTerm
210
def
206
ref
varTerm
211
def
appTerm
appTerm
211
ref
appTerm
absTerm
212
def
211
ref
appTerm
213
def
betaConv
nil
0
ref
1
ref
36
ref
4
ref
cons
opType
214
def
constTerm
215
def
212
ref
appTerm
216
def
axiom
nil
72
ref
216
remove
nil
cons
cons
73
ref
213
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
"A"
28
remove
cons
nil
cons
217
def
"P"
36
ref
var
218
def
212
remove
nil
cons
cons
"x"
27
ref
var
219
def
211
ref
nil
cons
220
def
cons
nil
cons
221
def
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
subst
222
def
appThm
223
def
35
ref
refl
224
def
215
ref
refl
225
def
206
ref
nil
219
ref
204
ref
211
ref
appTerm
226
def
nil
cons
227
def
cons
nil
cons
nil
cons
cons
217
ref
51
ref
cons
228
def
nil
103
ref
13
ref
1
ref
2
ref
5
ref
nil
cons
229
def
cons
opType
constTerm
230
def
144
ref
appTerm
231
def
144
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
110
ref
subst
158
remove
eqMp
232
def
subst
233
def
subst
absThm
appThm
nil
103
ref
95
ref
nil
cons
cons
nil
cons
nil
cons
cons
234
def
228
ref
103
ref
74
ref
7
ref
143
ref
106
ref
absTerm
appTerm
appTerm
106
ref
appTerm
absTerm
235
def
106
ref
appTerm
236
def
betaConv
nil
193
ref
235
ref
appTerm
237
def
axiom
nil
72
ref
237
remove
nil
cons
cons
73
ref
236
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
195
ref
196
ref
235
remove
nil
cons
cons
199
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
subst
subst
238
def
trans
appThm
224
ref
39
ref
204
ref
41
ref
appTerm
239
def
appTerm
240
def
refl
208
remove
206
ref
39
ref
46
remove
211
ref
appTerm
241
def
appTerm
204
ref
"Number.Natural.bit0"
const
45
remove
constTerm
242
def
211
ref
appTerm
243
def
appTerm
244
def
appTerm
absTerm
245
def
211
ref
appTerm
246
def
betaConv
nil
215
ref
245
ref
appTerm
247
def
axiom
nil
72
ref
247
remove
nil
cons
cons
73
ref
246
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
217
ref
218
ref
245
remove
nil
cons
cons
221
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
205
ref
206
ref
39
ref
243
remove
appTerm
209
ref
211
ref
appTerm
248
def
211
ref
appTerm
249
def
appTerm
250
def
absTerm
251
def
211
ref
appTerm
252
def
betaConv
253
def
39
ref
refl
254
def
nil
39
ref
242
ref
41
ref
appTerm
appTerm
255
def
41
ref
appTerm
axiom
appThm
222
remove
appThm
nil
219
ref
49
ref
cons
nil
cons
nil
cons
cons
233
ref
subst
trans
sym
109
ref
eqMp
nil
72
ref
255
remove
210
remove
41
ref
appTerm
appTerm
256
def
nil
cons
cons
73
ref
215
ref
206
ref
75
ref
250
ref
appTerm
39
ref
242
remove
226
ref
appTerm
257
def
appTerm
258
def
209
ref
226
ref
appTerm
226
ref
appTerm
appTerm
259
def
appTerm
260
def
absTerm
261
def
appTerm
262
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
nil
218
ref
261
remove
nil
cons
cons
nil
cons
nil
cons
cons
228
ref
182
ref
subst
subst
206
ref
nil
103
ref
260
remove
nil
cons
cons
nil
cons
nil
cons
cons
110
ref
subst
nil
72
ref
250
ref
nil
cons
263
def
cons
73
ref
259
remove
nil
cons
264
def
cons
nil
cons
cons
nil
cons
cons
265
def
90
ref
subst
265
remove
148
ref
subst
254
ref
206
ref
258
remove
204
ref
244
ref
appTerm
appTerm
absTerm
266
def
211
ref
appTerm
267
def
betaConv
nil
215
ref
266
ref
appTerm
268
def
axiom
nil
72
ref
268
remove
nil
cons
cons
73
ref
267
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
217
ref
218
ref
266
remove
nil
cons
cons
221
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
205
ref
205
ref
250
remove
assume
appThm
appThm
trans
appThm
nil
206
ref
227
remove
cons
269
def
"m"
27
ref
var
270
def
220
ref
cons
nil
cons
271
def
cons
nil
cons
cons
206
ref
39
ref
209
ref
204
ref
270
ref
varTerm
272
def
appTerm
appTerm
211
ref
appTerm
appTerm
204
ref
209
ref
272
ref
appTerm
273
def
211
ref
appTerm
274
def
appTerm
275
def
appTerm
absTerm
276
def
211
ref
appTerm
277
def
betaConv
270
ref
215
ref
276
ref
appTerm
278
def
absTerm
279
def
272
ref
appTerm
280
def
betaConv
nil
215
ref
279
ref
appTerm
281
def
axiom
nil
72
ref
281
remove
nil
cons
cons
73
ref
280
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
217
ref
218
ref
279
remove
nil
cons
cons
219
ref
272
ref
nil
cons
282
def
cons
nil
cons
283
def
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
nil
72
ref
278
remove
nil
cons
cons
73
ref
277
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
217
ref
218
ref
276
remove
nil
cons
cons
221
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
284
def
subst
285
def
205
ref
nil
271
ref
nil
cons
cons
206
ref
39
ref
273
ref
226
ref
appTerm
appTerm
275
ref
appTerm
absTerm
286
def
211
ref
appTerm
287
def
betaConv
270
ref
215
ref
286
ref
appTerm
288
def
absTerm
289
def
272
ref
appTerm
290
def
betaConv
nil
215
ref
289
ref
appTerm
291
def
axiom
nil
72
ref
291
remove
nil
cons
cons
73
ref
290
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
217
ref
218
ref
289
remove
nil
cons
cons
283
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
nil
72
ref
288
remove
nil
cons
cons
73
ref
287
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
217
ref
218
ref
286
remove
nil
cons
cons
221
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
292
def
subst
appThm
293
def
trans
appThm
nil
219
ref
204
ref
204
ref
249
remove
appTerm
294
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
233
ref
subst
295
def
trans
sym
109
ref
eqMp
eqMp
nil
116
ref
263
remove
cons
117
ref
264
remove
cons
nil
cons
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
72
ref
35
ref
256
remove
appTerm
262
remove
appTerm
nil
cons
cons
73
ref
215
ref
251
ref
appTerm
nil
cons
296
def
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
75
ref
refl
297
def
224
ref
251
ref
41
ref
appTerm
betaConv
appThm
225
ref
206
ref
297
ref
253
ref
appThm
251
ref
226
ref
appTerm
betaConv
appThm
absThm
appThm
appThm
appThm
225
ref
206
ref
253
remove
absThm
appThm
appThm
nil
"p"
36
ref
var
298
def
251
remove
nil
cons
299
def
cons
nil
cons
nil
cons
cons
298
ref
75
ref
35
ref
298
remove
varTerm
300
def
41
remove
appTerm
appTerm
215
ref
206
ref
75
ref
300
ref
211
ref
appTerm
301
def
appTerm
300
ref
226
ref
appTerm
appTerm
absTerm
appTerm
appTerm
appTerm
215
ref
206
ref
301
remove
absTerm
appTerm
appTerm
absTerm
302
def
300
ref
appTerm
303
def
betaConv
nil
0
ref
1
ref
214
ref
4
ref
cons
opType
constTerm
302
ref
appTerm
304
def
axiom
nil
72
ref
304
remove
nil
cons
cons
73
ref
303
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
"A"
37
remove
cons
nil
cons
"P"
214
ref
var
302
remove
nil
cons
cons
"x"
36
remove
var
300
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
nil
72
ref
296
remove
cons
73
ref
252
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
217
ref
218
ref
299
remove
cons
221
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
305
def
appThm
306
def
trans
307
def
subst
223
remove
trans
appThm
nil
219
ref
239
remove
nil
cons
cons
nil
cons
nil
cons
cons
233
ref
subst
trans
appThm
224
ref
225
ref
206
ref
254
ref
306
remove
appThm
307
ref
appThm
nil
219
ref
294
remove
nil
cons
cons
nil
cons
nil
cons
cons
233
remove
subst
trans
absThm
appThm
238
ref
trans
appThm
225
ref
206
ref
254
ref
205
ref
307
remove
appThm
appThm
nil
269
remove
nil
cons
nil
cons
cons
305
remove
subst
285
remove
trans
293
remove
trans
appThm
295
remove
trans
absThm
appThm
238
remove
trans
appThm
234
remove
103
ref
74
ref
35
ref
95
ref
appTerm
106
ref
appTerm
appTerm
106
ref
appTerm
absTerm
308
def
106
ref
appTerm
309
def
betaConv
nil
193
ref
308
ref
appTerm
310
def
axiom
nil
72
ref
310
remove
nil
cons
cons
73
ref
309
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
195
ref
196
ref
308
remove
nil
cons
cons
199
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
311
def
subst
312
def
trans
appThm
312
ref
trans
appThm
312
remove
trans
sym
109
ref
eqMp
nil
116
ref
215
ref
206
ref
39
ref
226
ref
appTerm
226
remove
appTerm
absTerm
appTerm
nil
cons
cons
117
ref
35
ref
240
remove
47
ref
appTerm
313
def
appTerm
35
ref
215
ref
206
ref
39
ref
244
remove
appTerm
241
ref
appTerm
absTerm
appTerm
appTerm
215
ref
206
ref
39
ref
204
ref
241
remove
appTerm
appTerm
257
remove
appTerm
absTerm
appTerm
appTerm
314
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
119
ref
123
remove
134
ref
appTerm
betaConv
134
remove
120
ref
appTerm
betaConv
125
ref
appThm
133
remove
122
ref
appTerm
betaConv
trans
trans
appThm
135
remove
appThm
130
remove
136
remove
appThm
eqMp
sym
109
ref
eqMp
315
def
subst
proveHyp
nil
116
ref
313
remove
nil
cons
cons
117
ref
314
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
131
ref
subst
proveHyp
trans
316
def
nil
270
ref
49
remove
cons
207
remove
"p"
27
ref
var
317
def
47
remove
nil
cons
cons
nil
cons
cons
cons
nil
cons
cons
74
ref
"_9294"
27
ref
var
318
def
74
ref
39
ref
211
ref
appTerm
319
def
318
remove
varTerm
appTerm
appTerm
189
ref
appTerm
absTerm
320
def
317
remove
varTerm
321
def
appTerm
322
def
appTerm
refl
320
ref
275
ref
appTerm
betaConv
appThm
119
ref
322
remove
betaConv
appThm
74
ref
319
ref
275
ref
appTerm
323
def
appTerm
189
ref
appTerm
refl
appThm
trans
320
remove
refl
39
ref
275
ref
appTerm
324
def
321
remove
appTerm
assume
sym
appThm
eqMp
sym
nil
103
ref
323
remove
nil
cons
cons
nil
cons
nil
cons
cons
103
ref
74
ref
107
remove
189
ref
appTerm
325
def
appTerm
190
ref
appTerm
absTerm
326
def
106
ref
appTerm
327
def
betaConv
nil
193
ref
326
ref
appTerm
328
def
axiom
nil
72
ref
328
remove
nil
cons
cons
73
ref
327
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
195
ref
196
ref
326
remove
nil
cons
cons
199
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
subst
12
ref
nil
206
ref
275
ref
nil
cons
329
def
cons
271
ref
cons
nil
cons
cons
330
def
206
ref
74
ref
39
ref
272
ref
appTerm
211
ref
appTerm
331
def
appTerm
35
ref
"Number.Natural.<="
const
38
ref
constTerm
332
def
272
ref
appTerm
211
ref
appTerm
333
def
appTerm
332
ref
211
ref
appTerm
334
def
272
ref
appTerm
appTerm
335
def
appTerm
336
def
absTerm
337
def
211
ref
appTerm
338
def
betaConv
270
ref
215
ref
337
ref
appTerm
339
def
absTerm
340
def
272
ref
appTerm
341
def
betaConv
225
ref
270
ref
225
ref
206
ref
336
remove
assume
sym
74
ref
335
remove
appTerm
331
remove
appTerm
342
def
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
nil
215
ref
270
ref
215
ref
206
ref
342
remove
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
72
ref
215
ref
340
ref
appTerm
nil
cons
cons
73
ref
341
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
217
ref
218
ref
340
remove
nil
cons
cons
283
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
nil
72
ref
339
remove
nil
cons
cons
73
ref
338
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
217
ref
218
ref
337
remove
nil
cons
cons
221
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
subst
appThm
nil
"t2"
3
ref
var
343
def
332
remove
275
ref
appTerm
211
ref
appTerm
nil
cons
cons
"t1"
3
ref
var
344
def
334
remove
275
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
343
ref
74
ref
11
ref
35
ref
344
ref
varTerm
345
def
appTerm
343
remove
varTerm
346
def
appTerm
appTerm
appTerm
"Data.Bool.\\/"
const
34
remove
constTerm
347
def
11
ref
345
ref
appTerm
appTerm
11
ref
346
ref
appTerm
appTerm
appTerm
absTerm
348
def
346
ref
appTerm
349
def
betaConv
344
remove
193
ref
348
ref
appTerm
350
def
absTerm
351
def
345
ref
appTerm
352
def
betaConv
nil
193
ref
351
ref
appTerm
353
def
axiom
nil
72
ref
353
remove
nil
cons
cons
73
ref
352
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
195
ref
196
ref
351
remove
nil
cons
cons
197
ref
345
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
nil
72
ref
350
remove
nil
cons
cons
73
ref
349
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
195
ref
196
ref
348
remove
nil
cons
cons
197
ref
346
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
subst
trans
trans
sym
347
ref
refl
330
ref
206
ref
74
ref
11
ref
333
remove
appTerm
appTerm
"Number.Natural.<"
const
38
remove
constTerm
354
def
211
ref
appTerm
272
ref
appTerm
appTerm
absTerm
355
def
211
ref
appTerm
356
def
betaConv
270
ref
215
ref
355
ref
appTerm
357
def
absTerm
358
def
272
ref
appTerm
359
def
betaConv
nil
215
ref
358
ref
appTerm
360
def
axiom
nil
72
ref
360
remove
nil
cons
cons
73
ref
359
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
217
ref
218
ref
358
remove
nil
cons
cons
283
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
nil
72
ref
357
remove
nil
cons
cons
73
ref
356
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
217
ref
218
ref
355
remove
nil
cons
cons
221
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
361
def
subst
nil
270
ref
329
remove
cons
nil
cons
nil
cons
cons
362
def
206
ref
74
ref
354
remove
272
ref
appTerm
211
ref
appTerm
appTerm
26
ref
214
remove
constTerm
363
def
"d"
27
ref
var
364
def
319
ref
273
remove
204
ref
364
ref
varTerm
365
def
appTerm
366
def
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
367
def
211
ref
appTerm
368
def
betaConv
270
ref
215
ref
367
ref
appTerm
369
def
absTerm
370
def
272
ref
appTerm
371
def
betaConv
nil
215
ref
370
ref
appTerm
372
def
axiom
nil
72
ref
372
remove
nil
cons
cons
73
ref
371
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
217
ref
218
ref
370
remove
nil
cons
cons
283
remove
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
nil
72
ref
369
remove
nil
cons
cons
73
ref
368
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
217
ref
218
ref
367
remove
nil
cons
cons
221
remove
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
373
def
subst
trans
363
ref
refl
374
def
364
ref
319
ref
refl
nil
206
ref
366
remove
nil
cons
cons
270
ref
274
ref
nil
cons
375
def
cons
nil
cons
376
def
cons
nil
cons
cons
284
remove
subst
205
ref
nil
206
ref
365
ref
nil
cons
cons
377
def
376
remove
cons
nil
cons
cons
292
ref
subst
appThm
trans
appThm
absThm
appThm
trans
appThm
362
remove
361
remove
subst
330
remove
373
remove
subst
trans
374
remove
364
ref
324
ref
refl
nil
377
remove
271
remove
cons
nil
cons
cons
292
remove
subst
appThm
absThm
appThm
trans
appThm
sym
nil
72
ref
347
ref
363
ref
364
ref
319
remove
204
ref
204
ref
209
ref
274
ref
appTerm
365
ref
appTerm
appTerm
appTerm
appTerm
378
def
absTerm
379
def
appTerm
380
def
appTerm
363
remove
364
ref
324
ref
204
ref
248
ref
365
ref
appTerm
appTerm
appTerm
381
def
absTerm
382
def
appTerm
383
def
appTerm
384
def
nil
cons
cons
nil
cons
nil
cons
cons
74
ref
76
ref
appTerm
385
def
refl
386
def
nil
103
ref
11
ref
76
ref
appTerm
387
def
nil
cons
388
def
cons
nil
cons
nil
cons
cons
200
ref
subst
appThm
sym
386
remove
105
ref
103
ref
74
ref
11
ref
190
ref
appTerm
appTerm
106
ref
appTerm
absTerm
389
def
106
ref
appTerm
390
def
betaConv
nil
193
ref
389
ref
appTerm
391
def
axiom
nil
72
ref
391
remove
nil
cons
cons
73
ref
390
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
195
ref
196
ref
389
remove
nil
cons
cons
199
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
subst
appThm
nil
197
ref
104
ref
cons
nil
cons
392
def
nil
cons
cons
195
ref
51
ref
cons
393
def
232
remove
subst
394
def
subst
trans
sym
109
ref
eqMp
eqMp
subst
sym
nil
72
ref
11
ref
384
remove
appTerm
395
def
nil
cons
396
def
cons
202
ref
cons
nil
cons
cons
397
def
90
ref
subst
397
remove
148
ref
subst
nil
215
ref
270
remove
215
ref
206
ref
39
ref
274
remove
appTerm
248
ref
272
remove
appTerm
398
def
appTerm
399
def
absTerm
appTerm
absTerm
400
def
appTerm
401
def
axiom
nil
72
ref
401
remove
nil
cons
402
def
cons
403
def
202
ref
cons
nil
cons
cons
404
def
138
ref
subst
proveHyp
404
ref
90
ref
subst
404
remove
148
ref
subst
nil
"_2184"
27
ref
var
405
def
220
remove
cons
"_2183"
27
ref
var
406
def
282
ref
cons
nil
cons
cons
nil
cons
cons
206
remove
39
ref
209
remove
406
remove
varTerm
407
def
appTerm
211
remove
appTerm
appTerm
248
ref
407
ref
appTerm
appTerm
absTerm
408
def
405
remove
varTerm
409
def
appTerm
410
def
betaConv
400
ref
407
ref
appTerm
411
def
betaConv
nil
403
remove
73
ref
411
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
217
ref
218
ref
400
remove
nil
cons
cons
219
ref
407
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
nil
72
ref
215
ref
408
ref
appTerm
nil
cons
cons
73
ref
410
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
217
ref
218
ref
408
remove
nil
cons
cons
219
ref
409
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
subst
nil
72
ref
399
remove
nil
cons
cons
73
ref
324
ref
204
ref
398
ref
appTerm
appTerm
nil
cons
412
def
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
nil
"_9301"
27
ref
var
413
def
398
remove
nil
cons
cons
"_9300"
27
ref
var
414
def
375
remove
cons
nil
cons
cons
nil
cons
cons
nil
72
ref
39
ref
414
remove
varTerm
415
def
appTerm
413
remove
varTerm
416
def
appTerm
417
def
nil
cons
418
def
cons
73
ref
39
remove
204
ref
415
remove
appTerm
appTerm
204
ref
416
remove
appTerm
appTerm
nil
cons
419
def
cons
nil
cons
cons
nil
cons
cons
420
def
90
ref
subst
420
remove
148
ref
subst
205
remove
417
remove
assume
appThm
eqMp
nil
116
ref
418
remove
cons
117
ref
419
remove
cons
nil
cons
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
subst
eqMp
nil
72
ref
412
remove
cons
202
remove
cons
nil
cons
cons
138
ref
subst
proveHyp
nil
"_9299"
27
remove
var
421
def
282
remove
cons
nil
cons
nil
cons
cons
nil
72
ref
324
remove
204
remove
248
remove
421
remove
varTerm
422
def
appTerm
appTerm
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
74
ref
387
ref
appTerm
refl
105
remove
200
remove
subst
appThm
nil
197
ref
388
remove
cons
nil
cons
nil
cons
cons
394
ref
subst
trans
sym
109
ref
eqMp
subst
364
ref
11
ref
381
remove
appTerm
absTerm
423
def
422
ref
appTerm
424
def
betaConv
nil
72
ref
380
remove
nil
cons
cons
73
ref
383
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
72
ref
385
ref
189
ref
appTerm
425
def
nil
cons
426
def
cons
73
ref
74
ref
11
ref
347
ref
76
ref
appTerm
78
ref
appTerm
appTerm
appTerm
35
ref
387
remove
appTerm
11
ref
78
ref
appTerm
427
def
appTerm
appTerm
nil
cons
428
def
cons
nil
cons
429
def
cons
nil
cons
cons
430
def
90
ref
subst
430
remove
148
ref
subst
74
ref
"_534"
3
ref
var
431
def
74
ref
11
ref
347
ref
431
remove
varTerm
432
def
appTerm
78
ref
appTerm
appTerm
appTerm
35
ref
11
ref
432
remove
appTerm
appTerm
427
ref
appTerm
appTerm
absTerm
433
def
76
ref
appTerm
434
def
appTerm
refl
435
def
433
ref
189
ref
appTerm
betaConv
appThm
119
ref
434
remove
betaConv
appThm
436
def
74
ref
11
ref
347
ref
189
ref
appTerm
437
def
78
ref
appTerm
appTerm
appTerm
35
ref
11
ref
189
ref
appTerm
438
def
appTerm
427
ref
appTerm
appTerm
refl
appThm
trans
433
remove
refl
439
def
425
remove
assume
appThm
eqMp
sym
119
ref
12
ref
113
ref
103
ref
74
ref
437
remove
106
ref
appTerm
appTerm
106
ref
appTerm
absTerm
440
def
106
ref
appTerm
441
def
betaConv
nil
193
ref
440
ref
appTerm
442
def
axiom
nil
72
ref
442
remove
nil
cons
cons
73
ref
441
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
195
ref
196
ref
440
remove
nil
cons
cons
199
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
subst
appThm
appThm
224
ref
nil
74
ref
438
remove
appTerm
95
ref
appTerm
axiom
443
def
appThm
427
ref
refl
444
def
appThm
nil
103
ref
427
ref
nil
cons
445
def
cons
nil
cons
nil
cons
cons
446
def
311
remove
subst
trans
appThm
nil
197
ref
445
remove
cons
nil
cons
nil
cons
cons
394
remove
subst
trans
sym
109
ref
eqMp
eqMp
eqMp
nil
116
ref
426
ref
cons
117
ref
428
ref
cons
nil
cons
447
def
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
nil
72
ref
385
ref
95
ref
appTerm
448
def
nil
cons
449
def
cons
429
remove
cons
nil
cons
cons
450
def
90
ref
subst
450
remove
148
ref
subst
435
remove
"_532"
3
ref
var
451
def
74
ref
11
ref
347
ref
451
remove
varTerm
452
def
appTerm
78
ref
appTerm
appTerm
appTerm
35
ref
11
ref
452
remove
appTerm
appTerm
427
ref
appTerm
appTerm
absTerm
95
ref
appTerm
betaConv
appThm
436
remove
74
ref
11
ref
347
ref
95
ref
appTerm
453
def
78
ref
appTerm
appTerm
appTerm
35
ref
11
ref
95
ref
appTerm
454
def
appTerm
427
remove
appTerm
appTerm
refl
appThm
trans
439
remove
448
remove
assume
appThm
eqMp
sym
119
ref
12
ref
113
remove
103
ref
74
ref
453
remove
106
ref
appTerm
appTerm
95
remove
appTerm
absTerm
455
def
106
ref
appTerm
456
def
betaConv
nil
193
ref
455
ref
appTerm
457
def
axiom
nil
72
ref
457
remove
nil
cons
cons
73
ref
456
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
195
ref
196
ref
455
remove
nil
cons
cons
199
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
subst
appThm
nil
74
ref
454
remove
appTerm
189
ref
appTerm
axiom
458
def
trans
appThm
224
ref
458
remove
appThm
444
remove
appThm
446
remove
103
ref
74
ref
35
ref
189
ref
appTerm
106
ref
appTerm
appTerm
189
ref
appTerm
absTerm
459
def
106
ref
appTerm
460
def
betaConv
nil
193
ref
459
ref
appTerm
461
def
axiom
nil
72
ref
461
remove
nil
cons
cons
73
ref
460
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
195
ref
196
ref
459
remove
nil
cons
cons
199
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
subst
trans
appThm
nil
103
ref
201
ref
cons
nil
cons
nil
cons
cons
103
ref
74
ref
74
ref
189
remove
appTerm
106
ref
appTerm
appTerm
190
remove
appTerm
absTerm
462
def
106
ref
appTerm
463
def
betaConv
nil
193
ref
462
ref
appTerm
464
def
axiom
nil
72
ref
464
remove
nil
cons
cons
73
ref
463
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
195
ref
196
ref
462
remove
nil
cons
cons
199
remove
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
subst
443
remove
trans
trans
sym
109
remove
eqMp
eqMp
eqMp
nil
116
ref
449
remove
cons
465
def
447
remove
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
103
ref
347
ref
108
remove
appTerm
325
remove
appTerm
absTerm
466
def
76
ref
appTerm
467
def
betaConv
nil
193
ref
466
ref
appTerm
468
def
axiom
nil
72
ref
468
remove
nil
cons
cons
73
ref
467
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
195
ref
196
ref
466
remove
nil
cons
cons
392
remove
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
nil
465
remove
117
ref
426
remove
cons
"R"
3
ref
var
469
def
428
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
72
ref
75
ref
122
ref
appTerm
470
def
469
remove
varTerm
471
def
appTerm
472
def
nil
cons
cons
73
ref
471
ref
nil
cons
473
def
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
nil
72
ref
75
ref
120
ref
appTerm
474
def
471
ref
appTerm
nil
cons
cons
73
ref
75
ref
472
remove
appTerm
471
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
"r"
3
remove
var
475
def
75
ref
474
ref
475
ref
varTerm
476
def
appTerm
appTerm
477
def
75
ref
470
ref
476
ref
appTerm
appTerm
476
ref
appTerm
appTerm
absTerm
478
def
471
remove
appTerm
479
def
betaConv
74
ref
347
ref
120
ref
appTerm
480
def
122
ref
appTerm
481
def
appTerm
refl
73
ref
193
ref
475
ref
477
remove
75
ref
75
ref
78
ref
appTerm
482
def
476
ref
appTerm
appTerm
476
ref
appTerm
483
def
appTerm
absTerm
appTerm
absTerm
122
ref
appTerm
betaConv
appThm
99
remove
480
remove
appTerm
refl
72
ref
73
ref
193
ref
475
remove
75
ref
77
remove
476
remove
appTerm
appTerm
483
remove
appTerm
absTerm
appTerm
absTerm
absTerm
484
def
120
ref
appTerm
betaConv
appThm
nil
87
remove
347
ref
appTerm
484
remove
appTerm
axiom
129
remove
appThm
eqMp
125
remove
appThm
eqMp
485
def
481
remove
assume
eqMp
nil
72
ref
193
ref
478
ref
appTerm
nil
cons
cons
73
ref
479
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
195
ref
196
ref
478
remove
nil
cons
cons
197
ref
473
remove
cons
nil
cons
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
eqMp
eqMp
subst
proveHyp
proveHyp
proveHyp
subst
224
ref
nil
218
ref
379
ref
nil
cons
cons
nil
cons
nil
cons
cons
228
remove
119
remove
12
ref
26
ref
6
ref
constTerm
486
def
refl
nil
"t"
5
ref
var
140
ref
nil
cons
487
def
cons
nil
cons
nil
cons
cons
50
ref
"B"
4
ref
cons
488
def
nil
cons
cons
51
ref
cons
"t"
54
ref
var
489
def
13
remove
1
ref
54
remove
66
remove
nil
cons
cons
opType
constTerm
490
def
489
ref
varTerm
491
def
appTerm
143
ref
491
ref
144
ref
appTerm
absTerm
492
def
appTerm
493
def
absTerm
494
def
491
ref
appTerm
495
def
betaConv
67
ref
refl
489
ref
493
remove
assume
sym
490
remove
492
remove
appTerm
491
ref
appTerm
496
def
assume
sym
deductAntisym
absThm
appThm
nil
67
ref
489
remove
496
remove
absTerm
appTerm
axiom
eqMp
nil
72
ref
67
ref
494
ref
appTerm
nil
cons
cons
73
ref
495
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
160
ref
161
ref
494
remove
nil
cons
cons
162
remove
491
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
subst
subst
appThm
appThm
appThm
7
ref
143
ref
11
ref
145
ref
appTerm
absTerm
appTerm
refl
appThm
sym
nil
150
ref
487
ref
cons
nil
cons
nil
cons
cons
150
ref
74
ref
11
ref
486
ref
143
ref
151
ref
144
ref
appTerm
497
def
absTerm
appTerm
appTerm
appTerm
7
ref
143
ref
11
ref
497
ref
appTerm
absTerm
appTerm
appTerm
absTerm
498
def
151
ref
appTerm
499
def
betaConv
nil
0
ref
154
remove
constTerm
500
def
498
ref
appTerm
501
def
axiom
nil
72
ref
501
remove
nil
cons
cons
73
ref
499
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
"A"
229
remove
cons
nil
cons
502
def
"P"
6
remove
var
503
def
498
remove
nil
cons
cons
"x"
5
ref
var
504
def
151
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
subst
eqMp
subst
505
def
subst
225
ref
364
ref
12
ref
379
remove
365
ref
appTerm
betaConv
appThm
absThm
appThm
trans
appThm
nil
218
ref
382
ref
nil
cons
cons
nil
cons
nil
cons
cons
505
remove
subst
225
remove
364
ref
12
remove
382
remove
365
remove
appTerm
betaConv
appThm
absThm
appThm
trans
appThm
trans
395
remove
assume
eqMp
nil
116
ref
215
ref
364
remove
11
ref
378
remove
appTerm
absTerm
appTerm
nil
cons
cons
117
ref
215
remove
423
ref
appTerm
nil
cons
506
def
cons
nil
cons
cons
nil
cons
cons
315
ref
subst
proveHyp
nil
72
ref
506
remove
cons
73
ref
424
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
217
remove
218
remove
423
remove
nil
cons
cons
219
remove
422
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
eqMp
subst
eqMp
eqMp
nil
116
ref
402
remove
cons
117
ref
201
remove
cons
nil
cons
507
def
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
116
ref
396
remove
cons
507
ref
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
subst
deductAntisym
316
remove
eqMp
254
remove
nil
116
ref
167
remove
nil
cons
cons
117
ref
169
remove
nil
cons
508
def
cons
nil
cons
cons
nil
cons
cons
509
def
131
ref
subst
appThm
nil
42
ref
20
ref
nil
cons
cons
nil
cons
nil
cons
cons
510
def
168
ref
43
ref
appTerm
511
def
betaConv
509
remove
315
ref
subst
nil
72
ref
508
remove
cons
73
ref
511
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
50
ref
nil
cons
512
def
139
ref
168
remove
nil
cons
cons
143
ref
43
ref
nil
cons
cons
nil
cons
513
def
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
subst
appThm
166
remove
refl
25
remove
appThm
eqMp
eqMp
eqMp
nil
116
ref
188
remove
cons
507
remove
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
nil
116
ref
185
remove
cons
117
ref
176
remove
cons
nil
cons
514
def
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
116
ref
183
remove
cons
514
ref
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
72
ref
0
ref
31
remove
constTerm
"x"
29
remove
var
515
def
75
ref
171
ref
515
remove
varTerm
appTerm
appTerm
175
ref
appTerm
absTerm
appTerm
nil
cons
cons
73
ref
75
ref
172
remove
appTerm
175
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
181
remove
178
remove
171
remove
nil
cons
cons
514
remove
cons
nil
cons
cons
nil
72
ref
7
ref
143
ref
75
ref
145
ref
appTerm
516
def
122
ref
appTerm
absTerm
517
def
appTerm
518
def
nil
cons
519
def
cons
520
def
73
ref
75
ref
486
ref
140
ref
appTerm
521
def
appTerm
522
def
122
ref
appTerm
nil
cons
523
def
cons
nil
cons
cons
nil
cons
cons
524
def
90
ref
subst
524
remove
148
ref
subst
nil
72
ref
521
ref
nil
cons
525
def
cons
526
def
73
ref
122
ref
nil
cons
527
def
cons
nil
cons
528
def
cons
nil
cons
cons
529
def
90
ref
subst
529
remove
148
ref
subst
nil
520
ref
528
ref
cons
nil
cons
cons
530
def
138
ref
subst
73
ref
75
ref
7
ref
143
ref
516
remove
78
ref
appTerm
absTerm
531
def
appTerm
532
def
appTerm
78
ref
appTerm
533
def
absTerm
534
def
122
ref
appTerm
535
def
betaConv
nil
526
remove
73
ref
193
ref
534
ref
appTerm
536
def
nil
cons
537
def
cons
nil
cons
538
def
cons
nil
cons
cons
539
def
138
ref
subst
74
ref
521
ref
appTerm
540
def
refl
150
remove
193
remove
73
ref
75
ref
7
ref
143
ref
75
ref
497
remove
appTerm
78
ref
appTerm
absTerm
appTerm
appTerm
78
ref
appTerm
absTerm
appTerm
absTerm
541
def
140
ref
appTerm
betaConv
appThm
nil
155
remove
486
ref
appTerm
541
remove
appTerm
axiom
156
remove
appThm
eqMp
542
def
nil
72
ref
540
remove
536
ref
appTerm
nil
cons
cons
73
ref
522
remove
536
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
539
remove
nil
72
ref
385
remove
78
remove
appTerm
543
def
nil
cons
544
def
cons
73
ref
79
remove
nil
cons
545
def
cons
nil
cons
cons
nil
cons
cons
546
def
90
ref
subst
546
remove
148
ref
subst
90
ref
148
ref
543
remove
assume
547
def
111
remove
eqMp
eqMp
132
remove
deductAntisym
eqMp
548
def
eqMp
nil
116
ref
544
remove
cons
117
ref
545
ref
cons
nil
cons
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
72
ref
537
ref
cons
73
ref
535
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
195
remove
196
ref
534
remove
nil
cons
cons
197
remove
527
ref
cons
nil
cons
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
116
ref
525
remove
cons
117
ref
527
ref
cons
nil
cons
549
def
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
eqMp
nil
116
ref
519
remove
cons
550
def
117
ref
523
remove
cons
nil
cons
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
551
def
subst
eqMp
eqMp
proveHyp
eqMp
nil
7
ref
42
ref
11
remove
18
ref
44
ref
appTerm
552
def
22
ref
appTerm
553
def
appTerm
absTerm
appTerm
thm
22
ref
refl
nil
116
ref
23
ref
22
ref
appTerm
554
def
nil
cons
cons
117
ref
486
ref
42
ref
23
remove
44
ref
appTerm
absTerm
appTerm
555
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
485
remove
sym
556
def
nil
196
ref
103
ref
75
ref
474
remove
106
ref
appTerm
557
def
appTerm
75
ref
470
remove
106
ref
appTerm
558
def
appTerm
106
remove
appTerm
559
def
appTerm
560
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
393
remove
182
ref
subst
561
def
subst
562
def
103
ref
nil
103
ref
560
remove
nil
cons
cons
nil
cons
nil
cons
cons
110
ref
subst
563
def
nil
72
ref
557
ref
nil
cons
564
def
cons
73
ref
559
remove
nil
cons
565
def
cons
nil
cons
cons
nil
cons
cons
566
def
90
ref
subst
567
def
566
remove
148
ref
subst
568
def
nil
72
ref
558
ref
nil
cons
569
def
cons
73
ref
198
ref
cons
nil
cons
570
def
cons
nil
cons
cons
571
def
90
ref
subst
572
def
571
remove
148
ref
subst
573
def
nil
72
ref
120
remove
nil
cons
cons
570
ref
cons
nil
cons
cons
138
ref
subst
557
remove
assume
eqMp
eqMp
nil
116
ref
569
remove
cons
117
ref
198
remove
cons
nil
cons
cons
nil
cons
cons
131
ref
subst
574
def
deductAntisym
eqMp
eqMp
nil
116
ref
564
remove
cons
117
ref
565
remove
cons
nil
cons
cons
nil
cons
cons
131
ref
subst
575
def
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
subst
proveHyp
nil
72
ref
347
ref
554
remove
appTerm
555
remove
appTerm
576
def
nil
cons
cons
73
ref
7
ref
42
ref
347
ref
553
ref
appTerm
486
ref
9
ref
552
ref
21
remove
appTerm
577
def
absTerm
578
def
appTerm
579
def
appTerm
580
def
absTerm
581
def
appTerm
582
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
nil
139
ref
581
remove
nil
cons
cons
nil
cons
nil
cons
cons
182
ref
subst
42
ref
nil
103
ref
580
remove
nil
cons
cons
nil
cons
nil
cons
cons
110
ref
subst
nil
139
ref
9
ref
75
ref
230
ref
20
ref
appTerm
43
ref
appTerm
583
def
appTerm
578
ref
20
ref
appTerm
584
def
appTerm
585
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
182
ref
subst
9
ref
nil
103
ref
585
remove
nil
cons
cons
nil
cons
nil
cons
cons
110
ref
subst
nil
72
ref
583
ref
nil
cons
586
def
cons
73
ref
584
ref
nil
cons
587
def
cons
nil
cons
cons
nil
cons
cons
588
def
90
ref
subst
588
remove
148
ref
subst
584
remove
betaConv
sym
19
ref
refl
589
def
583
remove
assume
appThm
sym
eqMp
eqMp
nil
116
ref
586
remove
cons
117
ref
587
remove
cons
nil
cons
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
72
ref
7
ref
143
ref
75
ref
231
ref
43
ref
appTerm
appTerm
578
ref
144
ref
appTerm
590
def
appTerm
absTerm
appTerm
nil
cons
cons
73
ref
579
ref
nil
cons
591
def
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
"t"
2
ref
var
592
def
75
ref
7
ref
143
ref
75
ref
231
remove
592
ref
varTerm
593
def
appTerm
appTerm
594
def
590
remove
appTerm
absTerm
appTerm
appTerm
579
remove
appTerm
absTerm
595
def
43
ref
appTerm
596
def
betaConv
139
ref
7
ref
592
ref
75
ref
7
ref
143
ref
594
remove
145
ref
appTerm
absTerm
597
def
appTerm
598
def
appTerm
599
def
521
remove
appTerm
absTerm
appTerm
absTerm
600
def
578
ref
appTerm
601
def
betaConv
500
ref
refl
139
ref
8
ref
592
ref
599
ref
refl
542
ref
appThm
absThm
appThm
absThm
appThm
sym
nil
503
ref
139
ref
7
ref
592
ref
599
remove
536
remove
appTerm
602
def
absTerm
603
def
appTerm
604
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
502
ref
51
ref
cons
182
ref
subst
subst
139
ref
nil
103
ref
604
remove
nil
cons
cons
nil
cons
nil
cons
cons
110
ref
subst
nil
139
ref
603
remove
nil
cons
cons
nil
cons
nil
cons
cons
182
ref
subst
592
remove
nil
103
ref
602
remove
nil
cons
cons
nil
cons
nil
cons
cons
110
ref
subst
nil
72
ref
598
remove
nil
cons
605
def
cons
606
def
538
remove
cons
nil
cons
cons
607
def
90
ref
subst
607
remove
148
ref
subst
nil
196
remove
117
ref
75
ref
518
remove
appTerm
122
remove
appTerm
608
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
561
remove
subst
609
def
73
ref
nil
103
ref
533
ref
nil
cons
610
def
cons
nil
cons
nil
cons
cons
110
ref
subst
nil
72
ref
532
remove
nil
cons
611
def
cons
612
def
73
ref
112
ref
cons
nil
cons
613
def
cons
nil
cons
cons
614
def
90
ref
subst
615
def
614
ref
148
ref
subst
616
def
143
ref
145
remove
absTerm
617
def
593
ref
appTerm
betaConv
sym
593
ref
refl
nil
72
ref
230
ref
593
ref
appTerm
593
ref
appTerm
nil
cons
cons
73
ref
140
remove
593
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
nil
143
ref
593
remove
nil
cons
cons
nil
cons
618
def
nil
cons
cons
597
ref
144
ref
appTerm
619
def
betaConv
nil
606
remove
73
ref
619
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
512
ref
139
ref
597
remove
nil
cons
cons
143
ref
144
ref
nil
cons
620
def
cons
nil
cons
621
def
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
512
ref
139
ref
617
ref
nil
cons
cons
622
def
618
remove
cons
nil
cons
cons
542
remove
sym
609
remove
117
ref
nil
103
ref
608
remove
nil
cons
cons
nil
cons
nil
cons
cons
110
ref
subst
530
ref
90
ref
subst
530
remove
148
ref
subst
nil
72
ref
146
ref
cons
623
def
528
remove
cons
nil
cons
cons
138
ref
subst
517
ref
144
ref
appTerm
624
def
betaConv
nil
520
remove
73
ref
624
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
512
ref
139
ref
517
remove
nil
cons
cons
621
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
550
remove
549
remove
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
625
def
subst
proveHyp
nil
72
ref
486
ref
617
ref
appTerm
626
def
nil
cons
627
def
cons
628
def
613
ref
cons
nil
cons
cons
629
def
138
ref
subst
proveHyp
629
ref
90
ref
subst
629
remove
148
ref
subst
614
remove
138
ref
subst
nil
628
remove
73
ref
610
ref
cons
nil
cons
630
def
cons
nil
cons
cons
138
ref
subst
nil
139
ref
143
ref
75
ref
617
remove
144
ref
appTerm
631
def
appTerm
533
ref
appTerm
632
def
absTerm
633
def
nil
cons
cons
nil
cons
nil
cons
cons
182
ref
subst
143
ref
nil
103
ref
632
remove
nil
cons
cons
nil
cons
nil
cons
cons
110
ref
subst
nil
72
ref
631
ref
nil
cons
634
def
cons
630
ref
cons
nil
cons
cons
635
def
90
ref
subst
635
remove
148
ref
subst
nil
"f"
5
remove
var
487
remove
cons
"y"
2
ref
var
636
def
620
remove
cons
nil
cons
cons
nil
cons
cons
488
remove
512
ref
cons
51
ref
cons
636
ref
59
remove
143
ref
63
ref
144
ref
appTerm
absTerm
636
remove
varTerm
637
def
appTerm
appTerm
63
ref
637
ref
appTerm
appTerm
absTerm
638
def
637
ref
appTerm
639
def
betaConv
55
remove
7
ref
638
ref
appTerm
640
def
absTerm
641
def
63
remove
appTerm
642
def
betaConv
nil
67
remove
641
ref
appTerm
643
def
axiom
nil
72
ref
643
remove
nil
cons
cons
73
ref
642
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
160
remove
161
remove
641
remove
nil
cons
cons
163
remove
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
nil
72
ref
640
remove
nil
cons
cons
73
ref
639
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
512
ref
139
ref
638
remove
nil
cons
cons
143
remove
637
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
subst
subst
631
remove
assume
eqMp
nil
623
ref
630
remove
cons
nil
cons
cons
644
def
138
ref
subst
proveHyp
644
ref
90
ref
subst
644
remove
148
ref
subst
615
remove
616
remove
nil
623
remove
613
ref
cons
nil
cons
cons
138
ref
subst
531
ref
144
remove
appTerm
645
def
betaConv
nil
612
remove
73
ref
645
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
512
ref
139
ref
531
remove
nil
cons
cons
621
remove
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
116
ref
611
remove
cons
118
ref
cons
nil
cons
cons
131
ref
subst
646
def
deductAntisym
eqMp
eqMp
nil
116
ref
146
remove
cons
117
ref
610
remove
cons
nil
cons
647
def
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
116
ref
634
remove
cons
647
ref
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
72
ref
7
ref
633
remove
appTerm
nil
cons
cons
73
ref
75
ref
626
remove
appTerm
533
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
512
ref
622
remove
647
remove
cons
nil
cons
cons
551
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
116
ref
627
remove
cons
118
ref
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
eqMp
eqMp
646
remove
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
116
ref
605
remove
cons
117
ref
537
remove
cons
nil
cons
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
72
ref
500
remove
600
ref
appTerm
nil
cons
cons
73
ref
601
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
502
remove
503
remove
600
remove
nil
cons
cons
504
remove
578
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
nil
72
ref
7
ref
595
ref
appTerm
nil
cons
cons
73
ref
596
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
512
ref
139
ref
595
remove
nil
cons
cons
513
ref
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
eqMp
nil
116
ref
553
remove
nil
cons
cons
117
ref
591
remove
cons
nil
cons
cons
nil
cons
cons
556
remove
562
remove
103
ref
563
remove
567
remove
568
remove
572
remove
573
remove
nil
72
ref
527
remove
cons
570
remove
cons
nil
cons
cons
138
ref
subst
558
remove
assume
eqMp
eqMp
574
remove
deductAntisym
eqMp
eqMp
575
remove
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
subst
proveHyp
eqMp
absThm
eqMp
eqMp
nil
72
ref
35
ref
576
remove
appTerm
582
remove
appTerm
nil
cons
cons
73
ref
0
ref
1
ref
16
ref
4
ref
cons
opType
648
def
constTerm
649
def
"x"
15
ref
var
650
def
347
remove
18
remove
650
ref
varTerm
651
def
appTerm
652
def
22
ref
appTerm
appTerm
486
remove
42
ref
652
remove
44
ref
appTerm
absTerm
appTerm
appTerm
absTerm
653
def
appTerm
654
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
297
remove
224
remove
653
ref
22
ref
appTerm
betaConv
appThm
8
ref
42
ref
653
ref
44
ref
appTerm
betaConv
absThm
appThm
appThm
appThm
649
ref
refl
650
ref
653
ref
651
ref
appTerm
betaConv
absThm
appThm
appThm
nil
"p"
16
ref
var
655
def
653
remove
nil
cons
cons
nil
cons
nil
cons
cons
655
ref
75
ref
35
ref
655
remove
varTerm
656
def
22
ref
appTerm
appTerm
7
ref
42
ref
656
ref
44
ref
appTerm
absTerm
appTerm
appTerm
appTerm
649
remove
650
remove
656
ref
651
remove
appTerm
absTerm
appTerm
appTerm
absTerm
657
def
656
ref
appTerm
658
def
betaConv
nil
0
ref
1
ref
648
ref
4
ref
cons
opType
constTerm
657
ref
appTerm
659
def
axiom
nil
72
ref
659
remove
nil
cons
cons
73
ref
658
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
"A"
17
remove
cons
nil
cons
"P"
648
remove
var
657
remove
nil
cons
cons
"x"
16
remove
var
656
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
159
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
nil
654
remove
thm
26
remove
1
ref
1
ref
1
ref
15
remove
14
ref
cons
opType
660
def
4
ref
cons
opType
661
def
4
remove
cons
opType
662
def
constTerm
663
def
refl
"fn"
660
ref
var
664
def
35
ref
230
ref
664
remove
varTerm
665
def
22
ref
appTerm
appTerm
"b"
2
ref
var
666
def
varTerm
667
def
appTerm
appTerm
refl
8
remove
42
ref
230
ref
665
remove
44
ref
appTerm
appTerm
refl
42
ref
43
ref
absTerm
668
def
43
ref
appTerm
betaConv
appThm
absThm
appThm
appThm
absThm
appThm
nil
"f"
1
remove
2
remove
14
ref
cons
opType
var
668
remove
nil
cons
cons
nil
cons
nil
cons
cons
50
remove
"B"
14
remove
cons
nil
cons
cons
51
ref
cons
164
remove
subst
subst
eqMp
nil
72
ref
663
ref
"_28102"
660
ref
var
669
def
35
remove
230
ref
669
ref
varTerm
670
def
22
remove
appTerm
appTerm
667
ref
appTerm
671
def
appTerm
7
ref
42
ref
230
ref
670
ref
44
remove
appTerm
appTerm
43
ref
appTerm
absTerm
672
def
appTerm
673
def
appTerm
674
def
absTerm
675
def
appTerm
676
def
nil
cons
cons
73
ref
663
remove
669
ref
673
ref
absTerm
677
def
appTerm
678
def
nil
cons
679
def
cons
nil
cons
680
def
cons
nil
cons
cons
138
ref
subst
nil
"P"
661
remove
var
681
def
669
ref
75
ref
675
ref
670
ref
appTerm
682
def
appTerm
678
ref
appTerm
683
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
660
ref
nil
cons
cons
nil
cons
684
def
51
remove
cons
182
ref
subst
685
def
subst
669
ref
nil
103
ref
683
remove
nil
cons
cons
nil
cons
nil
cons
cons
110
ref
subst
nil
72
ref
682
ref
nil
cons
686
def
cons
680
ref
cons
nil
cons
cons
687
def
90
ref
subst
687
remove
148
ref
subst
682
ref
betaConv
682
remove
assume
eqMp
nil
72
ref
674
remove
nil
cons
688
def
cons
680
remove
cons
nil
cons
cons
689
def
138
ref
subst
proveHyp
689
ref
90
ref
subst
689
remove
148
ref
subst
677
ref
670
ref
appTerm
690
def
betaConv
691
def
sym
nil
116
ref
671
remove
nil
cons
cons
117
ref
673
remove
nil
cons
692
def
cons
nil
cons
cons
nil
cons
cons
315
ref
subst
eqMp
684
ref
681
ref
677
ref
nil
cons
cons
693
def
"x"
660
remove
var
694
def
670
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
625
remove
subst
proveHyp
eqMp
nil
116
ref
688
remove
cons
117
ref
679
ref
cons
nil
cons
695
def
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
116
ref
686
remove
cons
695
ref
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
72
ref
0
remove
662
remove
constTerm
696
def
694
ref
75
ref
675
ref
694
ref
varTerm
697
def
appTerm
appTerm
678
ref
appTerm
absTerm
appTerm
nil
cons
cons
73
ref
75
ref
676
remove
appTerm
678
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
proveHyp
684
ref
681
ref
675
remove
nil
cons
cons
695
remove
cons
nil
cons
cons
551
ref
subst
eqMp
eqMp
proveHyp
nil
72
ref
679
remove
cons
73
ref
7
ref
42
ref
7
ref
9
ref
74
ref
577
ref
appTerm
230
remove
43
ref
appTerm
698
def
20
remove
appTerm
699
def
appTerm
700
def
absTerm
appTerm
absTerm
appTerm
701
def
nil
cons
702
def
cons
nil
cons
703
def
cons
nil
cons
cons
138
ref
subst
nil
681
remove
669
ref
75
ref
690
ref
appTerm
701
ref
appTerm
704
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
685
remove
subst
669
remove
nil
103
ref
704
remove
nil
cons
cons
nil
cons
nil
cons
cons
110
ref
subst
nil
72
ref
690
ref
nil
cons
705
def
cons
703
ref
cons
nil
cons
cons
706
def
90
ref
subst
706
remove
148
ref
subst
691
remove
690
remove
assume
eqMp
nil
72
ref
692
ref
cons
707
def
703
remove
cons
nil
cons
cons
708
def
138
ref
subst
proveHyp
708
ref
90
ref
subst
708
remove
148
ref
subst
nil
139
ref
42
ref
7
ref
666
remove
74
remove
552
remove
19
remove
667
ref
appTerm
appTerm
appTerm
698
remove
667
remove
appTerm
appTerm
absTerm
709
def
appTerm
710
def
absTerm
711
def
nil
cons
cons
nil
cons
nil
cons
cons
182
ref
subst
42
remove
nil
103
ref
710
remove
nil
cons
cons
nil
cons
nil
cons
cons
110
ref
subst
nil
139
ref
709
remove
nil
cons
cons
nil
cons
nil
cons
cons
182
remove
subst
9
remove
nil
103
remove
700
remove
nil
cons
cons
nil
cons
nil
cons
cons
110
remove
subst
nil
72
ref
577
ref
nil
cons
712
def
cons
73
ref
699
ref
nil
cons
713
def
cons
nil
cons
cons
nil
cons
cons
714
def
548
remove
nil
72
ref
545
ref
cons
73
ref
482
ref
76
remove
appTerm
nil
cons
715
def
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
482
remove
refl
547
remove
appThm
sym
nil
72
ref
112
ref
cons
716
def
613
remove
cons
nil
cons
cons
717
def
90
ref
subst
717
remove
148
ref
subst
114
remove
eqMp
nil
116
ref
112
remove
cons
118
remove
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
716
remove
73
ref
104
remove
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
nil
116
ref
545
remove
cons
117
ref
715
remove
cons
nil
cons
cons
nil
cons
cons
718
def
315
remove
subst
eqMp
138
ref
718
remove
131
ref
subst
eqMp
deductAntisym
deductAntisym
subst
714
ref
90
ref
subst
714
remove
148
ref
subst
672
ref
43
remove
appTerm
719
def
betaConv
nil
707
remove
73
ref
719
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
ref
subst
512
remove
139
remove
672
remove
nil
cons
cons
513
remove
cons
nil
cons
cons
159
remove
subst
eqMp
eqMp
720
def
sym
670
remove
refl
577
ref
assume
appThm
trans
510
remove
720
remove
subst
trans
eqMp
nil
116
ref
712
ref
cons
117
ref
713
ref
cons
nil
cons
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
nil
72
ref
75
ref
577
ref
appTerm
699
ref
appTerm
nil
cons
cons
73
ref
75
ref
699
ref
appTerm
577
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
nil
72
ref
713
ref
cons
73
ref
712
ref
cons
nil
cons
cons
nil
cons
cons
721
def
90
remove
subst
721
remove
148
remove
subst
589
remove
699
remove
assume
appThm
eqMp
nil
116
ref
713
remove
cons
117
ref
712
remove
cons
nil
cons
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
116
ref
692
remove
cons
117
remove
702
remove
cons
nil
cons
722
def
cons
nil
cons
cons
131
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
116
remove
705
remove
cons
722
ref
cons
nil
cons
cons
131
remove
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
72
remove
696
remove
694
remove
75
ref
677
remove
697
remove
appTerm
appTerm
701
ref
appTerm
absTerm
appTerm
nil
cons
cons
73
remove
75
remove
678
remove
appTerm
701
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
138
remove
subst
proveHyp
684
remove
693
remove
722
remove
cons
nil
cons
cons
551
remove
subst
eqMp
eqMp
proveHyp
nil
7
remove
711
remove
appTerm
thm