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