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