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