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