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