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