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
"x"
2
ref
var
9
def
"="
const
10
def
1
ref
2
ref
5
ref
nil
cons
11
def
cons
opType
constTerm
12
def
refl
13
def
nil
"t"
"Data.List.list"
typeOp
14
def
2
ref
nil
cons
15
def
opType
16
def
var
17
def
"Data.List.[]"
const
18
def
16
ref
constTerm
19
def
nil
cons
20
def
cons
21
def
"h"
2
ref
var
22
def
9
ref
varTerm
23
def
nil
cons
24
def
cons
nil
cons
cons
nil
cons
cons
17
ref
12
ref
"Data.List.last"
const
25
def
1
ref
16
ref
15
ref
cons
opType
26
def
constTerm
27
def
"Data.List.::"
const
1
ref
2
ref
1
ref
16
ref
16
ref
nil
cons
28
def
cons
opType
29
def
nil
cons
30
def
cons
opType
constTerm
31
def
22
ref
varTerm
32
def
appTerm
33
def
17
ref
varTerm
34
def
appTerm
35
def
appTerm
36
def
appTerm
"Data.Bool.cond"
const
1
ref
3
ref
1
ref
2
ref
1
ref
2
ref
15
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
37
def
"Data.List.null"
const
1
ref
16
ref
4
ref
cons
opType
38
def
constTerm
39
def
34
ref
appTerm
appTerm
40
def
32
ref
appTerm
27
ref
34
ref
appTerm
41
def
appTerm
42
def
appTerm
absTerm
43
def
34
ref
appTerm
44
def
betaConv
22
ref
0
ref
1
ref
38
ref
4
ref
cons
opType
45
def
constTerm
46
def
43
ref
appTerm
47
def
absTerm
48
def
32
ref
appTerm
49
def
betaConv
nil
7
ref
48
ref
appTerm
50
def
axiom
nil
"p"
3
ref
var
51
def
50
remove
nil
cons
cons
"q"
3
ref
var
52
def
49
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
10
ref
1
ref
3
ref
1
ref
3
ref
4
ref
cons
opType
53
def
nil
cons
cons
opType
54
def
constTerm
55
def
"Data.Bool.==>"
const
54
ref
constTerm
56
def
51
ref
varTerm
57
def
appTerm
58
def
52
ref
varTerm
59
def
appTerm
60
def
appTerm
61
def
refl
51
ref
52
ref
55
ref
"Data.Bool./\\"
const
54
ref
constTerm
62
def
57
ref
appTerm
63
def
59
ref
appTerm
64
def
appTerm
65
def
57
ref
appTerm
absTerm
66
def
absTerm
67
def
57
ref
appTerm
betaConv
59
ref
refl
68
def
appThm
66
remove
59
ref
appTerm
betaConv
trans
appThm
nil
10
ref
1
ref
54
ref
1
ref
54
ref
4
ref
cons
opType
69
def
nil
cons
cons
opType
constTerm
70
def
56
ref
appTerm
67
remove
appTerm
axiom
57
ref
refl
71
def
appThm
68
ref
appThm
eqMp
72
def
sym
73
def
65
remove
refl
52
ref
10
ref
1
ref
69
ref
1
ref
69
remove
4
ref
cons
opType
nil
cons
cons
opType
constTerm
74
def
"f"
54
ref
var
75
def
75
ref
varTerm
76
def
57
ref
appTerm
59
ref
appTerm
absTerm
77
def
appTerm
75
ref
76
ref
"Data.Bool.T"
const
3
ref
constTerm
78
def
appTerm
78
ref
appTerm
absTerm
79
def
appTerm
absTerm
80
def
59
ref
appTerm
betaConv
appThm
10
ref
1
ref
53
ref
1
ref
53
ref
4
ref
cons
opType
81
def
nil
cons
cons
opType
constTerm
82
def
63
ref
appTerm
refl
51
ref
80
remove
absTerm
83
def
57
ref
appTerm
betaConv
appThm
nil
70
ref
62
ref
appTerm
83
ref
appTerm
axiom
84
def
71
remove
appThm
eqMp
68
ref
appThm
eqMp
85
def
sym
75
ref
76
ref
refl
nil
"t"
3
ref
var
86
def
57
ref
nil
cons
87
def
cons
nil
cons
nil
cons
cons
88
def
55
ref
86
ref
varTerm
89
def
appTerm
90
def
78
ref
appTerm
91
def
assume
sym
nil
78
ref
axiom
92
def
eqMp
89
ref
assume
92
ref
deductAntisym
deductAntisym
93
def
subst
57
ref
assume
94
def
eqMp
appThm
nil
86
ref
59
ref
nil
cons
95
def
cons
nil
cons
nil
cons
cons
96
def
93
ref
subst
59
ref
assume
97
def
eqMp
appThm
absThm
eqMp
98
def
nil
"P"
3
ref
var
99
def
87
ref
cons
"Q"
3
ref
var
100
def
95
ref
cons
nil
cons
101
def
cons
nil
cons
cons
55
ref
refl
102
def
75
ref
76
remove
99
ref
varTerm
103
def
appTerm
104
def
100
ref
varTerm
105
def
appTerm
absTerm
106
def
51
ref
52
ref
57
ref
absTerm
absTerm
107
def
appTerm
betaConv
107
ref
103
ref
appTerm
betaConv
105
ref
refl
108
def
appThm
52
ref
103
ref
absTerm
105
ref
appTerm
betaConv
trans
trans
appThm
79
ref
107
ref
appTerm
betaConv
107
ref
78
ref
appTerm
betaConv
78
ref
refl
109
def
appThm
52
ref
78
ref
absTerm
78
ref
appTerm
betaConv
trans
trans
appThm
55
ref
62
ref
103
ref
appTerm
110
def
105
ref
appTerm
111
def
appTerm
refl
52
ref
74
remove
75
remove
104
remove
59
ref
appTerm
absTerm
appTerm
79
ref
appTerm
absTerm
105
ref
appTerm
betaConv
appThm
82
ref
110
remove
appTerm
refl
83
remove
103
ref
appTerm
betaConv
appThm
84
remove
103
ref
refl
112
def
appThm
eqMp
108
ref
appThm
eqMp
111
remove
assume
eqMp
113
def
107
remove
refl
appThm
eqMp
sym
92
ref
eqMp
114
def
subst
deductAntisym
eqMp
72
remove
60
ref
assume
eqMp
sym
94
remove
eqMp
102
ref
77
remove
51
ref
52
ref
59
ref
absTerm
115
def
absTerm
116
def
appTerm
betaConv
116
ref
57
ref
appTerm
betaConv
68
ref
appThm
115
ref
59
ref
appTerm
betaConv
trans
trans
appThm
79
remove
116
ref
appTerm
betaConv
116
ref
78
ref
appTerm
betaConv
109
remove
appThm
115
ref
78
ref
appTerm
betaConv
trans
trans
117
def
appThm
85
remove
64
remove
assume
eqMp
116
ref
refl
118
def
appThm
eqMp
sym
92
ref
eqMp
119
def
proveHyp
deductAntisym
120
def
subst
proveHyp
"A"
15
remove
cons
121
def
nil
cons
122
def
"P"
5
ref
var
123
def
48
remove
nil
cons
cons
9
ref
32
ref
nil
cons
cons
nil
cons
124
def
cons
nil
cons
cons
nil
51
ref
7
ref
123
ref
varTerm
125
def
appTerm
126
def
nil
cons
127
def
cons
52
ref
125
ref
23
ref
appTerm
128
def
nil
cons
129
def
cons
nil
cons
cons
nil
cons
cons
130
def
73
ref
subst
130
remove
119
remove
98
remove
deductAntisym
131
def
subst
55
ref
128
ref
appTerm
refl
9
ref
78
ref
absTerm
132
def
23
ref
appTerm
betaConv
appThm
"p"
5
ref
var
133
def
10
ref
1
ref
5
ref
6
ref
nil
cons
cons
opType
constTerm
133
ref
varTerm
134
def
appTerm
132
remove
appTerm
absTerm
135
def
125
ref
appTerm
betaConv
136
def
nil
10
ref
1
ref
6
ref
1
ref
6
ref
4
ref
cons
opType
137
def
nil
cons
cons
opType
constTerm
138
def
7
ref
appTerm
135
remove
appTerm
axiom
125
ref
refl
139
def
appThm
140
def
126
ref
assume
eqMp
eqMp
23
ref
refl
141
def
appThm
eqMp
sym
92
ref
eqMp
eqMp
nil
99
ref
127
remove
cons
100
ref
129
remove
cons
nil
cons
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
142
def
subst
eqMp
eqMp
nil
51
ref
47
remove
nil
cons
cons
52
ref
44
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
"A"
28
ref
cons
nil
cons
143
def
"P"
38
ref
var
144
def
43
remove
nil
cons
cons
"x"
16
ref
var
145
def
34
ref
nil
cons
cons
nil
cons
146
def
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
147
def
subst
37
ref
refl
148
def
nil
86
ref
39
ref
19
ref
appTerm
149
def
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
nil
149
ref
axiom
eqMp
appThm
150
def
141
ref
appThm
27
ref
19
ref
appTerm
151
def
refl
152
def
appThm
nil
"t2"
2
ref
var
153
def
151
ref
nil
cons
cons
154
def
"t1"
2
ref
var
155
def
24
remove
cons
nil
cons
cons
nil
cons
cons
153
ref
12
ref
37
ref
78
ref
appTerm
155
ref
varTerm
156
def
appTerm
153
ref
varTerm
157
def
appTerm
appTerm
156
ref
appTerm
absTerm
158
def
157
ref
appTerm
159
def
betaConv
155
ref
7
ref
158
ref
appTerm
160
def
absTerm
161
def
156
ref
appTerm
162
def
betaConv
nil
7
ref
161
ref
appTerm
163
def
axiom
nil
51
ref
163
remove
nil
cons
cons
52
ref
162
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
122
ref
123
ref
161
remove
nil
cons
cons
9
ref
156
ref
nil
cons
cons
nil
cons
164
def
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
nil
51
ref
160
remove
nil
cons
cons
52
ref
159
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
122
ref
123
ref
158
remove
nil
cons
cons
9
ref
157
ref
nil
cons
cons
nil
cons
165
def
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
166
def
subst
trans
trans
167
def
appThm
141
ref
appThm
nil
86
ref
12
ref
23
ref
appTerm
168
def
23
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
141
remove
eqMp
169
def
trans
absThm
appThm
nil
86
ref
78
ref
nil
cons
cons
nil
cons
nil
cons
cons
170
def
86
ref
55
ref
7
ref
9
ref
89
ref
absTerm
appTerm
appTerm
89
ref
appTerm
absTerm
171
def
89
ref
appTerm
172
def
betaConv
nil
0
ref
81
remove
constTerm
173
def
171
ref
appTerm
174
def
axiom
nil
51
ref
174
remove
nil
cons
cons
52
ref
172
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
"A"
4
ref
cons
nil
cons
175
def
"P"
53
ref
var
176
def
171
remove
nil
cons
cons
"x"
3
ref
var
177
def
89
ref
nil
cons
cons
nil
cons
178
def
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
179
def
subst
180
def
trans
sym
92
ref
eqMp
nil
7
ref
9
ref
12
ref
27
ref
31
ref
23
ref
appTerm
19
ref
appTerm
appTerm
appTerm
23
ref
appTerm
absTerm
appTerm
thm
nil
51
ref
46
ref
"l"
16
ref
var
181
def
56
ref
"Data.Bool.~"
const
53
remove
constTerm
182
def
10
ref
1
ref
16
ref
38
ref
nil
cons
183
def
cons
opType
constTerm
184
def
181
ref
varTerm
185
def
appTerm
19
ref
appTerm
186
def
appTerm
187
def
appTerm
188
def
12
ref
"Data.List.head"
const
189
def
26
remove
constTerm
190
def
"Data.List.reverse"
const
191
def
29
remove
constTerm
192
def
185
ref
appTerm
193
def
appTerm
194
def
appTerm
27
ref
185
ref
appTerm
195
def
appTerm
196
def
appTerm
absTerm
197
def
appTerm
198
def
nil
cons
cons
nil
cons
nil
cons
cons
55
ref
57
ref
appTerm
199
def
refl
200
def
nil
86
ref
182
ref
57
ref
appTerm
201
def
nil
cons
202
def
cons
nil
cons
nil
cons
cons
86
ref
55
ref
56
ref
89
ref
appTerm
203
def
"Data.Bool.F"
const
3
ref
constTerm
204
def
appTerm
appTerm
182
ref
89
ref
appTerm
205
def
appTerm
absTerm
206
def
89
ref
appTerm
207
def
betaConv
nil
173
ref
206
ref
appTerm
208
def
axiom
nil
51
ref
208
remove
nil
cons
cons
52
ref
207
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
206
remove
nil
cons
cons
178
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
209
def
subst
appThm
sym
200
remove
88
ref
86
ref
55
ref
182
ref
205
ref
appTerm
appTerm
89
ref
appTerm
absTerm
210
def
89
ref
appTerm
211
def
betaConv
nil
173
ref
210
ref
appTerm
212
def
axiom
nil
51
ref
212
remove
nil
cons
cons
52
ref
211
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
210
remove
nil
cons
cons
178
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
213
def
subst
214
def
appThm
nil
177
ref
87
ref
cons
nil
cons
215
def
nil
cons
cons
175
ref
nil
nil
cons
216
def
cons
169
ref
subst
217
def
subst
trans
sym
92
ref
eqMp
eqMp
subst
sym
nil
51
ref
182
ref
198
ref
appTerm
218
def
nil
cons
219
def
cons
220
def
52
ref
204
ref
nil
cons
221
def
cons
nil
cons
222
def
cons
nil
cons
cons
223
def
73
ref
subst
223
remove
131
ref
subst
143
ref
216
ref
cons
224
def
56
ref
refl
225
def
182
ref
refl
226
def
nil
145
ref
20
remove
cons
nil
cons
nil
cons
cons
224
ref
169
ref
subst
subst
appThm
nil
55
ref
182
ref
78
ref
appTerm
227
def
appTerm
204
ref
appTerm
axiom
228
def
trans
appThm
13
ref
27
ref
refl
229
def
nil
184
ref
192
ref
19
ref
appTerm
230
def
appTerm
19
ref
appTerm
axiom
appThm
appThm
190
ref
19
ref
appTerm
231
def
refl
appThm
appThm
nil
86
ref
12
ref
151
ref
appTerm
231
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
86
ref
55
ref
56
ref
204
ref
appTerm
232
def
89
ref
appTerm
appTerm
78
ref
appTerm
absTerm
233
def
89
ref
appTerm
234
def
betaConv
nil
173
ref
233
ref
appTerm
235
def
axiom
nil
51
ref
235
remove
nil
cons
cons
52
ref
234
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
233
remove
nil
cons
cons
178
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
236
def
subst
trans
sym
92
ref
eqMp
nil
51
ref
56
ref
182
ref
184
ref
19
ref
appTerm
19
ref
appTerm
appTerm
appTerm
12
ref
27
ref
230
remove
appTerm
appTerm
231
remove
appTerm
appTerm
237
def
nil
cons
cons
52
ref
7
ref
22
ref
46
ref
17
ref
56
ref
56
ref
182
ref
184
ref
34
ref
appTerm
19
ref
appTerm
appTerm
appTerm
12
ref
27
ref
192
ref
34
ref
appTerm
238
def
appTerm
appTerm
190
ref
34
ref
appTerm
appTerm
appTerm
239
def
appTerm
56
ref
182
ref
184
ref
35
ref
appTerm
19
ref
appTerm
240
def
appTerm
241
def
appTerm
12
ref
27
ref
192
ref
35
ref
appTerm
242
def
appTerm
appTerm
190
ref
35
ref
appTerm
243
def
appTerm
appTerm
244
def
appTerm
245
def
absTerm
246
def
appTerm
247
def
absTerm
248
def
appTerm
249
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
131
ref
subst
proveHyp
nil
123
ref
248
remove
nil
cons
cons
nil
cons
nil
cons
cons
55
ref
126
remove
appTerm
refl
136
remove
appThm
140
remove
eqMp
sym
250
def
subst
22
ref
nil
86
ref
247
remove
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
nil
144
ref
246
remove
nil
cons
cons
nil
cons
nil
cons
cons
224
ref
250
ref
subst
251
def
subst
17
ref
nil
86
ref
245
remove
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
nil
51
ref
239
remove
nil
cons
252
def
cons
52
ref
244
remove
nil
cons
253
def
cons
nil
cons
cons
nil
cons
cons
254
def
73
ref
subst
254
remove
131
ref
subst
225
ref
226
ref
17
ref
241
ref
absTerm
255
def
34
ref
appTerm
256
def
betaConv
22
ref
46
ref
255
ref
appTerm
257
def
absTerm
258
def
32
ref
appTerm
259
def
betaConv
nil
7
ref
258
ref
appTerm
260
def
axiom
nil
51
ref
260
remove
nil
cons
cons
52
ref
259
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
122
ref
123
ref
258
remove
nil
cons
cons
124
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
nil
51
ref
257
remove
nil
cons
cons
52
ref
256
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
143
ref
144
ref
255
remove
nil
cons
cons
146
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
nil
51
ref
241
remove
nil
cons
cons
52
ref
55
ref
240
ref
appTerm
204
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
nil
99
ref
240
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
51
ref
182
ref
103
ref
appTerm
261
def
nil
cons
262
def
cons
52
ref
55
ref
103
ref
appTerm
204
ref
appTerm
nil
cons
263
def
cons
nil
cons
cons
nil
cons
cons
264
def
73
ref
subst
264
remove
131
ref
subst
nil
51
ref
103
ref
nil
cons
265
def
cons
222
ref
cons
nil
cons
cons
225
ref
199
ref
59
ref
appTerm
266
def
assume
267
def
appThm
68
ref
appThm
sym
nil
51
ref
95
ref
cons
268
def
52
ref
95
ref
cons
nil
cons
cons
nil
cons
cons
269
def
73
ref
subst
269
remove
131
ref
subst
97
remove
eqMp
nil
99
ref
95
ref
cons
101
remove
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
270
def
eqMp
271
def
nil
51
ref
60
ref
nil
cons
272
def
cons
52
ref
56
ref
59
ref
appTerm
273
def
57
ref
appTerm
nil
cons
274
def
cons
nil
cons
cons
nil
cons
cons
131
ref
subst
proveHyp
273
ref
refl
267
remove
appThm
sym
270
remove
eqMp
eqMp
nil
268
remove
52
ref
87
ref
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
nil
99
ref
272
ref
cons
100
ref
274
remove
cons
nil
cons
cons
nil
cons
cons
275
def
102
ref
106
remove
116
ref
appTerm
betaConv
116
remove
103
ref
appTerm
betaConv
108
ref
appThm
115
remove
105
ref
appTerm
betaConv
trans
trans
appThm
117
remove
appThm
113
remove
118
remove
appThm
eqMp
sym
92
ref
eqMp
276
def
subst
eqMp
120
ref
275
remove
114
ref
subst
eqMp
deductAntisym
deductAntisym
subst
55
ref
261
ref
appTerm
refl
51
ref
58
ref
204
ref
appTerm
absTerm
277
def
103
ref
appTerm
betaConv
appThm
nil
82
ref
182
ref
appTerm
277
remove
appTerm
axiom
112
ref
appThm
eqMp
261
remove
assume
eqMp
nil
51
ref
56
ref
103
ref
appTerm
278
def
204
ref
appTerm
nil
cons
cons
52
ref
232
ref
103
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
131
ref
subst
proveHyp
nil
51
ref
221
ref
cons
52
ref
265
ref
cons
nil
cons
cons
nil
cons
cons
279
def
73
ref
subst
279
remove
131
ref
subst
51
ref
57
ref
absTerm
280
def
103
ref
appTerm
281
def
betaConv
nil
55
ref
204
ref
appTerm
282
def
173
ref
280
ref
appTerm
283
def
appTerm
axiom
204
ref
assume
eqMp
nil
51
ref
283
remove
nil
cons
cons
52
ref
281
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
280
remove
nil
cons
cons
177
ref
265
ref
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
eqMp
nil
99
ref
221
ref
cons
100
ref
265
remove
cons
nil
cons
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
99
ref
262
remove
cons
100
ref
263
remove
cons
nil
cons
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
284
def
subst
eqMp
appThm
nil
55
ref
182
ref
204
ref
appTerm
285
def
appTerm
78
ref
appTerm
axiom
286
def
trans
appThm
13
ref
229
ref
17
ref
184
ref
242
remove
appTerm
"Data.List.@"
const
1
ref
16
ref
30
remove
cons
opType
constTerm
287
def
238
ref
appTerm
33
ref
19
ref
appTerm
appTerm
appTerm
absTerm
288
def
34
ref
appTerm
289
def
betaConv
22
ref
46
ref
288
ref
appTerm
290
def
absTerm
291
def
32
ref
appTerm
292
def
betaConv
nil
7
ref
291
ref
appTerm
293
def
axiom
nil
51
ref
293
remove
nil
cons
cons
52
ref
292
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
122
ref
123
ref
291
remove
nil
cons
cons
124
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
nil
51
ref
290
remove
nil
cons
cons
52
ref
289
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
143
ref
144
ref
288
remove
nil
cons
cons
146
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
appThm
nil
21
remove
181
ref
238
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
181
ref
12
ref
27
ref
287
ref
185
ref
appTerm
294
def
35
ref
appTerm
appTerm
appTerm
36
ref
appTerm
absTerm
295
def
185
ref
appTerm
296
def
betaConv
297
def
229
ref
nil
181
ref
35
ref
nil
cons
298
def
cons
299
def
nil
cons
nil
cons
cons
181
ref
184
ref
287
ref
19
ref
appTerm
300
def
185
ref
appTerm
appTerm
185
ref
appTerm
absTerm
301
def
185
ref
appTerm
302
def
betaConv
nil
46
ref
301
ref
appTerm
303
def
axiom
nil
51
ref
303
remove
nil
cons
cons
52
ref
302
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
143
ref
144
ref
301
remove
nil
cons
cons
145
ref
185
ref
nil
cons
304
def
cons
nil
cons
305
def
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
subst
appThm
nil
51
ref
12
ref
27
ref
300
remove
35
ref
appTerm
appTerm
appTerm
36
ref
appTerm
306
def
nil
cons
cons
52
ref
7
ref
"h'"
2
ref
var
307
def
46
ref
"t'"
16
ref
var
308
def
56
ref
12
ref
27
ref
287
ref
308
ref
varTerm
309
def
appTerm
35
ref
appTerm
310
def
appTerm
appTerm
36
ref
appTerm
311
def
appTerm
12
ref
27
ref
287
ref
31
ref
307
ref
varTerm
312
def
appTerm
309
ref
appTerm
313
def
appTerm
35
ref
appTerm
appTerm
appTerm
36
ref
appTerm
314
def
appTerm
315
def
absTerm
316
def
appTerm
317
def
absTerm
318
def
appTerm
319
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
131
ref
subst
proveHyp
nil
123
ref
318
remove
nil
cons
cons
nil
cons
nil
cons
cons
250
ref
subst
307
ref
nil
86
ref
317
remove
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
nil
144
ref
316
remove
nil
cons
cons
nil
cons
nil
cons
cons
251
ref
subst
308
ref
nil
86
ref
315
remove
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
nil
51
ref
311
ref
nil
cons
320
def
cons
52
ref
314
remove
nil
cons
321
def
cons
nil
cons
cons
nil
cons
cons
322
def
73
ref
subst
322
remove
131
ref
subst
13
ref
229
ref
nil
299
remove
17
ref
309
ref
nil
cons
323
def
cons
22
ref
312
ref
nil
cons
324
def
cons
nil
cons
325
def
cons
cons
nil
cons
cons
17
ref
184
ref
287
ref
35
ref
appTerm
185
ref
appTerm
appTerm
33
remove
287
ref
34
ref
appTerm
185
ref
appTerm
appTerm
appTerm
absTerm
326
def
34
ref
appTerm
327
def
betaConv
22
ref
46
ref
326
ref
appTerm
328
def
absTerm
329
def
32
ref
appTerm
330
def
betaConv
181
ref
7
ref
329
ref
appTerm
331
def
absTerm
332
def
185
ref
appTerm
333
def
betaConv
nil
46
ref
332
ref
appTerm
334
def
axiom
nil
51
ref
334
remove
nil
cons
cons
52
ref
333
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
143
ref
144
ref
332
remove
nil
cons
cons
305
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
nil
51
ref
331
remove
nil
cons
cons
52
ref
330
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
122
ref
123
ref
329
remove
nil
cons
cons
124
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
nil
51
ref
328
remove
nil
cons
cons
52
ref
327
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
143
ref
144
ref
326
remove
nil
cons
cons
146
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
subst
appThm
nil
17
ref
310
remove
nil
cons
cons
325
remove
cons
nil
cons
cons
147
ref
subst
148
ref
nil
"l2"
16
ref
var
335
def
298
remove
cons
"l1"
16
ref
var
336
def
323
remove
cons
nil
cons
cons
nil
cons
cons
335
ref
55
ref
39
ref
287
remove
336
ref
varTerm
337
def
appTerm
338
def
335
ref
varTerm
339
def
appTerm
340
def
appTerm
appTerm
62
ref
39
ref
337
ref
appTerm
appTerm
39
ref
339
ref
appTerm
341
def
appTerm
appTerm
absTerm
342
def
339
ref
appTerm
343
def
betaConv
336
ref
46
ref
342
ref
appTerm
344
def
absTerm
345
def
337
ref
appTerm
346
def
betaConv
nil
46
ref
345
ref
appTerm
347
def
axiom
nil
51
ref
347
remove
nil
cons
cons
52
ref
346
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
143
ref
144
ref
345
remove
nil
cons
cons
145
ref
337
ref
nil
cons
348
def
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
nil
51
ref
344
remove
nil
cons
cons
52
ref
343
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
143
ref
144
ref
342
remove
nil
cons
cons
145
ref
339
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
subst
62
ref
39
ref
309
ref
appTerm
349
def
appTerm
refl
17
ref
182
ref
39
ref
35
ref
appTerm
350
def
appTerm
351
def
absTerm
352
def
34
ref
appTerm
353
def
betaConv
22
ref
46
ref
352
ref
appTerm
354
def
absTerm
355
def
32
ref
appTerm
356
def
betaConv
nil
7
ref
355
ref
appTerm
357
def
axiom
nil
51
ref
357
remove
nil
cons
cons
52
ref
356
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
122
ref
123
ref
355
remove
nil
cons
cons
124
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
nil
51
ref
354
remove
nil
cons
cons
52
ref
353
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
143
ref
144
ref
352
remove
nil
cons
cons
146
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
nil
51
ref
351
remove
nil
cons
cons
52
ref
55
ref
350
ref
appTerm
204
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
nil
99
ref
350
ref
nil
cons
cons
nil
cons
nil
cons
cons
284
ref
subst
eqMp
358
def
appThm
nil
86
ref
349
remove
nil
cons
cons
nil
cons
nil
cons
cons
86
ref
55
ref
62
ref
89
ref
appTerm
359
def
204
ref
appTerm
appTerm
204
ref
appTerm
absTerm
360
def
89
ref
appTerm
361
def
betaConv
nil
173
ref
360
ref
appTerm
362
def
axiom
nil
51
ref
362
remove
nil
cons
cons
52
ref
361
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
360
remove
nil
cons
cons
178
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
subst
trans
trans
appThm
312
remove
refl
appThm
311
remove
assume
147
ref
trans
appThm
nil
153
ref
42
remove
nil
cons
363
def
cons
155
ref
324
remove
cons
nil
cons
cons
nil
cons
cons
153
ref
12
ref
37
ref
204
ref
appTerm
156
ref
appTerm
157
ref
appTerm
appTerm
157
ref
appTerm
absTerm
364
def
157
remove
appTerm
365
def
betaConv
155
ref
7
ref
364
ref
appTerm
366
def
absTerm
367
def
156
remove
appTerm
368
def
betaConv
nil
7
ref
367
ref
appTerm
369
def
axiom
nil
51
ref
369
remove
nil
cons
cons
52
ref
368
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
122
ref
123
ref
367
remove
nil
cons
cons
164
remove
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
nil
51
ref
366
remove
nil
cons
cons
52
ref
365
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
122
ref
123
ref
364
remove
nil
cons
cons
165
remove
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
370
def
subst
trans
trans
trans
appThm
147
ref
appThm
nil
9
ref
363
remove
cons
nil
cons
nil
cons
cons
169
ref
subst
trans
sym
92
ref
eqMp
eqMp
nil
99
ref
320
remove
cons
100
ref
321
remove
cons
nil
cons
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
51
ref
62
ref
306
remove
appTerm
319
remove
appTerm
nil
cons
cons
52
ref
46
ref
295
ref
appTerm
371
def
nil
cons
372
def
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
225
ref
62
ref
refl
373
def
295
ref
19
ref
appTerm
betaConv
appThm
8
ref
307
remove
46
ref
refl
374
def
308
remove
225
ref
295
ref
309
remove
appTerm
betaConv
appThm
295
ref
313
remove
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
374
ref
181
ref
297
remove
absThm
appThm
appThm
nil
"p"
38
ref
var
375
def
295
remove
nil
cons
376
def
cons
nil
cons
nil
cons
cons
375
ref
56
ref
62
ref
375
ref
varTerm
377
def
19
ref
appTerm
appTerm
7
ref
22
ref
46
ref
17
ref
56
ref
377
ref
34
ref
appTerm
appTerm
377
ref
35
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
46
ref
181
ref
377
ref
185
ref
appTerm
absTerm
appTerm
appTerm
absTerm
378
def
377
ref
appTerm
379
def
betaConv
nil
0
ref
1
ref
45
ref
4
ref
cons
opType
constTerm
378
ref
appTerm
380
def
axiom
nil
51
ref
380
remove
nil
cons
cons
52
ref
379
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
"A"
183
remove
cons
nil
cons
"P"
45
ref
var
378
remove
nil
cons
cons
"x"
38
ref
var
377
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
381
def
subst
eqMp
eqMp
382
def
nil
51
ref
372
ref
cons
52
ref
296
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
143
ref
144
ref
376
remove
cons
305
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
383
def
subst
nil
124
ref
nil
cons
cons
384
def
167
remove
subst
trans
trans
appThm
17
ref
12
ref
243
remove
appTerm
32
ref
appTerm
absTerm
385
def
34
ref
appTerm
386
def
betaConv
22
ref
46
ref
385
ref
appTerm
387
def
absTerm
388
def
32
remove
appTerm
389
def
betaConv
nil
7
ref
388
ref
appTerm
390
def
axiom
nil
51
ref
390
remove
nil
cons
cons
52
ref
389
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
122
remove
123
ref
388
remove
nil
cons
cons
124
remove
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
nil
51
ref
387
remove
nil
cons
cons
52
ref
386
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
143
ref
144
ref
385
remove
nil
cons
cons
146
remove
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
appThm
384
remove
169
ref
subst
trans
appThm
170
ref
86
ref
55
ref
56
ref
78
ref
appTerm
391
def
89
ref
appTerm
appTerm
89
ref
appTerm
absTerm
392
def
89
ref
appTerm
393
def
betaConv
nil
173
ref
392
ref
appTerm
394
def
axiom
nil
51
ref
394
remove
nil
cons
cons
52
ref
393
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
392
remove
nil
cons
cons
178
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
395
def
subst
trans
sym
92
ref
eqMp
eqMp
nil
99
ref
252
remove
cons
100
ref
253
remove
cons
nil
cons
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
51
ref
62
ref
237
remove
appTerm
249
remove
appTerm
nil
cons
cons
52
ref
46
ref
181
ref
188
remove
12
ref
27
ref
193
ref
appTerm
appTerm
190
ref
185
ref
appTerm
appTerm
396
def
appTerm
absTerm
397
def
appTerm
398
def
nil
cons
399
def
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
225
ref
373
ref
397
ref
19
ref
appTerm
betaConv
appThm
8
ref
22
ref
374
ref
17
ref
225
ref
397
ref
34
ref
appTerm
betaConv
appThm
397
ref
35
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
374
ref
181
ref
397
ref
185
ref
appTerm
betaConv
absThm
appThm
appThm
nil
375
ref
397
remove
nil
cons
cons
nil
cons
nil
cons
cons
381
ref
subst
eqMp
eqMp
400
def
subst
nil
51
ref
0
ref
1
ref
1
ref
14
remove
28
ref
opType
401
def
4
ref
cons
opType
402
def
4
ref
cons
opType
constTerm
403
def
"l"
401
ref
var
404
def
56
ref
182
ref
10
ref
1
ref
401
ref
402
remove
nil
cons
cons
opType
constTerm
405
def
404
ref
varTerm
406
def
appTerm
18
remove
401
ref
constTerm
407
def
appTerm
408
def
appTerm
appTerm
184
ref
25
remove
1
ref
401
ref
28
remove
cons
opType
409
def
constTerm
191
remove
1
ref
401
ref
401
remove
nil
cons
cons
opType
constTerm
410
def
406
ref
appTerm
411
def
appTerm
appTerm
189
remove
409
remove
constTerm
406
ref
appTerm
appTerm
appTerm
absTerm
appTerm
412
def
nil
cons
413
def
cons
222
ref
cons
nil
cons
cons
414
def
120
ref
subst
proveHyp
400
ref
nil
51
ref
399
ref
cons
415
def
52
ref
56
ref
412
ref
appTerm
204
ref
appTerm
416
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
224
ref
nil
46
ref
181
ref
184
ref
192
ref
193
ref
appTerm
417
def
appTerm
185
ref
appTerm
418
def
absTerm
419
def
appTerm
420
def
axiom
421
def
subst
nil
51
ref
403
ref
404
ref
405
ref
410
remove
411
ref
appTerm
appTerm
406
remove
appTerm
absTerm
appTerm
422
def
nil
cons
423
def
cons
424
def
52
ref
56
ref
398
ref
appTerm
425
def
416
remove
appTerm
426
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
421
remove
nil
51
ref
420
ref
nil
cons
427
def
cons
428
def
52
ref
56
ref
422
remove
appTerm
429
def
426
remove
appTerm
430
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
224
ref
nil
46
ref
181
ref
55
ref
184
ref
193
ref
appTerm
19
ref
appTerm
431
def
appTerm
186
ref
appTerm
absTerm
appTerm
432
def
axiom
433
def
subst
nil
51
ref
403
remove
404
remove
55
ref
405
remove
411
remove
appTerm
407
remove
appTerm
appTerm
408
remove
appTerm
absTerm
appTerm
434
def
nil
cons
435
def
cons
436
def
52
ref
56
ref
420
remove
appTerm
437
def
430
remove
appTerm
438
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
433
remove
nil
51
ref
432
ref
nil
cons
439
def
cons
440
def
52
ref
56
ref
434
remove
appTerm
441
def
438
remove
appTerm
442
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
nil
220
ref
52
ref
56
ref
432
ref
appTerm
443
def
442
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
56
ref
218
ref
appTerm
refl
443
ref
refl
441
ref
refl
437
ref
refl
429
ref
refl
425
ref
refl
nil
86
ref
413
ref
cons
nil
cons
nil
cons
cons
209
ref
subst
444
def
appThm
appThm
appThm
appThm
appThm
appThm
sym
nil
220
remove
52
ref
443
remove
441
remove
437
remove
429
remove
425
remove
182
ref
412
remove
appTerm
445
def
appTerm
446
def
appTerm
447
def
appTerm
448
def
appTerm
449
def
appTerm
nil
cons
450
def
cons
nil
cons
cons
nil
cons
cons
451
def
73
ref
subst
451
remove
131
ref
subst
nil
440
remove
52
ref
449
remove
nil
cons
452
def
cons
nil
cons
cons
nil
cons
cons
453
def
73
ref
subst
453
remove
131
ref
subst
nil
436
remove
52
ref
448
remove
nil
cons
454
def
cons
nil
cons
cons
nil
cons
cons
455
def
73
ref
subst
455
remove
131
ref
subst
nil
428
ref
52
ref
447
remove
nil
cons
456
def
cons
nil
cons
cons
nil
cons
cons
457
def
73
ref
subst
457
remove
131
ref
subst
nil
424
remove
52
ref
446
remove
nil
cons
458
def
cons
nil
cons
cons
nil
cons
cons
459
def
73
ref
subst
459
remove
131
ref
subst
nil
415
remove
52
ref
445
remove
nil
cons
460
def
cons
nil
cons
cons
nil
cons
cons
461
def
73
ref
subst
461
remove
131
ref
subst
444
remove
414
ref
73
ref
subst
414
remove
131
ref
subst
nil
144
ref
197
ref
nil
cons
cons
nil
cons
nil
cons
cons
224
ref
102
ref
226
ref
8
ref
nil
"t"
5
ref
var
125
ref
nil
cons
462
def
cons
nil
cons
nil
cons
cons
121
remove
"B"
4
ref
cons
nil
cons
cons
216
remove
cons
"t"
1
ref
2
ref
"B"
varType
nil
cons
cons
opType
463
def
var
464
def
10
remove
1
ref
463
ref
1
ref
463
ref
4
ref
cons
opType
465
def
nil
cons
cons
opType
constTerm
466
def
464
ref
varTerm
467
def
appTerm
9
ref
467
ref
23
ref
appTerm
absTerm
468
def
appTerm
469
def
absTerm
470
def
467
ref
appTerm
471
def
betaConv
0
ref
1
remove
465
ref
4
remove
cons
opType
constTerm
472
def
refl
464
ref
469
remove
assume
sym
466
remove
468
remove
appTerm
467
ref
appTerm
473
def
assume
sym
deductAntisym
absThm
appThm
nil
472
ref
464
remove
473
remove
absTerm
appTerm
axiom
eqMp
nil
51
ref
472
remove
470
ref
appTerm
nil
cons
cons
52
ref
471
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
"A"
463
ref
nil
cons
cons
nil
cons
"P"
465
remove
var
470
remove
nil
cons
cons
"x"
463
remove
var
467
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
subst
subst
appThm
appThm
appThm
"Data.Bool.?"
const
474
def
6
ref
constTerm
475
def
9
ref
182
ref
128
ref
appTerm
absTerm
appTerm
refl
appThm
sym
nil
133
ref
462
remove
cons
nil
cons
nil
cons
cons
133
ref
55
ref
182
ref
7
ref
9
ref
134
ref
23
ref
appTerm
476
def
absTerm
appTerm
477
def
appTerm
appTerm
475
ref
9
ref
182
ref
476
ref
appTerm
absTerm
appTerm
appTerm
absTerm
478
def
134
ref
appTerm
479
def
betaConv
nil
0
remove
137
remove
constTerm
480
def
478
ref
appTerm
481
def
axiom
nil
51
ref
481
remove
nil
cons
cons
52
ref
479
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
"A"
11
remove
cons
nil
cons
482
def
"P"
6
remove
var
483
def
478
remove
nil
cons
cons
"x"
5
ref
var
484
def
134
ref
nil
cons
cons
nil
cons
485
def
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
subst
eqMp
subst
subst
474
remove
45
remove
constTerm
486
def
refl
181
ref
226
ref
197
remove
185
ref
appTerm
betaConv
appThm
nil
51
ref
187
ref
nil
cons
487
def
cons
488
def
52
ref
196
ref
nil
cons
489
def
cons
nil
cons
490
def
cons
nil
cons
cons
nil
51
ref
199
ref
204
ref
appTerm
491
def
nil
cons
492
def
cons
493
def
52
ref
55
ref
182
ref
60
remove
appTerm
appTerm
63
remove
182
ref
59
ref
appTerm
494
def
appTerm
appTerm
nil
cons
495
def
cons
nil
cons
496
def
cons
nil
cons
cons
497
def
73
ref
subst
497
remove
131
ref
subst
55
ref
"_546"
3
ref
var
498
def
55
ref
182
ref
56
ref
498
remove
varTerm
499
def
appTerm
59
ref
appTerm
appTerm
appTerm
62
ref
499
remove
appTerm
494
ref
appTerm
appTerm
absTerm
500
def
57
ref
appTerm
501
def
appTerm
refl
502
def
500
ref
204
ref
appTerm
betaConv
appThm
102
ref
501
remove
betaConv
appThm
503
def
55
ref
182
ref
232
remove
59
ref
appTerm
504
def
appTerm
appTerm
62
ref
204
ref
appTerm
505
def
494
ref
appTerm
appTerm
refl
appThm
trans
500
remove
refl
506
def
491
remove
assume
507
def
appThm
eqMp
sym
102
ref
226
ref
96
ref
236
remove
subst
508
def
appThm
228
ref
trans
appThm
nil
86
ref
494
ref
nil
cons
509
def
cons
nil
cons
nil
cons
cons
510
def
86
ref
55
ref
505
remove
89
ref
appTerm
appTerm
204
ref
appTerm
absTerm
511
def
89
ref
appTerm
512
def
betaConv
nil
173
ref
511
ref
appTerm
513
def
axiom
nil
51
ref
513
remove
nil
cons
cons
52
ref
512
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
511
remove
nil
cons
cons
178
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
514
def
subst
appThm
nil
86
ref
221
ref
cons
nil
cons
nil
cons
cons
86
ref
55
ref
282
ref
89
ref
appTerm
appTerm
205
ref
appTerm
absTerm
515
def
89
ref
appTerm
516
def
betaConv
nil
173
ref
515
ref
appTerm
517
def
axiom
nil
51
ref
517
remove
nil
cons
cons
52
ref
516
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
515
remove
nil
cons
cons
178
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
518
def
subst
286
ref
trans
519
def
trans
sym
92
ref
eqMp
eqMp
eqMp
nil
99
ref
492
ref
cons
520
def
100
ref
495
ref
cons
nil
cons
521
def
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
nil
51
ref
199
remove
78
ref
appTerm
522
def
nil
cons
523
def
cons
524
def
496
remove
cons
nil
cons
cons
525
def
73
ref
subst
525
remove
131
ref
subst
502
remove
"_544"
3
ref
var
526
def
55
ref
182
ref
56
ref
526
remove
varTerm
527
def
appTerm
59
ref
appTerm
appTerm
appTerm
62
ref
527
remove
appTerm
494
ref
appTerm
appTerm
absTerm
78
ref
appTerm
betaConv
appThm
503
remove
55
ref
182
ref
391
remove
59
ref
appTerm
528
def
appTerm
appTerm
62
ref
78
ref
appTerm
529
def
494
ref
appTerm
appTerm
refl
appThm
trans
506
remove
522
remove
assume
530
def
appThm
eqMp
sym
102
ref
226
ref
96
ref
395
remove
subst
531
def
appThm
appThm
510
ref
86
ref
55
ref
529
remove
89
ref
appTerm
appTerm
89
ref
appTerm
absTerm
532
def
89
ref
appTerm
533
def
betaConv
nil
173
ref
532
ref
appTerm
534
def
axiom
nil
51
ref
534
remove
nil
cons
cons
52
ref
533
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
532
remove
nil
cons
cons
178
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
535
def
subst
appThm
nil
177
ref
509
remove
cons
nil
cons
nil
cons
cons
217
ref
subst
536
def
trans
sym
92
ref
eqMp
eqMp
eqMp
nil
99
ref
523
remove
cons
537
def
521
remove
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
86
ref
"Data.Bool.\\/"
const
54
remove
constTerm
538
def
91
remove
appTerm
90
remove
204
ref
appTerm
appTerm
absTerm
539
def
57
ref
appTerm
540
def
betaConv
nil
173
ref
539
ref
appTerm
541
def
axiom
542
def
nil
51
ref
541
remove
nil
cons
cons
543
def
52
ref
540
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
539
ref
nil
cons
cons
544
def
215
remove
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
545
def
nil
537
ref
100
ref
492
remove
cons
546
def
"R"
3
ref
var
547
def
495
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
51
ref
56
ref
105
ref
appTerm
548
def
547
ref
varTerm
549
def
appTerm
550
def
nil
cons
cons
52
ref
549
ref
nil
cons
551
def
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
nil
51
ref
278
ref
549
ref
appTerm
nil
cons
cons
52
ref
56
ref
550
remove
appTerm
549
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
"r"
3
ref
var
552
def
56
ref
278
remove
552
ref
varTerm
553
def
appTerm
appTerm
554
def
56
ref
548
remove
553
ref
appTerm
appTerm
553
ref
appTerm
appTerm
absTerm
555
def
549
remove
appTerm
556
def
betaConv
55
ref
538
ref
103
ref
appTerm
557
def
105
ref
appTerm
558
def
appTerm
refl
52
ref
173
ref
552
ref
554
remove
56
ref
273
remove
553
ref
appTerm
appTerm
553
ref
appTerm
559
def
appTerm
absTerm
appTerm
absTerm
105
ref
appTerm
betaConv
appThm
82
remove
557
remove
appTerm
refl
51
ref
52
ref
173
ref
552
ref
56
ref
58
remove
553
ref
appTerm
appTerm
559
remove
appTerm
absTerm
appTerm
absTerm
absTerm
560
def
103
remove
appTerm
betaConv
appThm
nil
70
remove
538
ref
appTerm
560
remove
appTerm
axiom
112
remove
appThm
eqMp
108
remove
appThm
eqMp
558
remove
assume
eqMp
nil
51
ref
173
ref
555
ref
appTerm
nil
cons
cons
52
ref
556
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
555
remove
nil
cons
cons
177
ref
551
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
eqMp
eqMp
561
def
subst
proveHyp
proveHyp
proveHyp
subst
trans
absThm
appThm
trans
218
remove
assume
eqMp
nil
51
ref
486
remove
181
ref
62
ref
187
ref
appTerm
182
ref
196
remove
appTerm
562
def
appTerm
563
def
absTerm
564
def
appTerm
565
def
nil
cons
cons
222
ref
cons
nil
cons
cons
120
ref
subst
proveHyp
nil
144
ref
181
ref
56
ref
564
ref
185
ref
appTerm
566
def
appTerm
204
ref
appTerm
567
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
251
ref
subst
181
ref
nil
86
ref
567
remove
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
nil
51
ref
566
ref
nil
cons
568
def
cons
222
ref
cons
nil
cons
cons
569
def
73
ref
subst
569
remove
131
ref
subst
566
ref
betaConv
566
remove
assume
eqMp
nil
51
ref
563
remove
nil
cons
570
def
cons
222
ref
cons
nil
cons
cons
571
def
120
ref
subst
proveHyp
571
ref
73
ref
subst
571
remove
131
ref
subst
nil
99
ref
487
remove
cons
100
ref
562
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
572
def
114
ref
subst
nil
488
ref
52
ref
182
ref
431
ref
appTerm
573
def
nil
cons
574
def
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
nil
"_17157"
16
ref
var
575
def
304
ref
cons
nil
cons
nil
cons
cons
nil
"b"
3
ref
var
576
def
184
ref
575
remove
varTerm
577
def
appTerm
19
ref
appTerm
nil
cons
cons
"a"
3
ref
var
578
def
182
ref
184
ref
192
ref
577
ref
appTerm
appTerm
19
ref
appTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
51
ref
55
ref
578
ref
varTerm
579
def
appTerm
580
def
204
ref
appTerm
581
def
nil
cons
582
def
cons
583
def
52
ref
55
ref
538
ref
579
ref
appTerm
576
ref
varTerm
584
def
appTerm
585
def
appTerm
56
ref
182
ref
584
ref
appTerm
586
def
appTerm
587
def
579
ref
appTerm
appTerm
nil
cons
588
def
cons
nil
cons
589
def
cons
nil
cons
cons
590
def
73
ref
subst
590
remove
131
ref
subst
55
ref
"_610"
3
ref
var
591
def
55
ref
538
ref
591
remove
varTerm
592
def
appTerm
584
ref
appTerm
appTerm
587
ref
592
remove
appTerm
appTerm
absTerm
593
def
579
ref
appTerm
594
def
appTerm
refl
595
def
593
ref
204
ref
appTerm
betaConv
appThm
102
ref
594
remove
betaConv
appThm
596
def
55
ref
538
ref
204
ref
appTerm
597
def
584
ref
appTerm
598
def
appTerm
587
ref
204
ref
appTerm
appTerm
refl
appThm
trans
593
remove
refl
599
def
581
remove
assume
600
def
appThm
eqMp
sym
102
ref
nil
86
ref
584
ref
nil
cons
601
def
cons
nil
cons
nil
cons
cons
602
def
86
ref
55
ref
597
ref
89
ref
appTerm
appTerm
89
ref
appTerm
absTerm
603
def
89
ref
appTerm
604
def
betaConv
nil
173
ref
603
ref
appTerm
605
def
axiom
nil
51
ref
605
remove
nil
cons
cons
52
ref
604
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
603
remove
nil
cons
cons
178
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
606
def
subst
607
def
appThm
nil
86
ref
586
ref
nil
cons
608
def
cons
nil
cons
nil
cons
cons
609
def
209
ref
subst
602
ref
213
ref
subst
trans
appThm
nil
177
ref
601
remove
cons
nil
cons
nil
cons
cons
217
ref
subst
trans
sym
92
ref
eqMp
eqMp
eqMp
nil
99
ref
582
ref
cons
610
def
100
ref
588
ref
cons
nil
cons
611
def
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
nil
51
ref
580
remove
78
ref
appTerm
612
def
nil
cons
613
def
cons
614
def
589
remove
cons
nil
cons
cons
615
def
73
ref
subst
615
remove
131
ref
subst
595
remove
"_608"
3
ref
var
616
def
55
ref
538
ref
616
remove
varTerm
617
def
appTerm
584
ref
appTerm
appTerm
587
ref
617
remove
appTerm
appTerm
absTerm
78
ref
appTerm
betaConv
appThm
596
remove
55
ref
538
ref
78
ref
appTerm
618
def
584
ref
appTerm
619
def
appTerm
587
remove
78
ref
appTerm
appTerm
refl
appThm
trans
599
remove
612
remove
assume
620
def
appThm
eqMp
sym
102
ref
602
remove
86
ref
55
ref
618
ref
89
ref
appTerm
appTerm
78
ref
appTerm
absTerm
621
def
89
ref
appTerm
622
def
betaConv
nil
173
ref
621
ref
appTerm
623
def
axiom
nil
51
ref
623
remove
nil
cons
cons
52
ref
622
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
621
remove
nil
cons
cons
178
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
624
def
subst
625
def
appThm
609
ref
86
ref
55
ref
203
remove
78
ref
appTerm
appTerm
78
ref
appTerm
absTerm
626
def
89
ref
appTerm
627
def
betaConv
nil
173
ref
626
ref
appTerm
628
def
axiom
nil
51
ref
628
remove
nil
cons
cons
52
ref
627
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
626
remove
nil
cons
cons
178
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
subst
appThm
170
ref
86
ref
55
ref
55
ref
78
ref
appTerm
629
def
89
ref
appTerm
appTerm
89
ref
appTerm
absTerm
630
def
89
ref
appTerm
631
def
betaConv
nil
173
ref
630
ref
appTerm
632
def
axiom
nil
51
ref
632
remove
nil
cons
cons
52
ref
631
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
630
remove
nil
cons
cons
178
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
633
def
subst
634
def
trans
sym
92
ref
eqMp
eqMp
eqMp
nil
99
ref
613
remove
cons
635
def
611
remove
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
539
ref
579
ref
appTerm
636
def
betaConv
542
ref
nil
543
ref
52
ref
636
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
544
ref
177
ref
579
ref
nil
cons
637
def
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
638
def
nil
635
ref
100
ref
582
remove
cons
639
def
547
ref
588
remove
cons
nil
cons
cons
cons
nil
cons
cons
561
ref
subst
proveHyp
proveHyp
proveHyp
640
def
subst
181
ref
538
ref
573
remove
appTerm
186
ref
appTerm
absTerm
641
def
577
ref
appTerm
642
def
betaConv
374
ref
181
ref
nil
51
ref
431
ref
nil
cons
cons
52
ref
186
ref
nil
cons
643
def
cons
nil
cons
cons
nil
cons
cons
nil
493
ref
52
ref
55
ref
266
ref
appTerm
62
ref
538
ref
57
ref
appTerm
494
ref
appTerm
appTerm
538
ref
201
ref
appTerm
59
ref
appTerm
644
def
appTerm
appTerm
nil
cons
645
def
cons
nil
cons
646
def
cons
nil
cons
cons
647
def
73
ref
subst
647
remove
131
ref
subst
55
ref
"_558"
3
ref
var
648
def
55
ref
55
ref
648
remove
varTerm
649
def
appTerm
59
ref
appTerm
appTerm
62
ref
538
ref
649
ref
appTerm
494
ref
appTerm
appTerm
538
ref
182
ref
649
remove
appTerm
appTerm
59
ref
appTerm
appTerm
appTerm
absTerm
650
def
57
ref
appTerm
651
def
appTerm
refl
652
def
650
ref
204
ref
appTerm
betaConv
appThm
102
ref
651
remove
betaConv
appThm
653
def
55
ref
282
remove
59
ref
appTerm
appTerm
62
ref
597
remove
494
ref
appTerm
appTerm
538
ref
285
ref
appTerm
654
def
59
ref
appTerm
655
def
appTerm
appTerm
refl
appThm
trans
650
remove
refl
656
def
507
ref
appThm
eqMp
sym
102
ref
96
ref
518
remove
subst
appThm
373
ref
510
ref
606
ref
subst
appThm
538
ref
refl
657
def
286
ref
appThm
68
ref
appThm
96
ref
624
ref
subst
trans
658
def
appThm
510
ref
86
ref
55
ref
359
remove
78
ref
appTerm
appTerm
89
ref
appTerm
absTerm
659
def
89
ref
appTerm
660
def
betaConv
nil
173
ref
659
ref
appTerm
661
def
axiom
nil
51
ref
661
remove
nil
cons
cons
52
ref
660
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
659
remove
nil
cons
cons
178
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
subst
trans
appThm
536
remove
trans
sym
92
ref
eqMp
eqMp
eqMp
nil
520
ref
100
ref
645
ref
cons
nil
cons
662
def
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
nil
524
ref
646
remove
cons
nil
cons
cons
663
def
73
ref
subst
663
remove
131
ref
subst
652
remove
"_556"
3
ref
var
664
def
55
ref
55
ref
664
remove
varTerm
665
def
appTerm
59
ref
appTerm
appTerm
62
ref
538
ref
665
ref
appTerm
494
ref
appTerm
appTerm
538
ref
182
ref
665
remove
appTerm
appTerm
59
ref
appTerm
appTerm
appTerm
absTerm
78
ref
appTerm
betaConv
appThm
653
remove
55
ref
629
remove
59
ref
appTerm
appTerm
62
ref
618
remove
494
remove
appTerm
appTerm
538
ref
227
ref
appTerm
666
def
59
ref
appTerm
667
def
appTerm
appTerm
refl
appThm
trans
656
remove
530
ref
appThm
eqMp
sym
102
ref
96
ref
633
remove
subst
appThm
373
ref
510
remove
624
ref
subst
appThm
657
ref
228
ref
appThm
68
remove
appThm
96
ref
606
ref
subst
trans
668
def
appThm
96
remove
535
ref
subst
trans
appThm
nil
177
ref
95
ref
cons
nil
cons
nil
cons
cons
217
ref
subst
669
def
trans
sym
92
ref
eqMp
eqMp
eqMp
nil
537
ref
662
remove
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
545
ref
nil
537
ref
546
ref
547
ref
645
remove
cons
nil
cons
cons
cons
nil
cons
cons
561
ref
subst
proveHyp
proveHyp
proveHyp
subst
absThm
appThm
102
ref
374
ref
181
ref
373
ref
181
ref
538
ref
431
remove
appTerm
187
remove
appTerm
absTerm
670
def
185
ref
appTerm
betaConv
671
def
appThm
641
ref
185
ref
appTerm
betaConv
672
def
appThm
absThm
appThm
appThm
373
ref
374
ref
181
ref
671
remove
absThm
appThm
appThm
374
ref
181
ref
672
remove
absThm
appThm
appThm
appThm
nil
375
ref
670
ref
nil
cons
cons
"q"
38
remove
var
641
ref
nil
cons
673
def
cons
nil
cons
cons
nil
cons
cons
224
ref
"q"
5
remove
var
674
def
55
ref
7
ref
9
ref
62
ref
476
ref
appTerm
674
remove
varTerm
675
def
23
remove
appTerm
676
def
appTerm
absTerm
appTerm
appTerm
62
ref
477
remove
appTerm
7
ref
9
ref
676
remove
absTerm
appTerm
appTerm
appTerm
absTerm
677
def
675
ref
appTerm
678
def
betaConv
133
ref
480
ref
677
ref
appTerm
679
def
absTerm
680
def
134
remove
appTerm
681
def
betaConv
nil
480
remove
680
ref
appTerm
682
def
axiom
nil
51
ref
682
remove
nil
cons
cons
52
ref
681
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
482
ref
483
ref
680
remove
nil
cons
cons
485
remove
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
nil
51
ref
679
remove
nil
cons
cons
52
ref
678
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
482
remove
483
remove
677
remove
nil
cons
cons
484
remove
675
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
subst
subst
eqMp
trans
432
remove
assume
eqMp
nil
99
ref
46
ref
670
remove
appTerm
nil
cons
cons
100
ref
46
ref
641
remove
appTerm
nil
cons
683
def
cons
nil
cons
cons
nil
cons
cons
276
ref
subst
proveHyp
nil
51
ref
683
remove
cons
52
ref
642
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
143
ref
144
ref
673
remove
cons
145
ref
577
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
eqMp
subst
eqMp
nil
51
ref
574
remove
cons
52
ref
12
ref
27
ref
417
ref
appTerm
684
def
appTerm
685
def
194
ref
appTerm
686
def
nil
cons
687
def
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
nil
"_17152"
16
ref
var
688
def
193
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
576
ref
184
ref
688
remove
varTerm
689
def
appTerm
19
ref
appTerm
nil
cons
690
def
cons
578
ref
12
ref
27
ref
192
remove
689
ref
appTerm
appTerm
appTerm
190
remove
689
ref
appTerm
appTerm
nil
cons
691
def
cons
nil
cons
cons
nil
cons
cons
640
ref
subst
nil
52
ref
691
remove
cons
51
ref
690
remove
cons
nil
cons
cons
nil
cons
cons
nil
"t2"
3
ref
var
692
def
95
ref
cons
"t1"
3
ref
var
693
def
87
ref
cons
nil
cons
cons
694
def
nil
cons
cons
692
ref
55
ref
538
ref
693
ref
varTerm
695
def
appTerm
696
def
692
ref
varTerm
697
def
appTerm
698
def
appTerm
538
ref
697
ref
appTerm
699
def
695
ref
appTerm
appTerm
absTerm
700
def
697
ref
appTerm
701
def
betaConv
693
ref
173
ref
700
ref
appTerm
702
def
absTerm
703
def
695
ref
appTerm
704
def
betaConv
nil
173
ref
703
ref
appTerm
705
def
axiom
nil
51
ref
705
remove
nil
cons
cons
52
ref
704
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
703
remove
nil
cons
cons
177
ref
695
ref
nil
cons
cons
nil
cons
706
def
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
nil
51
ref
702
remove
nil
cons
cons
52
ref
701
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
700
remove
nil
cons
cons
177
ref
697
ref
nil
cons
cons
nil
cons
707
def
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
subst
708
def
subst
181
ref
538
ref
186
remove
appTerm
396
ref
appTerm
absTerm
709
def
689
ref
appTerm
710
def
betaConv
374
ref
181
ref
nil
488
remove
52
ref
396
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
493
remove
52
ref
61
remove
644
remove
appTerm
nil
cons
711
def
cons
nil
cons
712
def
cons
nil
cons
cons
713
def
73
ref
subst
713
remove
131
ref
subst
55
ref
"_542"
3
ref
var
714
def
55
ref
56
ref
714
remove
varTerm
715
def
appTerm
59
ref
appTerm
appTerm
538
ref
182
ref
715
remove
appTerm
appTerm
59
ref
appTerm
appTerm
absTerm
716
def
57
remove
appTerm
717
def
appTerm
refl
718
def
716
ref
204
ref
appTerm
betaConv
appThm
102
ref
717
remove
betaConv
appThm
719
def
55
ref
504
remove
appTerm
655
remove
appTerm
refl
appThm
trans
716
remove
refl
720
def
507
remove
appThm
eqMp
sym
102
ref
508
remove
appThm
658
remove
appThm
634
remove
trans
sym
92
ref
eqMp
eqMp
eqMp
nil
520
remove
100
ref
711
ref
cons
nil
cons
721
def
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
nil
524
remove
712
remove
cons
nil
cons
cons
722
def
73
ref
subst
722
remove
131
ref
subst
718
remove
"_540"
3
ref
var
723
def
55
ref
56
ref
723
remove
varTerm
724
def
appTerm
59
ref
appTerm
appTerm
538
ref
182
ref
724
remove
appTerm
appTerm
59
ref
appTerm
appTerm
absTerm
78
ref
appTerm
betaConv
appThm
719
remove
55
ref
528
remove
appTerm
667
remove
appTerm
refl
appThm
trans
720
remove
530
remove
appThm
eqMp
sym
102
ref
531
remove
appThm
668
remove
appThm
669
remove
trans
sym
92
ref
eqMp
eqMp
eqMp
nil
537
ref
721
remove
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
545
remove
nil
537
remove
546
remove
547
ref
711
remove
cons
nil
cons
cons
cons
nil
cons
cons
561
ref
subst
proveHyp
proveHyp
proveHyp
subst
657
ref
nil
51
ref
643
remove
cons
nil
cons
nil
cons
cons
214
remove
subst
appThm
396
remove
refl
appThm
trans
absThm
appThm
398
ref
assume
eqMp
nil
51
ref
46
ref
709
ref
appTerm
nil
cons
cons
52
ref
710
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
143
ref
144
ref
709
remove
nil
cons
cons
145
ref
689
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
eqMp
eqMp
subst
eqMp
nil
51
ref
687
remove
cons
52
ref
685
remove
195
ref
appTerm
725
def
nil
cons
cons
nil
cons
726
def
cons
nil
cons
cons
131
ref
subst
proveHyp
nil
"_17150"
16
ref
var
727
def
304
ref
cons
nil
cons
nil
cons
cons
419
ref
727
remove
varTerm
728
def
appTerm
729
def
betaConv
nil
428
remove
52
ref
729
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
143
ref
144
ref
419
remove
nil
cons
cons
145
ref
728
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
subst
nil
51
ref
418
remove
nil
cons
cons
726
remove
cons
nil
cons
cons
120
ref
subst
proveHyp
nil
"_17163"
16
ref
var
730
def
304
ref
cons
"_17162"
16
remove
var
731
def
417
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
51
ref
184
ref
731
remove
varTerm
732
def
appTerm
730
remove
varTerm
733
def
appTerm
734
def
nil
cons
735
def
cons
52
ref
12
ref
27
ref
732
remove
appTerm
appTerm
27
ref
733
remove
appTerm
appTerm
nil
cons
736
def
cons
nil
cons
cons
nil
cons
cons
737
def
73
ref
subst
737
remove
131
ref
subst
229
ref
734
remove
assume
appThm
eqMp
nil
99
ref
735
remove
cons
100
ref
736
remove
cons
nil
cons
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
51
ref
62
ref
686
remove
appTerm
725
remove
appTerm
nil
cons
cons
490
remove
cons
nil
cons
cons
120
ref
subst
proveHyp
nil
"z"
2
ref
var
738
def
195
ref
nil
cons
cons
"y"
2
ref
var
739
def
194
remove
nil
cons
cons
9
ref
684
remove
nil
cons
cons
nil
cons
cons
cons
nil
cons
cons
nil
576
ref
538
ref
182
ref
168
ref
739
remove
varTerm
740
def
appTerm
741
def
appTerm
742
def
appTerm
743
def
182
ref
168
remove
738
remove
varTerm
744
def
appTerm
745
def
appTerm
746
def
appTerm
nil
cons
cons
578
ref
12
ref
740
ref
appTerm
744
ref
appTerm
747
def
nil
cons
748
def
cons
nil
cons
cons
nil
cons
cons
640
remove
subst
225
ref
nil
576
remove
746
ref
nil
cons
749
def
cons
578
ref
742
remove
nil
cons
750
def
cons
nil
cons
cons
nil
cons
cons
nil
583
remove
52
ref
55
ref
182
ref
585
remove
appTerm
appTerm
62
ref
182
ref
579
ref
appTerm
appTerm
586
ref
appTerm
appTerm
nil
cons
751
def
cons
nil
cons
752
def
cons
nil
cons
cons
753
def
73
ref
subst
753
remove
131
ref
subst
55
ref
"_614"
3
ref
var
754
def
55
ref
182
ref
538
ref
754
remove
varTerm
755
def
appTerm
584
ref
appTerm
appTerm
appTerm
62
ref
182
ref
755
remove
appTerm
appTerm
586
ref
appTerm
appTerm
absTerm
756
def
579
remove
appTerm
757
def
appTerm
refl
758
def
756
ref
204
ref
appTerm
betaConv
appThm
102
ref
757
remove
betaConv
appThm
759
def
55
ref
182
ref
598
remove
appTerm
appTerm
62
ref
285
ref
appTerm
586
ref
appTerm
appTerm
refl
appThm
trans
756
remove
refl
760
def
600
remove
appThm
eqMp
sym
102
ref
226
ref
607
remove
appThm
appThm
373
ref
286
ref
appThm
586
ref
refl
761
def
appThm
609
ref
535
remove
subst
trans
appThm
nil
177
ref
608
remove
cons
nil
cons
nil
cons
cons
217
ref
subst
trans
sym
92
ref
eqMp
eqMp
eqMp
nil
610
remove
100
ref
751
ref
cons
nil
cons
762
def
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
nil
614
remove
752
remove
cons
nil
cons
cons
763
def
73
ref
subst
763
remove
131
ref
subst
758
remove
"_612"
3
ref
var
764
def
55
ref
182
ref
538
ref
764
remove
varTerm
765
def
appTerm
584
remove
appTerm
appTerm
appTerm
62
ref
182
ref
765
remove
appTerm
appTerm
586
ref
appTerm
appTerm
absTerm
78
ref
appTerm
betaConv
appThm
759
remove
55
ref
182
ref
619
remove
appTerm
appTerm
62
ref
227
ref
appTerm
586
remove
appTerm
appTerm
refl
appThm
trans
760
remove
620
remove
appThm
eqMp
sym
102
ref
226
ref
625
remove
appThm
228
ref
trans
appThm
373
ref
228
ref
appThm
761
remove
appThm
609
remove
514
remove
subst
trans
appThm
519
remove
trans
sym
92
ref
eqMp
eqMp
eqMp
nil
635
ref
762
remove
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
638
remove
nil
635
remove
639
remove
547
ref
751
remove
cons
nil
cons
cons
cons
nil
cons
cons
561
ref
subst
proveHyp
proveHyp
proveHyp
subst
373
ref
nil
578
ref
741
ref
nil
cons
766
def
cons
nil
cons
nil
cons
cons
nil
86
ref
637
remove
cons
nil
cons
nil
cons
cons
213
remove
subst
767
def
subst
appThm
nil
578
remove
745
remove
nil
cons
cons
nil
cons
nil
cons
cons
767
remove
subst
appThm
trans
appThm
747
ref
refl
768
def
appThm
trans
743
ref
refl
nil
52
ref
748
ref
cons
769
def
51
ref
749
ref
cons
nil
cons
cons
nil
cons
cons
708
ref
subst
appThm
nil
552
remove
749
remove
cons
769
remove
51
ref
750
ref
cons
770
def
nil
cons
cons
cons
nil
cons
cons
102
ref
nil
"t3"
3
ref
var
771
def
553
ref
nil
cons
cons
772
def
694
remove
cons
nil
cons
cons
771
ref
55
ref
696
remove
699
remove
771
ref
varTerm
773
def
appTerm
appTerm
774
def
appTerm
538
ref
698
remove
appTerm
773
ref
appTerm
775
def
appTerm
776
def
absTerm
777
def
773
ref
appTerm
778
def
betaConv
692
ref
173
ref
777
ref
appTerm
779
def
absTerm
780
def
697
remove
appTerm
781
def
betaConv
693
ref
173
ref
780
ref
appTerm
782
def
absTerm
783
def
695
remove
appTerm
784
def
betaConv
173
ref
refl
785
def
693
ref
785
ref
692
ref
785
remove
771
ref
776
remove
assume
sym
55
ref
775
remove
appTerm
774
remove
appTerm
786
def
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
absThm
appThm
nil
173
ref
693
ref
173
ref
692
ref
173
ref
771
remove
786
remove
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
51
ref
173
ref
783
ref
appTerm
nil
cons
cons
52
ref
784
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
783
remove
nil
cons
cons
706
remove
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
nil
51
ref
782
remove
nil
cons
cons
52
ref
781
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
780
remove
nil
cons
cons
707
remove
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
nil
51
ref
779
remove
nil
cons
cons
52
ref
778
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
777
remove
nil
cons
cons
177
ref
773
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
787
def
subst
appThm
nil
772
remove
692
remove
87
remove
cons
693
remove
95
remove
cons
nil
cons
cons
cons
nil
cons
cons
787
remove
subst
appThm
sym
657
ref
708
remove
appThm
553
remove
refl
appThm
eqMp
subst
trans
nil
770
ref
52
ref
743
remove
538
ref
746
remove
appTerm
747
ref
appTerm
788
def
appTerm
nil
cons
789
def
cons
nil
cons
790
def
cons
nil
cons
cons
791
def
73
ref
subst
791
remove
131
ref
subst
657
ref
226
ref
nil
770
remove
52
ref
55
ref
741
ref
appTerm
204
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
nil
99
ref
766
ref
cons
792
def
nil
cons
nil
cons
cons
284
remove
subst
eqMp
appThm
286
ref
trans
appThm
788
ref
refl
appThm
nil
86
ref
788
remove
nil
cons
cons
nil
cons
nil
cons
cons
624
remove
subst
trans
sym
92
ref
eqMp
eqMp
nil
99
ref
750
ref
cons
100
ref
789
ref
cons
nil
cons
793
def
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
nil
51
ref
766
ref
cons
790
remove
cons
nil
cons
cons
794
def
73
ref
subst
794
remove
131
ref
subst
657
ref
226
ref
13
ref
741
ref
assume
appThm
795
def
740
ref
refl
appThm
nil
9
ref
740
remove
nil
cons
cons
nil
cons
nil
cons
cons
169
ref
subst
trans
appThm
228
remove
trans
appThm
657
remove
226
remove
795
remove
744
remove
refl
appThm
appThm
appThm
768
remove
appThm
appThm
nil
86
ref
538
ref
182
ref
747
ref
appTerm
appTerm
747
ref
appTerm
nil
cons
796
def
cons
nil
cons
nil
cons
cons
606
remove
subst
trans
sym
nil
51
ref
55
ref
747
ref
appTerm
797
def
204
ref
appTerm
798
def
nil
cons
799
def
cons
52
ref
796
ref
cons
nil
cons
800
def
cons
nil
cons
cons
801
def
73
ref
subst
801
remove
131
ref
subst
55
ref
"_630"
3
ref
var
802
def
538
ref
182
ref
802
remove
varTerm
803
def
appTerm
appTerm
803
remove
appTerm
absTerm
804
def
747
ref
appTerm
805
def
appTerm
refl
806
def
804
ref
204
ref
appTerm
betaConv
appThm
102
remove
805
remove
betaConv
appThm
807
def
654
remove
204
ref
appTerm
refl
appThm
trans
804
remove
refl
808
def
798
remove
assume
appThm
eqMp
sym
nil
86
ref
285
remove
nil
cons
cons
nil
cons
nil
cons
cons
86
ref
55
ref
538
ref
89
ref
appTerm
809
def
204
ref
appTerm
appTerm
89
ref
appTerm
absTerm
810
def
89
ref
appTerm
811
def
betaConv
nil
173
ref
810
ref
appTerm
812
def
axiom
nil
51
ref
812
remove
nil
cons
cons
52
ref
811
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
810
remove
nil
cons
cons
178
ref
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
subst
286
remove
trans
sym
92
ref
eqMp
eqMp
eqMp
nil
99
ref
799
ref
cons
100
ref
796
ref
cons
nil
cons
813
def
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
nil
51
ref
797
remove
78
ref
appTerm
814
def
nil
cons
815
def
cons
800
remove
cons
nil
cons
cons
816
def
73
ref
subst
816
remove
131
ref
subst
806
remove
"_628"
3
remove
var
817
def
538
remove
182
remove
817
remove
varTerm
818
def
appTerm
appTerm
818
remove
appTerm
absTerm
78
ref
appTerm
betaConv
appThm
807
remove
666
remove
78
ref
appTerm
refl
appThm
trans
808
remove
814
remove
assume
appThm
eqMp
sym
nil
86
ref
227
remove
nil
cons
cons
nil
cons
nil
cons
cons
86
ref
55
ref
809
ref
78
ref
appTerm
appTerm
78
remove
appTerm
absTerm
819
def
89
remove
appTerm
820
def
betaConv
nil
173
ref
819
ref
appTerm
821
def
axiom
nil
51
ref
821
remove
nil
cons
cons
52
ref
820
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
819
remove
nil
cons
cons
178
remove
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
subst
sym
92
ref
eqMp
eqMp
eqMp
nil
99
ref
815
remove
cons
822
def
813
remove
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
539
remove
747
remove
appTerm
823
def
betaConv
542
remove
nil
543
remove
52
ref
823
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
544
remove
177
ref
748
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
nil
822
remove
100
ref
799
remove
cons
547
ref
796
remove
cons
nil
cons
cons
cons
nil
cons
cons
561
ref
subst
proveHyp
proveHyp
proveHyp
eqMp
eqMp
nil
792
ref
793
remove
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
86
ref
809
remove
205
remove
appTerm
absTerm
824
def
741
remove
appTerm
825
def
betaConv
nil
173
ref
824
ref
appTerm
826
def
axiom
nil
51
ref
826
remove
nil
cons
cons
52
ref
825
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
ref
176
ref
824
remove
nil
cons
cons
177
ref
766
remove
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
nil
792
remove
100
ref
750
remove
cons
547
remove
789
remove
cons
nil
cons
cons
cons
nil
cons
cons
561
remove
subst
proveHyp
proveHyp
proveHyp
eqMp
eqMp
subst
eqMp
nil
51
ref
489
remove
cons
827
def
222
remove
cons
nil
cons
cons
120
ref
subst
proveHyp
nil
827
remove
nil
cons
nil
cons
cons
55
ref
201
remove
appTerm
refl
88
remove
209
remove
subst
appThm
nil
177
ref
202
remove
cons
nil
cons
nil
cons
cons
217
remove
subst
trans
sym
92
ref
eqMp
subst
572
remove
276
remove
subst
eqMp
eqMp
eqMp
nil
99
ref
570
remove
cons
100
ref
221
remove
cons
nil
cons
828
def
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
99
ref
568
remove
cons
828
ref
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
51
ref
46
ref
145
ref
56
ref
564
ref
145
remove
varTerm
appTerm
appTerm
204
ref
appTerm
absTerm
appTerm
nil
cons
cons
52
ref
56
ref
565
remove
appTerm
204
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
143
ref
144
ref
564
remove
nil
cons
cons
828
ref
cons
nil
cons
cons
nil
51
ref
7
ref
9
ref
56
ref
128
remove
appTerm
829
def
105
ref
appTerm
absTerm
appTerm
nil
cons
830
def
cons
831
def
52
ref
56
ref
475
ref
125
ref
appTerm
832
def
appTerm
833
def
105
ref
appTerm
nil
cons
834
def
cons
nil
cons
cons
nil
cons
cons
835
def
73
ref
subst
835
remove
131
ref
subst
nil
51
ref
832
ref
nil
cons
836
def
cons
837
def
52
ref
105
ref
nil
cons
838
def
cons
nil
cons
839
def
cons
nil
cons
cons
840
def
73
ref
subst
840
remove
131
ref
subst
nil
831
remove
839
remove
cons
nil
cons
cons
120
ref
subst
52
ref
56
ref
7
ref
9
ref
829
remove
59
ref
appTerm
absTerm
appTerm
appTerm
59
ref
appTerm
absTerm
841
def
105
remove
appTerm
842
def
betaConv
nil
837
remove
52
ref
173
ref
841
ref
appTerm
843
def
nil
cons
844
def
cons
nil
cons
cons
nil
cons
cons
845
def
120
ref
subst
55
remove
832
remove
appTerm
846
def
refl
133
remove
173
remove
52
ref
56
ref
7
ref
9
ref
56
ref
476
remove
appTerm
59
ref
appTerm
absTerm
appTerm
appTerm
59
remove
appTerm
absTerm
appTerm
absTerm
847
def
125
remove
appTerm
betaConv
appThm
nil
138
remove
475
remove
appTerm
847
remove
appTerm
axiom
139
remove
appThm
eqMp
nil
51
ref
846
remove
843
ref
appTerm
nil
cons
cons
52
ref
833
remove
843
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
845
remove
nil
51
ref
266
remove
nil
cons
848
def
cons
52
ref
272
ref
cons
nil
cons
cons
nil
cons
cons
849
def
73
ref
subst
849
remove
131
ref
subst
271
remove
eqMp
nil
99
ref
848
remove
cons
100
ref
272
remove
cons
nil
cons
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
51
ref
844
remove
cons
52
ref
842
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
175
remove
176
remove
841
remove
nil
cons
cons
177
remove
838
ref
cons
nil
cons
cons
nil
cons
cons
142
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
99
ref
836
remove
cons
100
ref
838
remove
cons
nil
cons
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
eqMp
nil
99
ref
830
remove
cons
100
ref
834
remove
cons
nil
cons
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
eqMp
nil
99
ref
413
remove
cons
828
ref
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
99
ref
399
remove
cons
100
ref
460
remove
cons
nil
cons
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
eqMp
nil
99
ref
423
remove
cons
100
ref
458
remove
cons
nil
cons
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
eqMp
nil
99
ref
427
remove
cons
100
ref
456
remove
cons
nil
cons
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
eqMp
nil
99
ref
435
remove
cons
100
ref
454
remove
cons
nil
cons
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
eqMp
nil
99
ref
439
remove
cons
100
ref
452
remove
cons
nil
cons
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
eqMp
nil
99
ref
219
remove
cons
850
def
100
ref
450
remove
cons
nil
cons
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
eqMp
nil
850
remove
828
remove
cons
nil
cons
cons
114
ref
subst
deductAntisym
eqMp
eqMp
nil
198
remove
thm
400
remove
nil
398
remove
thm
nil
144
ref
336
ref
46
ref
335
ref
12
ref
27
ref
340
remove
appTerm
appTerm
37
ref
341
remove
appTerm
27
ref
337
remove
appTerm
851
def
appTerm
27
ref
339
ref
appTerm
appTerm
appTerm
absTerm
852
def
appTerm
853
def
absTerm
854
def
nil
cons
cons
nil
cons
nil
cons
cons
251
ref
subst
336
remove
nil
86
ref
853
remove
nil
cons
855
def
cons
nil
cons
nil
cons
cons
93
ref
subst
13
ref
229
remove
nil
181
ref
348
remove
cons
nil
cons
nil
cons
cons
856
def
181
ref
184
remove
294
remove
19
ref
appTerm
appTerm
185
ref
appTerm
absTerm
857
def
185
ref
appTerm
858
def
betaConv
nil
46
ref
857
ref
appTerm
859
def
axiom
nil
51
ref
859
remove
nil
cons
cons
52
ref
858
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
120
ref
subst
proveHyp
143
remove
144
ref
857
remove
nil
cons
cons
305
remove
cons
nil
cons
cons
142
remove
subst
eqMp
eqMp
subst
appThm
appThm
150
remove
851
ref
refl
860
def
appThm
152
remove
appThm
nil
154
remove
155
ref
851
ref
nil
cons
861
def
cons
nil
cons
862
def
cons
nil
cons
cons
166
remove
subst
trans
appThm
nil
9
ref
861
remove
cons
nil
cons
nil
cons
cons
169
ref
subst
trans
sym
92
ref
eqMp
nil
51
ref
12
ref
27
ref
338
ref
19
ref
appTerm
appTerm
appTerm
37
ref
149
remove
appTerm
851
ref
appTerm
151
remove
appTerm
appTerm
863
def
nil
cons
cons
52
ref
7
ref
22
ref
46
ref
17
ref
56
remove
12
ref
27
ref
338
ref
34
ref
appTerm
appTerm
appTerm
40
remove
851
ref
appTerm
41
remove
appTerm
appTerm
864
def
appTerm
12
ref
27
ref
338
remove
35
ref
appTerm
appTerm
appTerm
37
ref
350
remove
appTerm
851
remove
appTerm
36
ref
appTerm
appTerm
865
def
appTerm
866
def
absTerm
867
def
appTerm
868
def
absTerm
869
def
appTerm
870
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
131
ref
subst
proveHyp
nil
123
ref
869
remove
nil
cons
cons
nil
cons
nil
cons
cons
250
ref
subst
22
ref
nil
86
ref
868
remove
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
nil
144
ref
867
remove
nil
cons
cons
nil
cons
nil
cons
cons
251
ref
subst
17
ref
nil
86
ref
866
remove
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
nil
51
ref
864
remove
nil
cons
871
def
cons
52
ref
865
remove
nil
cons
872
def
cons
nil
cons
cons
nil
cons
cons
873
def
73
remove
subst
873
remove
131
remove
subst
13
ref
856
remove
383
remove
subst
appThm
148
ref
358
ref
appThm
860
remove
appThm
36
ref
refl
appThm
nil
153
ref
36
remove
nil
cons
874
def
cons
862
remove
cons
nil
cons
cons
370
ref
subst
trans
appThm
nil
9
ref
874
remove
cons
nil
cons
nil
cons
cons
169
ref
subst
trans
sym
92
ref
eqMp
eqMp
nil
99
remove
871
remove
cons
100
remove
872
remove
cons
nil
cons
cons
nil
cons
cons
114
remove
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
51
remove
62
remove
863
remove
appTerm
870
remove
appTerm
nil
cons
cons
52
remove
855
remove
cons
nil
cons
cons
nil
cons
cons
120
remove
subst
proveHyp
225
ref
373
remove
852
ref
19
remove
appTerm
betaConv
appThm
8
ref
22
ref
374
ref
17
ref
225
remove
852
ref
34
remove
appTerm
betaConv
appThm
852
ref
35
remove
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
374
ref
335
remove
852
ref
339
remove
appTerm
betaConv
absThm
appThm
appThm
nil
375
remove
852
remove
nil
cons
cons
nil
cons
nil
cons
cons
381
remove
subst
eqMp
eqMp
eqMp
absThm
eqMp
nil
46
ref
854
remove
appTerm
thm
8
ref
"x1"
2
ref
var
875
def
8
remove
"x2"
2
remove
var
876
def
374
remove
181
ref
13
remove
nil
17
ref
31
ref
876
ref
varTerm
877
def
appTerm
185
ref
appTerm
878
def
nil
cons
cons
22
ref
875
ref
varTerm
879
def
nil
cons
880
def
cons
nil
cons
cons
nil
cons
cons
147
ref
subst
148
remove
nil
17
ref
304
remove
cons
22
ref
877
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
881
def
358
remove
subst
appThm
879
ref
refl
appThm
881
remove
147
remove
subst
882
def
appThm
nil
153
remove
37
remove
39
remove
185
remove
appTerm
appTerm
877
remove
appTerm
195
remove
appTerm
nil
cons
883
def
cons
155
remove
880
remove
cons
nil
cons
cons
nil
cons
cons
370
remove
subst
trans
trans
appThm
882
remove
appThm
nil
9
remove
883
remove
cons
nil
cons
nil
cons
cons
169
remove
subst
trans
absThm
appThm
170
remove
224
remove
179
remove
subst
subst
trans
absThm
appThm
180
ref
trans
absThm
appThm
180
remove
trans
sym
92
remove
eqMp
nil
7
ref
875
remove
7
ref
876
remove
46
ref
181
remove
12
remove
27
ref
31
remove
879
remove
appTerm
878
ref
appTerm
appTerm
appTerm
27
remove
878
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
thm
nil
123
remove
22
ref
46
remove
17
ref
371
remove
absTerm
884
def
appTerm
885
def
absTerm
886
def
nil
cons
cons
nil
cons
nil
cons
cons
250
remove
subst
22
remove
nil
86
ref
885
remove
nil
cons
cons
nil
cons
nil
cons
cons
93
ref
subst
nil
144
remove
884
remove
nil
cons
cons
nil
cons
nil
cons
cons
251
remove
subst
17
remove
nil
86
remove
372
remove
cons
nil
cons
nil
cons
cons
93
remove
subst
382
remove
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
7
remove
886
remove
appTerm
thm