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