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