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