6
version
nil
"g"
"->"
typeOp
0
def
"Data.Option.option"
typeOp
1
def
"A"
varType
2
def
nil
cons
3
def
opType
4
def
4
ref
nil
cons
5
def
cons
opType
6
def
var
"Function.id"
const
7
def
6
ref
constTerm
8
def
nil
cons
cons
"f"
6
ref
var
"Data.Option.map"
const
9
def
0
ref
0
ref
2
ref
3
ref
cons
opType
10
def
6
ref
nil
cons
cons
opType
constTerm
7
remove
10
ref
constTerm
11
def
appTerm
12
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
"A"
5
ref
cons
13
def
"B"
5
ref
cons
nil
cons
cons
nil
nil
cons
14
def
cons
"g"
0
ref
2
ref
"B"
varType
15
def
nil
cons
16
def
cons
opType
17
def
var
18
def
"="
const
19
def
0
ref
"bool"
typeOp
nil
opType
20
def
0
ref
20
ref
20
ref
nil
cons
21
def
cons
opType
22
def
nil
cons
cons
opType
23
def
constTerm
24
def
19
ref
0
ref
17
ref
0
ref
17
ref
21
ref
cons
opType
25
def
nil
cons
cons
opType
constTerm
"f"
17
ref
var
26
def
varTerm
27
def
appTerm
18
ref
varTerm
28
def
appTerm
29
def
appTerm
"Data.Bool.!"
const
30
def
0
ref
0
ref
2
ref
21
ref
cons
opType
31
def
21
ref
cons
opType
32
def
constTerm
33
def
"x"
2
ref
var
34
def
19
ref
0
ref
15
ref
0
ref
15
ref
21
ref
cons
opType
nil
cons
cons
opType
constTerm
27
ref
34
ref
varTerm
35
def
appTerm
appTerm
28
ref
35
ref
appTerm
36
def
appTerm
absTerm
appTerm
37
def
appTerm
absTerm
38
def
28
ref
appTerm
39
def
betaConv
26
ref
30
ref
0
ref
25
ref
21
ref
cons
opType
constTerm
40
def
38
ref
appTerm
41
def
absTerm
42
def
27
ref
appTerm
43
def
betaConv
40
ref
refl
44
def
26
ref
44
ref
18
ref
nil
"y"
20
ref
var
45
def
37
ref
nil
cons
cons
"x"
20
ref
var
46
def
29
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
"A"
21
ref
cons
nil
cons
47
def
14
ref
cons
"y"
2
ref
var
48
def
24
ref
19
ref
0
ref
2
ref
31
ref
nil
cons
cons
opType
constTerm
49
def
35
ref
appTerm
50
def
48
remove
varTerm
51
def
appTerm
appTerm
49
ref
51
ref
appTerm
35
ref
appTerm
appTerm
absTerm
52
def
51
ref
appTerm
53
def
betaConv
34
ref
33
ref
52
ref
appTerm
54
def
absTerm
55
def
35
ref
appTerm
56
def
betaConv
nil
33
ref
55
ref
appTerm
57
def
axiom
nil
"p"
20
ref
var
58
def
57
remove
nil
cons
cons
"q"
20
ref
var
59
def
56
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
24
ref
"Data.Bool.==>"
const
23
ref
constTerm
60
def
58
ref
varTerm
61
def
appTerm
62
def
59
ref
varTerm
63
def
appTerm
64
def
appTerm
refl
58
ref
59
ref
24
ref
"Data.Bool./\\"
const
23
ref
constTerm
65
def
61
ref
appTerm
66
def
63
ref
appTerm
67
def
appTerm
68
def
61
ref
appTerm
absTerm
69
def
absTerm
70
def
61
ref
appTerm
betaConv
63
ref
refl
71
def
appThm
69
remove
63
ref
appTerm
betaConv
trans
appThm
nil
19
ref
0
ref
23
ref
0
ref
23
ref
21
ref
cons
opType
72
def
nil
cons
cons
opType
constTerm
73
def
60
ref
appTerm
70
remove
appTerm
axiom
61
ref
refl
74
def
appThm
71
ref
appThm
eqMp
75
def
sym
76
def
68
remove
refl
59
ref
19
ref
0
ref
72
ref
0
ref
72
remove
21
ref
cons
opType
nil
cons
cons
opType
constTerm
77
def
"f"
23
ref
var
78
def
78
ref
varTerm
79
def
61
ref
appTerm
63
ref
appTerm
absTerm
80
def
appTerm
78
ref
79
ref
"Data.Bool.T"
const
20
ref
constTerm
81
def
appTerm
81
ref
appTerm
absTerm
82
def
appTerm
absTerm
83
def
63
ref
appTerm
betaConv
appThm
19
ref
0
ref
22
ref
0
ref
22
ref
21
ref
cons
opType
84
def
nil
cons
cons
opType
constTerm
85
def
66
remove
appTerm
refl
58
ref
83
remove
absTerm
86
def
61
ref
appTerm
betaConv
appThm
nil
73
ref
65
ref
appTerm
86
ref
appTerm
axiom
87
def
74
remove
appThm
eqMp
71
ref
appThm
eqMp
88
def
sym
78
ref
79
ref
refl
nil
"t"
20
ref
var
89
def
61
ref
nil
cons
90
def
cons
nil
cons
nil
cons
cons
24
ref
89
ref
varTerm
91
def
appTerm
92
def
81
ref
appTerm
93
def
assume
sym
nil
81
ref
axiom
94
def
eqMp
91
ref
assume
94
ref
deductAntisym
deductAntisym
95
def
subst
61
ref
assume
96
def
eqMp
appThm
nil
89
ref
63
ref
nil
cons
97
def
cons
nil
cons
nil
cons
cons
95
ref
subst
63
ref
assume
eqMp
appThm
absThm
eqMp
98
def
nil
"P"
20
ref
var
99
def
90
remove
cons
"Q"
20
ref
var
100
def
97
remove
cons
nil
cons
cons
nil
cons
cons
24
ref
refl
101
def
78
ref
79
remove
99
ref
varTerm
102
def
appTerm
103
def
100
ref
varTerm
104
def
appTerm
absTerm
58
ref
59
ref
61
ref
absTerm
absTerm
105
def
appTerm
betaConv
105
ref
102
ref
appTerm
betaConv
104
ref
refl
106
def
appThm
59
ref
102
ref
absTerm
104
ref
appTerm
betaConv
trans
trans
appThm
82
ref
105
ref
appTerm
betaConv
105
ref
81
ref
appTerm
betaConv
81
ref
refl
107
def
appThm
59
ref
81
ref
absTerm
81
ref
appTerm
betaConv
trans
trans
appThm
24
ref
65
ref
102
ref
appTerm
108
def
104
ref
appTerm
109
def
appTerm
refl
59
ref
77
remove
78
remove
103
remove
63
ref
appTerm
absTerm
appTerm
82
ref
appTerm
absTerm
104
ref
appTerm
betaConv
appThm
85
ref
108
remove
appTerm
refl
86
remove
102
ref
appTerm
betaConv
appThm
87
remove
102
ref
refl
110
def
appThm
eqMp
106
ref
appThm
eqMp
109
remove
assume
eqMp
105
remove
refl
appThm
eqMp
sym
94
ref
eqMp
111
def
subst
112
def
deductAntisym
eqMp
75
remove
64
ref
assume
eqMp
sym
96
ref
eqMp
101
ref
80
remove
58
ref
59
ref
63
ref
absTerm
113
def
absTerm
114
def
appTerm
betaConv
114
ref
61
ref
appTerm
betaConv
71
remove
appThm
113
ref
63
ref
appTerm
betaConv
trans
trans
appThm
82
remove
114
ref
appTerm
betaConv
114
ref
81
ref
appTerm
betaConv
107
remove
appThm
113
remove
81
ref
appTerm
betaConv
trans
trans
appThm
88
remove
67
remove
assume
eqMp
114
remove
refl
appThm
eqMp
sym
94
ref
eqMp
115
def
proveHyp
deductAntisym
116
def
subst
proveHyp
"A"
3
ref
cons
117
def
nil
cons
118
def
"P"
31
ref
var
119
def
55
remove
nil
cons
cons
34
ref
35
ref
nil
cons
cons
nil
cons
120
def
cons
nil
cons
cons
nil
58
ref
33
ref
119
ref
varTerm
121
def
appTerm
122
def
nil
cons
123
def
cons
59
ref
121
ref
35
ref
appTerm
124
def
nil
cons
125
def
cons
nil
cons
cons
nil
cons
cons
126
def
76
ref
subst
126
remove
115
remove
98
remove
deductAntisym
127
def
subst
24
ref
124
ref
appTerm
refl
34
ref
81
ref
absTerm
128
def
35
ref
appTerm
betaConv
appThm
"p"
31
ref
var
129
def
19
ref
0
ref
31
remove
32
ref
nil
cons
cons
opType
constTerm
129
ref
varTerm
130
def
appTerm
128
remove
appTerm
absTerm
131
def
121
ref
appTerm
betaConv
132
def
nil
19
ref
0
ref
32
ref
0
ref
32
ref
21
ref
cons
opType
nil
cons
cons
opType
constTerm
133
def
33
ref
appTerm
131
remove
appTerm
axiom
121
ref
refl
134
def
appThm
135
def
122
ref
assume
eqMp
eqMp
35
ref
refl
136
def
appThm
eqMp
sym
94
ref
eqMp
eqMp
nil
99
ref
123
remove
cons
100
ref
125
remove
cons
nil
cons
cons
nil
cons
cons
111
ref
subst
deductAntisym
eqMp
137
def
subst
eqMp
eqMp
nil
58
ref
54
remove
nil
cons
cons
59
ref
53
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
118
ref
119
ref
52
remove
nil
cons
cons
34
ref
51
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
subst
subst
absThm
appThm
absThm
appThm
sym
nil
40
ref
26
ref
40
ref
18
ref
24
ref
37
remove
appTerm
29
remove
appTerm
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
58
ref
40
ref
42
ref
appTerm
nil
cons
cons
59
ref
43
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
"A"
17
ref
nil
cons
cons
nil
cons
138
def
"P"
25
remove
var
139
def
42
remove
nil
cons
cons
"x"
17
ref
var
140
def
27
ref
nil
cons
cons
nil
cons
141
def
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
nil
58
ref
41
remove
nil
cons
cons
59
ref
39
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
138
ref
139
ref
38
remove
nil
cons
cons
140
remove
28
ref
nil
cons
142
def
cons
nil
cons
143
def
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
144
def
subst
subst
30
ref
0
ref
0
ref
4
ref
21
ref
cons
opType
145
def
21
ref
cons
opType
constTerm
146
def
refl
147
def
"x"
4
ref
var
148
def
19
ref
0
ref
4
ref
145
ref
nil
cons
cons
opType
constTerm
149
def
12
ref
148
ref
varTerm
150
def
appTerm
appTerm
151
def
refl
13
ref
nil
cons
152
def
14
ref
cons
153
def
34
ref
49
remove
11
ref
35
ref
appTerm
appTerm
35
ref
appTerm
absTerm
154
def
35
ref
appTerm
155
def
betaConv
nil
33
ref
154
ref
appTerm
156
def
axiom
nil
58
ref
156
remove
nil
cons
cons
59
ref
155
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
118
ref
119
ref
154
remove
nil
cons
cons
120
ref
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
157
def
subst
appThm
absThm
appThm
trans
sym
nil
"P"
145
remove
var
158
def
148
ref
151
remove
150
ref
appTerm
159
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
153
ref
24
ref
122
remove
appTerm
refl
132
remove
appThm
135
remove
eqMp
sym
160
def
subst
161
def
subst
148
ref
nil
89
ref
159
ref
nil
cons
162
def
cons
nil
cons
nil
cons
cons
95
ref
subst
148
ref
"Data.Bool.\\/"
const
23
remove
constTerm
163
def
149
ref
150
ref
appTerm
164
def
"Data.Option.none"
const
165
def
4
ref
constTerm
166
def
appTerm
167
def
appTerm
"Data.Bool.?"
const
32
remove
constTerm
168
def
"a"
2
ref
var
169
def
164
remove
"Data.Option.some"
const
170
def
0
ref
2
ref
5
remove
cons
opType
constTerm
171
def
169
ref
varTerm
172
def
appTerm
173
def
appTerm
174
def
absTerm
175
def
appTerm
176
def
appTerm
177
def
absTerm
178
def
150
ref
appTerm
179
def
betaConv
nil
146
ref
178
ref
appTerm
180
def
axiom
nil
58
ref
180
remove
nil
cons
cons
59
ref
179
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
152
remove
158
ref
178
remove
nil
cons
cons
148
ref
150
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
181
def
nil
58
ref
177
ref
nil
cons
cons
182
def
59
ref
162
ref
cons
nil
cons
183
def
cons
nil
cons
cons
116
ref
subst
proveHyp
nil
58
ref
167
ref
nil
cons
184
def
cons
185
def
183
ref
cons
nil
cons
cons
186
def
76
ref
subst
186
remove
127
ref
subst
149
remove
refl
187
def
12
ref
refl
188
def
167
ref
assume
189
def
appThm
nil
"f"
10
remove
var
11
remove
nil
cons
cons
nil
cons
nil
cons
cons
190
def
117
ref
"B"
3
remove
cons
nil
cons
cons
14
ref
cons
191
def
26
ref
19
ref
0
ref
1
ref
16
ref
opType
192
def
0
ref
192
ref
21
ref
cons
opType
nil
cons
cons
opType
constTerm
193
def
9
ref
0
ref
17
ref
0
ref
4
ref
192
ref
nil
cons
194
def
cons
opType
195
def
nil
cons
cons
opType
constTerm
196
def
27
ref
appTerm
197
def
166
ref
appTerm
appTerm
165
ref
192
ref
constTerm
appTerm
absTerm
198
def
27
ref
appTerm
199
def
betaConv
nil
40
ref
198
ref
appTerm
200
def
axiom
nil
58
ref
200
remove
nil
cons
cons
59
ref
199
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
138
ref
139
ref
198
remove
nil
cons
cons
141
ref
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
201
def
subst
subst
trans
appThm
189
ref
appThm
nil
148
ref
166
remove
nil
cons
cons
nil
cons
nil
cons
cons
153
ref
nil
89
ref
50
remove
35
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
95
ref
subst
136
remove
eqMp
202
def
subst
203
def
subst
trans
sym
94
ref
eqMp
eqMp
nil
99
ref
184
ref
cons
204
def
100
ref
162
ref
cons
nil
cons
205
def
cons
nil
cons
cons
111
ref
subst
deductAntisym
eqMp
nil
58
ref
60
ref
167
remove
appTerm
206
def
159
ref
appTerm
207
def
nil
cons
cons
59
ref
60
ref
176
ref
appTerm
208
def
159
ref
appTerm
209
def
nil
cons
cons
nil
cons
210
def
cons
nil
cons
cons
127
ref
subst
proveHyp
nil
119
ref
169
ref
60
ref
175
ref
172
ref
appTerm
211
def
appTerm
212
def
159
ref
appTerm
213
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
160
ref
subst
169
ref
nil
89
ref
213
remove
nil
cons
cons
nil
cons
nil
cons
cons
95
ref
subst
nil
58
ref
211
ref
nil
cons
214
def
cons
215
def
183
ref
cons
nil
cons
cons
216
def
76
ref
subst
216
remove
127
ref
subst
211
ref
betaConv
211
remove
assume
eqMp
217
def
nil
58
ref
174
ref
nil
cons
218
def
cons
219
def
183
remove
cons
nil
cons
cons
220
def
116
ref
subst
proveHyp
220
ref
76
ref
subst
220
remove
127
ref
subst
187
remove
188
remove
174
remove
assume
221
def
appThm
190
remove
191
remove
169
ref
193
remove
197
remove
173
ref
appTerm
appTerm
170
ref
0
ref
15
ref
194
ref
cons
opType
constTerm
27
ref
172
ref
appTerm
appTerm
appTerm
absTerm
222
def
172
ref
appTerm
223
def
betaConv
26
ref
33
ref
222
ref
appTerm
224
def
absTerm
225
def
27
remove
appTerm
226
def
betaConv
nil
40
ref
225
ref
appTerm
227
def
axiom
nil
58
ref
227
remove
nil
cons
cons
59
ref
226
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
138
ref
139
ref
225
remove
nil
cons
cons
141
remove
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
nil
58
ref
224
remove
nil
cons
cons
59
ref
223
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
118
ref
119
ref
222
remove
nil
cons
cons
34
ref
172
ref
nil
cons
cons
nil
cons
228
def
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
229
def
subst
subst
171
remove
refl
nil
228
remove
nil
cons
cons
230
def
157
remove
subst
appThm
trans
trans
appThm
221
ref
appThm
nil
148
ref
173
remove
nil
cons
cons
nil
cons
nil
cons
cons
203
remove
subst
trans
sym
94
ref
eqMp
eqMp
nil
99
ref
218
remove
cons
231
def
205
ref
cons
nil
cons
cons
111
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
99
ref
214
remove
cons
232
def
205
ref
cons
nil
cons
cons
111
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
58
ref
33
ref
34
ref
60
ref
175
ref
35
ref
appTerm
appTerm
233
def
159
ref
appTerm
absTerm
appTerm
nil
cons
cons
210
remove
cons
nil
cons
cons
116
ref
subst
proveHyp
118
ref
119
ref
175
remove
nil
cons
cons
234
def
205
remove
cons
nil
cons
cons
nil
58
ref
33
ref
34
ref
60
ref
124
remove
appTerm
235
def
104
ref
appTerm
absTerm
appTerm
nil
cons
236
def
cons
237
def
59
ref
60
ref
168
ref
121
ref
appTerm
238
def
appTerm
239
def
104
ref
appTerm
nil
cons
240
def
cons
nil
cons
cons
nil
cons
cons
241
def
76
ref
subst
241
remove
127
ref
subst
nil
58
ref
238
ref
nil
cons
242
def
cons
243
def
59
ref
104
ref
nil
cons
244
def
cons
nil
cons
245
def
cons
nil
cons
cons
246
def
76
ref
subst
246
remove
127
ref
subst
nil
237
remove
245
remove
cons
nil
cons
cons
116
ref
subst
59
ref
60
ref
33
ref
34
ref
235
remove
63
ref
appTerm
absTerm
appTerm
appTerm
63
ref
appTerm
absTerm
247
def
104
ref
appTerm
248
def
betaConv
nil
243
remove
59
ref
30
ref
84
remove
constTerm
249
def
247
ref
appTerm
250
def
nil
cons
251
def
cons
nil
cons
cons
nil
cons
cons
252
def
116
ref
subst
24
ref
238
remove
appTerm
253
def
refl
129
remove
249
ref
59
ref
60
ref
33
ref
34
ref
60
ref
130
remove
35
ref
appTerm
appTerm
63
ref
appTerm
absTerm
appTerm
appTerm
63
ref
appTerm
absTerm
appTerm
absTerm
254
def
121
remove
appTerm
betaConv
appThm
nil
133
remove
168
remove
appTerm
254
remove
appTerm
axiom
134
remove
appThm
eqMp
nil
58
ref
253
remove
250
ref
appTerm
nil
cons
cons
59
ref
239
remove
250
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
252
remove
nil
58
ref
24
ref
61
remove
appTerm
63
ref
appTerm
255
def
nil
cons
256
def
cons
59
ref
64
remove
nil
cons
257
def
cons
nil
cons
cons
nil
cons
cons
258
def
76
ref
subst
258
remove
127
ref
subst
76
ref
127
ref
255
remove
assume
96
remove
eqMp
eqMp
112
remove
deductAntisym
eqMp
eqMp
nil
99
ref
256
remove
cons
100
ref
257
remove
cons
nil
cons
cons
nil
cons
cons
111
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
58
ref
251
remove
cons
59
ref
248
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
47
ref
"P"
22
ref
var
259
def
247
remove
nil
cons
cons
46
ref
244
ref
cons
nil
cons
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
99
ref
242
remove
cons
100
ref
244
remove
cons
nil
cons
cons
nil
cons
cons
111
ref
subst
deductAntisym
eqMp
eqMp
nil
99
ref
236
remove
cons
100
ref
240
remove
cons
nil
cons
cons
nil
cons
cons
111
ref
subst
deductAntisym
eqMp
260
def
subst
eqMp
eqMp
nil
58
ref
65
ref
207
remove
appTerm
209
remove
appTerm
nil
cons
cons
59
ref
60
ref
177
remove
appTerm
261
def
159
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
nil
"z"
20
ref
var
262
def
162
remove
cons
45
ref
176
remove
nil
cons
cons
46
ref
184
remove
cons
nil
cons
cons
263
def
cons
nil
cons
cons
nil
58
ref
24
ref
46
ref
varTerm
264
def
appTerm
265
def
"Data.Bool.F"
const
20
ref
constTerm
266
def
appTerm
267
def
nil
cons
268
def
cons
59
ref
60
ref
65
ref
60
ref
264
ref
appTerm
262
ref
varTerm
269
def
appTerm
appTerm
60
ref
45
remove
varTerm
270
def
appTerm
271
def
269
ref
appTerm
272
def
appTerm
appTerm
60
ref
163
ref
264
ref
appTerm
270
ref
appTerm
appTerm
269
ref
appTerm
appTerm
nil
cons
273
def
cons
nil
cons
274
def
cons
nil
cons
cons
275
def
76
ref
subst
275
remove
127
ref
subst
24
ref
"_15640"
20
ref
var
276
def
60
ref
65
ref
60
ref
276
remove
varTerm
277
def
appTerm
269
ref
appTerm
appTerm
272
ref
appTerm
appTerm
60
ref
163
ref
277
remove
appTerm
270
ref
appTerm
appTerm
269
ref
appTerm
appTerm
absTerm
278
def
264
ref
appTerm
279
def
appTerm
refl
280
def
278
ref
266
ref
appTerm
betaConv
appThm
101
ref
279
remove
betaConv
appThm
281
def
60
ref
65
ref
60
ref
266
ref
appTerm
282
def
269
ref
appTerm
appTerm
272
ref
appTerm
appTerm
60
ref
163
ref
266
ref
appTerm
283
def
270
ref
appTerm
appTerm
269
ref
appTerm
appTerm
refl
appThm
trans
278
remove
refl
284
def
267
remove
assume
appThm
eqMp
sym
60
ref
refl
285
def
65
ref
refl
286
def
nil
89
ref
269
ref
nil
cons
287
def
cons
nil
cons
nil
cons
cons
288
def
89
ref
24
ref
282
remove
91
ref
appTerm
appTerm
81
ref
appTerm
absTerm
289
def
91
ref
appTerm
290
def
betaConv
nil
249
ref
289
ref
appTerm
291
def
axiom
nil
58
ref
291
remove
nil
cons
cons
59
ref
290
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
47
ref
259
ref
289
remove
nil
cons
cons
46
ref
91
ref
nil
cons
cons
nil
cons
292
def
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
subst
appThm
272
ref
refl
293
def
appThm
nil
89
ref
272
ref
nil
cons
cons
nil
cons
nil
cons
cons
294
def
89
ref
24
ref
65
ref
81
ref
appTerm
295
def
91
ref
appTerm
appTerm
91
ref
appTerm
absTerm
296
def
91
ref
appTerm
297
def
betaConv
nil
249
ref
296
ref
appTerm
298
def
axiom
nil
58
ref
298
remove
nil
cons
cons
59
ref
297
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
47
ref
259
ref
296
remove
nil
cons
cons
292
ref
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
subst
trans
appThm
285
ref
nil
89
ref
270
ref
nil
cons
cons
nil
cons
nil
cons
cons
299
def
89
ref
24
ref
283
remove
91
ref
appTerm
appTerm
91
ref
appTerm
absTerm
300
def
91
ref
appTerm
301
def
betaConv
nil
249
ref
300
ref
appTerm
302
def
axiom
nil
58
ref
302
remove
nil
cons
cons
59
ref
301
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
47
ref
259
ref
300
remove
nil
cons
cons
292
ref
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
subst
appThm
269
ref
refl
303
def
appThm
appThm
294
remove
nil
89
ref
60
ref
91
ref
appTerm
304
def
91
ref
appTerm
305
def
nil
cons
cons
nil
cons
nil
cons
cons
95
ref
subst
89
ref
305
remove
absTerm
306
def
91
ref
appTerm
307
def
betaConv
nil
249
ref
306
ref
appTerm
308
def
axiom
nil
58
ref
308
remove
nil
cons
cons
59
ref
307
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
47
ref
259
ref
306
remove
nil
cons
cons
292
ref
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
eqMp
subst
trans
sym
94
ref
eqMp
eqMp
eqMp
nil
99
ref
268
ref
cons
100
ref
273
ref
cons
nil
cons
309
def
cons
nil
cons
cons
111
ref
subst
deductAntisym
eqMp
nil
58
ref
265
remove
81
ref
appTerm
310
def
nil
cons
311
def
cons
274
remove
cons
nil
cons
cons
312
def
76
ref
subst
312
remove
127
ref
subst
280
remove
"_15638"
20
ref
var
313
def
60
ref
65
ref
60
ref
313
remove
varTerm
314
def
appTerm
269
ref
appTerm
appTerm
272
ref
appTerm
appTerm
60
ref
163
ref
314
remove
appTerm
270
ref
appTerm
appTerm
269
ref
appTerm
appTerm
absTerm
81
ref
appTerm
betaConv
appThm
281
remove
60
ref
65
ref
60
ref
81
ref
appTerm
315
def
269
ref
appTerm
appTerm
272
ref
appTerm
appTerm
60
ref
163
ref
81
ref
appTerm
316
def
270
remove
appTerm
appTerm
269
ref
appTerm
appTerm
refl
appThm
trans
284
remove
310
remove
assume
appThm
eqMp
sym
285
ref
286
remove
288
remove
89
ref
24
ref
315
remove
91
ref
appTerm
appTerm
91
ref
appTerm
absTerm
317
def
91
ref
appTerm
318
def
betaConv
nil
249
ref
317
ref
appTerm
319
def
axiom
nil
58
ref
319
remove
nil
cons
cons
59
ref
318
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
47
ref
259
ref
317
remove
nil
cons
cons
292
ref
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
subst
320
def
appThm
293
remove
appThm
appThm
285
remove
299
remove
89
ref
24
ref
316
remove
91
ref
appTerm
appTerm
81
ref
appTerm
absTerm
321
def
91
ref
appTerm
322
def
betaConv
nil
249
ref
321
ref
appTerm
323
def
axiom
nil
58
ref
323
remove
nil
cons
cons
59
ref
322
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
47
ref
259
ref
321
remove
nil
cons
cons
292
ref
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
subst
appThm
303
remove
appThm
320
remove
trans
appThm
sym
nil
58
ref
24
ref
269
ref
appTerm
324
def
266
ref
appTerm
325
def
nil
cons
326
def
cons
59
ref
60
ref
65
ref
269
ref
appTerm
272
remove
appTerm
appTerm
269
ref
appTerm
nil
cons
327
def
cons
nil
cons
328
def
cons
nil
cons
cons
329
def
76
ref
subst
329
remove
127
ref
subst
24
ref
"_15644"
20
ref
var
330
def
60
ref
65
ref
330
remove
varTerm
331
def
appTerm
271
ref
331
ref
appTerm
appTerm
appTerm
331
remove
appTerm
absTerm
332
def
269
ref
appTerm
333
def
appTerm
refl
334
def
332
ref
266
ref
appTerm
betaConv
appThm
101
remove
333
remove
betaConv
appThm
335
def
60
ref
65
ref
266
ref
appTerm
336
def
271
ref
266
ref
appTerm
337
def
appTerm
338
def
appTerm
266
ref
appTerm
refl
appThm
trans
332
remove
refl
339
def
325
remove
assume
appThm
eqMp
sym
nil
89
ref
338
remove
nil
cons
cons
nil
cons
nil
cons
cons
89
ref
24
ref
304
ref
266
ref
appTerm
appTerm
"Data.Bool.~"
const
22
remove
constTerm
340
def
91
ref
appTerm
appTerm
absTerm
341
def
91
ref
appTerm
342
def
betaConv
nil
249
ref
341
ref
appTerm
343
def
axiom
nil
58
ref
343
remove
nil
cons
cons
59
ref
342
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
47
ref
259
ref
341
remove
nil
cons
cons
292
ref
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
subst
340
ref
refl
nil
89
ref
337
remove
nil
cons
cons
nil
cons
nil
cons
cons
89
ref
24
ref
336
remove
91
ref
appTerm
appTerm
266
ref
appTerm
absTerm
344
def
91
ref
appTerm
345
def
betaConv
nil
249
ref
344
ref
appTerm
346
def
axiom
nil
58
ref
346
remove
nil
cons
cons
59
ref
345
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
47
ref
259
ref
344
remove
nil
cons
cons
292
ref
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
subst
appThm
nil
24
ref
340
remove
266
ref
appTerm
appTerm
81
ref
appTerm
axiom
trans
trans
sym
94
ref
eqMp
eqMp
eqMp
nil
99
ref
326
ref
cons
100
ref
327
ref
cons
nil
cons
347
def
cons
nil
cons
cons
111
ref
subst
deductAntisym
eqMp
nil
58
ref
324
remove
81
ref
appTerm
348
def
nil
cons
349
def
cons
328
remove
cons
nil
cons
cons
350
def
76
ref
subst
350
remove
127
ref
subst
334
remove
"_15642"
20
ref
var
351
def
60
ref
65
ref
351
remove
varTerm
352
def
appTerm
271
ref
352
ref
appTerm
appTerm
appTerm
352
remove
appTerm
absTerm
81
ref
appTerm
betaConv
appThm
335
remove
60
ref
295
remove
271
remove
81
ref
appTerm
appTerm
353
def
appTerm
81
ref
appTerm
refl
appThm
trans
339
remove
348
remove
assume
appThm
eqMp
sym
nil
89
ref
353
remove
nil
cons
cons
nil
cons
nil
cons
cons
89
ref
24
ref
304
remove
81
ref
appTerm
appTerm
81
ref
appTerm
absTerm
354
def
91
ref
appTerm
355
def
betaConv
nil
249
ref
354
ref
appTerm
356
def
axiom
nil
58
ref
356
remove
nil
cons
cons
59
ref
355
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
47
ref
259
ref
354
remove
nil
cons
cons
292
ref
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
subst
sym
94
ref
eqMp
eqMp
eqMp
nil
99
ref
349
remove
cons
357
def
347
remove
cons
nil
cons
cons
111
ref
subst
deductAntisym
eqMp
89
ref
163
ref
93
remove
appTerm
92
remove
266
remove
appTerm
appTerm
absTerm
358
def
269
remove
appTerm
359
def
betaConv
nil
249
ref
358
ref
appTerm
360
def
axiom
361
def
nil
58
ref
360
remove
nil
cons
cons
362
def
59
ref
359
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
47
ref
259
ref
358
ref
nil
cons
cons
363
def
46
ref
287
remove
cons
nil
cons
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
nil
357
remove
100
ref
326
remove
cons
"R"
20
ref
var
364
def
327
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
58
ref
60
ref
104
ref
appTerm
365
def
364
ref
varTerm
366
def
appTerm
367
def
nil
cons
cons
59
ref
366
ref
nil
cons
368
def
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
nil
58
ref
60
ref
102
ref
appTerm
369
def
366
ref
appTerm
nil
cons
cons
59
ref
60
ref
367
remove
appTerm
366
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
"r"
20
remove
var
370
def
60
ref
369
remove
370
ref
varTerm
371
def
appTerm
appTerm
372
def
60
ref
365
remove
371
ref
appTerm
appTerm
371
ref
appTerm
appTerm
absTerm
373
def
366
remove
appTerm
374
def
betaConv
24
ref
163
ref
102
ref
appTerm
375
def
104
ref
appTerm
376
def
appTerm
refl
59
ref
249
ref
370
ref
372
remove
60
ref
60
ref
63
remove
appTerm
371
ref
appTerm
appTerm
371
ref
appTerm
377
def
appTerm
absTerm
appTerm
absTerm
104
remove
appTerm
betaConv
appThm
85
remove
375
remove
appTerm
refl
58
ref
59
ref
249
ref
370
remove
60
remove
62
remove
371
remove
appTerm
appTerm
377
remove
appTerm
absTerm
appTerm
absTerm
absTerm
378
def
102
remove
appTerm
betaConv
appThm
nil
73
remove
163
remove
appTerm
378
remove
appTerm
axiom
110
remove
appThm
eqMp
106
remove
appThm
eqMp
376
remove
assume
eqMp
nil
58
ref
249
ref
373
ref
appTerm
nil
cons
cons
59
ref
374
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
47
ref
259
ref
373
remove
nil
cons
cons
46
ref
368
remove
cons
nil
cons
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
eqMp
eqMp
379
def
subst
proveHyp
proveHyp
proveHyp
eqMp
eqMp
eqMp
nil
99
remove
311
remove
cons
380
def
309
remove
cons
nil
cons
cons
111
ref
subst
deductAntisym
eqMp
358
remove
264
ref
appTerm
381
def
betaConv
361
remove
nil
362
remove
59
ref
381
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
47
ref
363
remove
46
remove
264
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
nil
380
remove
100
ref
268
remove
cons
364
remove
273
remove
cons
nil
cons
cons
cons
nil
cons
cons
379
remove
subst
proveHyp
proveHyp
proveHyp
382
def
subst
eqMp
eqMp
eqMp
absThm
eqMp
eqMp
nil
19
ref
0
ref
6
ref
0
ref
6
remove
21
ref
cons
opType
nil
cons
cons
opType
constTerm
12
remove
appTerm
8
remove
appTerm
thm
nil
"P"
0
ref
0
ref
15
ref
"C"
varType
383
def
nil
cons
384
def
cons
opType
385
def
21
ref
cons
opType
386
def
var
387
def
"f"
385
ref
var
388
def
40
ref
18
ref
146
remove
148
ref
19
ref
0
ref
1
remove
384
ref
opType
389
def
0
ref
389
ref
21
ref
cons
opType
nil
cons
cons
opType
constTerm
390
def
9
ref
0
ref
0
ref
2
remove
384
ref
cons
opType
391
def
0
ref
4
remove
389
ref
nil
cons
392
def
cons
opType
393
def
nil
cons
394
def
cons
opType
constTerm
"Function.o"
const
395
def
0
ref
385
ref
0
ref
17
remove
391
ref
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
388
ref
varTerm
396
def
appTerm
28
ref
appTerm
397
def
appTerm
398
def
150
ref
appTerm
appTerm
9
remove
0
ref
385
ref
0
ref
192
remove
392
ref
cons
opType
399
def
nil
cons
cons
opType
constTerm
396
ref
appTerm
400
def
196
remove
28
ref
appTerm
401
def
150
remove
appTerm
appTerm
402
def
appTerm
403
def
absTerm
404
def
appTerm
405
def
absTerm
406
def
appTerm
407
def
absTerm
408
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
385
ref
nil
cons
cons
nil
cons
409
def
14
ref
cons
410
def
160
ref
subst
subst
388
ref
nil
89
ref
407
remove
nil
cons
cons
nil
cons
nil
cons
cons
95
ref
subst
nil
139
ref
406
remove
nil
cons
cons
nil
cons
nil
cons
cons
138
ref
14
ref
cons
411
def
160
ref
subst
subst
18
ref
nil
89
ref
405
remove
nil
cons
cons
nil
cons
nil
cons
cons
95
ref
subst
nil
158
remove
404
remove
nil
cons
cons
nil
cons
nil
cons
cons
161
remove
subst
148
ref
nil
89
ref
403
ref
nil
cons
412
def
cons
nil
cons
nil
cons
cons
95
ref
subst
181
remove
nil
182
remove
59
ref
412
ref
cons
nil
cons
413
def
cons
nil
cons
cons
116
ref
subst
proveHyp
nil
185
remove
413
ref
cons
nil
cons
cons
414
def
76
ref
subst
414
remove
127
ref
subst
390
remove
refl
415
def
398
ref
refl
416
def
189
ref
appThm
nil
"f"
391
remove
var
397
ref
nil
cons
cons
nil
cons
nil
cons
cons
417
def
117
remove
"B"
384
remove
cons
nil
cons
418
def
cons
14
ref
cons
419
def
201
ref
subst
subst
trans
appThm
400
ref
refl
420
def
401
ref
refl
421
def
189
remove
appThm
nil
26
remove
142
remove
cons
nil
cons
nil
cons
cons
422
def
201
ref
subst
trans
appThm
"A"
16
remove
cons
418
remove
cons
14
ref
cons
423
def
201
remove
subst
trans
appThm
nil
"x"
389
ref
var
424
def
165
remove
389
remove
constTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
392
ref
cons
nil
cons
14
ref
cons
202
remove
subst
425
def
subst
trans
sym
94
ref
eqMp
eqMp
nil
204
remove
100
remove
412
ref
cons
nil
cons
426
def
cons
nil
cons
cons
111
ref
subst
deductAntisym
eqMp
nil
58
ref
206
remove
403
ref
appTerm
427
def
nil
cons
cons
59
ref
208
remove
403
ref
appTerm
428
def
nil
cons
cons
nil
cons
429
def
cons
nil
cons
cons
127
ref
subst
proveHyp
nil
119
ref
169
ref
212
remove
403
ref
appTerm
430
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
160
remove
subst
169
remove
nil
89
ref
430
remove
nil
cons
cons
nil
cons
nil
cons
cons
95
remove
subst
nil
215
remove
413
ref
cons
nil
cons
cons
431
def
76
ref
subst
431
remove
127
ref
subst
217
remove
nil
219
remove
413
remove
cons
nil
cons
cons
432
def
116
ref
subst
proveHyp
432
ref
76
remove
subst
432
remove
127
remove
subst
415
ref
416
remove
221
ref
appThm
417
remove
419
remove
229
ref
subst
subst
170
remove
0
ref
383
ref
392
ref
cons
opType
constTerm
433
def
refl
230
remove
34
ref
19
ref
0
ref
383
ref
0
ref
383
remove
21
ref
cons
opType
nil
cons
cons
opType
constTerm
397
remove
35
ref
appTerm
appTerm
396
ref
36
remove
appTerm
appTerm
absTerm
434
def
35
remove
appTerm
435
def
betaConv
18
ref
33
ref
434
ref
appTerm
436
def
absTerm
437
def
28
ref
appTerm
438
def
betaConv
388
ref
40
ref
437
ref
appTerm
439
def
absTerm
440
def
396
ref
appTerm
441
def
betaConv
nil
30
remove
0
ref
386
remove
21
ref
cons
opType
constTerm
442
def
440
ref
appTerm
443
def
axiom
nil
58
ref
443
remove
nil
cons
cons
59
ref
441
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
409
remove
387
remove
440
remove
nil
cons
cons
"x"
385
remove
var
396
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
nil
58
ref
439
remove
nil
cons
cons
59
ref
438
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
138
remove
139
remove
437
remove
nil
cons
cons
143
remove
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
nil
58
ref
436
remove
nil
cons
cons
59
ref
435
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
118
ref
119
remove
434
remove
nil
cons
cons
120
remove
cons
nil
cons
cons
137
ref
subst
eqMp
eqMp
444
def
subst
appThm
trans
trans
appThm
420
remove
421
remove
221
remove
appThm
422
remove
229
ref
subst
trans
appThm
nil
"a"
15
remove
var
28
remove
172
remove
appTerm
445
def
nil
cons
cons
nil
cons
nil
cons
cons
423
remove
229
remove
subst
subst
trans
appThm
nil
424
ref
433
remove
396
remove
445
remove
appTerm
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
425
ref
subst
trans
sym
94
ref
eqMp
eqMp
nil
231
remove
426
ref
cons
nil
cons
cons
111
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
232
remove
426
ref
cons
nil
cons
cons
111
remove
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
58
ref
33
ref
34
ref
233
remove
403
ref
appTerm
absTerm
appTerm
nil
cons
cons
429
remove
cons
nil
cons
cons
116
ref
subst
proveHyp
118
remove
234
remove
426
remove
cons
nil
cons
cons
260
remove
subst
eqMp
eqMp
nil
58
ref
65
remove
427
remove
appTerm
428
remove
appTerm
nil
cons
cons
59
ref
261
remove
403
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
ref
subst
proveHyp
nil
262
remove
412
remove
cons
263
remove
cons
nil
cons
cons
382
remove
subst
eqMp
eqMp
446
def
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
442
ref
408
remove
appTerm
thm
442
ref
refl
388
ref
44
remove
18
ref
nil
"g"
393
ref
var
398
ref
nil
cons
cons
"f"
393
ref
var
395
remove
0
ref
399
ref
0
ref
195
ref
394
remove
cons
opType
nil
cons
cons
opType
constTerm
400
ref
appTerm
401
ref
appTerm
447
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
13
ref
"B"
392
ref
cons
nil
cons
cons
14
ref
cons
144
remove
subst
subst
147
remove
148
remove
415
remove
nil
"g"
195
remove
var
401
remove
nil
cons
cons
"f"
399
remove
var
400
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
"B"
194
remove
cons
13
remove
"C"
392
remove
cons
nil
cons
cons
cons
14
remove
cons
444
remove
subst
subst
appThm
446
remove
appThm
nil
424
remove
402
remove
nil
cons
cons
nil
cons
nil
cons
cons
425
remove
subst
trans
absThm
appThm
nil
89
ref
81
remove
nil
cons
cons
nil
cons
nil
cons
cons
448
def
153
remove
89
remove
24
remove
33
remove
34
remove
91
ref
absTerm
appTerm
appTerm
91
ref
appTerm
absTerm
449
def
91
remove
appTerm
450
def
betaConv
nil
249
remove
449
ref
appTerm
451
def
axiom
nil
58
remove
451
remove
nil
cons
cons
59
remove
450
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
116
remove
subst
proveHyp
47
remove
259
remove
449
remove
nil
cons
cons
292
remove
cons
nil
cons
cons
137
remove
subst
eqMp
eqMp
452
def
subst
subst
trans
trans
absThm
appThm
448
ref
411
remove
452
ref
subst
subst
trans
absThm
appThm
448
remove
410
remove
452
remove
subst
subst
trans
sym
94
remove
eqMp
nil
442
remove
388
remove
40
remove
18
remove
19
remove
0
ref
393
ref
0
remove
393
remove
21
remove
cons
opType
nil
cons
cons
opType
constTerm
447
remove
appTerm
398
remove
appTerm
absTerm
appTerm
absTerm
appTerm
thm