article list-append-thm.art

Article list-append-thm.art

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