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