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
3
ref
1
ref
3
ref
4
ref
cons
opType
11
def
nil
cons
cons
opType
12
def
constTerm
13
def
refl
14
def
"Data.List.member"
const
1
ref
2
ref
1
ref
"Data.List.list"
typeOp
2
ref
nil
cons
15
def
opType
16
def
4
ref
cons
opType
17
def
nil
cons
18
def
cons
opType
constTerm
19
def
9
ref
varTerm
20
def
appTerm
21
def
refl
22
def
nil
10
ref
1
ref
16
ref
18
ref
cons
opType
constTerm
23
def
"Data.List.nubReverse"
const
1
ref
16
ref
16
ref
nil
cons
24
def
cons
opType
25
def
constTerm
26
def
"Data.List.[]"
const
16
ref
constTerm
27
def
appTerm
28
def
appTerm
27
ref
appTerm
axiom
29
def
appThm
9
ref
"Data.Bool.~"
const
11
ref
constTerm
30
def
21
ref
27
ref
appTerm
31
def
appTerm
32
def
absTerm
33
def
20
ref
appTerm
34
def
betaConv
nil
7
ref
33
ref
appTerm
35
def
axiom
nil
"p"
3
ref
var
36
def
35
remove
nil
cons
cons
"q"
3
ref
var
37
def
34
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
13
ref
"Data.Bool.==>"
const
12
ref
constTerm
38
def
36
ref
varTerm
39
def
appTerm
40
def
37
ref
varTerm
41
def
appTerm
42
def
appTerm
refl
36
ref
37
ref
13
ref
"Data.Bool./\\"
const
12
ref
constTerm
43
def
39
ref
appTerm
44
def
41
ref
appTerm
45
def
appTerm
46
def
39
ref
appTerm
absTerm
47
def
absTerm
48
def
39
ref
appTerm
betaConv
41
ref
refl
49
def
appThm
47
remove
41
ref
appTerm
betaConv
trans
appThm
nil
10
ref
1
ref
12
ref
1
ref
12
ref
4
ref
cons
opType
50
def
nil
cons
cons
opType
constTerm
51
def
38
ref
appTerm
48
remove
appTerm
axiom
39
ref
refl
52
def
appThm
49
ref
appThm
eqMp
53
def
sym
54
def
46
remove
refl
37
ref
10
ref
1
ref
50
ref
1
ref
50
remove
4
ref
cons
opType
nil
cons
cons
opType
constTerm
55
def
"f"
12
ref
var
56
def
56
ref
varTerm
57
def
39
ref
appTerm
41
ref
appTerm
absTerm
58
def
appTerm
56
ref
57
ref
"Data.Bool.T"
const
3
ref
constTerm
59
def
appTerm
59
ref
appTerm
absTerm
60
def
appTerm
absTerm
61
def
41
ref
appTerm
betaConv
appThm
10
ref
1
ref
11
ref
1
ref
11
ref
4
ref
cons
opType
62
def
nil
cons
cons
opType
constTerm
63
def
44
remove
appTerm
refl
36
ref
61
remove
absTerm
64
def
39
ref
appTerm
betaConv
appThm
nil
51
ref
43
ref
appTerm
64
ref
appTerm
axiom
65
def
52
remove
appThm
eqMp
49
ref
appThm
eqMp
66
def
sym
56
ref
57
ref
refl
nil
"t"
3
ref
var
67
def
39
ref
nil
cons
68
def
cons
nil
cons
nil
cons
cons
13
ref
67
ref
varTerm
69
def
appTerm
70
def
59
ref
appTerm
71
def
assume
sym
nil
59
ref
axiom
72
def
eqMp
69
ref
assume
72
ref
deductAntisym
deductAntisym
73
def
subst
39
ref
assume
74
def
eqMp
appThm
nil
67
ref
41
ref
nil
cons
75
def
cons
nil
cons
nil
cons
cons
73
ref
subst
41
ref
assume
76
def
eqMp
appThm
absThm
eqMp
77
def
nil
"P"
3
ref
var
78
def
68
ref
cons
"Q"
3
ref
var
79
def
75
ref
cons
nil
cons
80
def
cons
nil
cons
cons
14
ref
56
ref
57
remove
78
ref
varTerm
81
def
appTerm
82
def
79
ref
varTerm
83
def
appTerm
absTerm
84
def
36
ref
37
ref
39
ref
absTerm
absTerm
85
def
appTerm
betaConv
85
ref
81
ref
appTerm
betaConv
83
ref
refl
86
def
appThm
37
ref
81
ref
absTerm
83
ref
appTerm
betaConv
trans
trans
appThm
60
ref
85
ref
appTerm
betaConv
85
ref
59
ref
appTerm
betaConv
59
ref
refl
87
def
appThm
37
ref
59
ref
absTerm
59
ref
appTerm
betaConv
trans
trans
appThm
13
ref
43
ref
81
ref
appTerm
88
def
83
ref
appTerm
89
def
appTerm
refl
37
ref
55
remove
56
remove
82
remove
41
ref
appTerm
absTerm
appTerm
60
ref
appTerm
absTerm
83
ref
appTerm
betaConv
appThm
63
ref
88
remove
appTerm
refl
64
remove
81
ref
appTerm
betaConv
appThm
65
remove
81
ref
refl
90
def
appThm
eqMp
86
ref
appThm
eqMp
89
remove
assume
eqMp
91
def
85
remove
refl
appThm
eqMp
sym
72
ref
eqMp
92
def
subst
deductAntisym
eqMp
53
remove
42
ref
assume
eqMp
sym
74
remove
eqMp
14
ref
58
remove
36
ref
37
ref
41
ref
absTerm
93
def
absTerm
94
def
appTerm
betaConv
94
ref
39
ref
appTerm
betaConv
49
ref
appThm
93
ref
41
ref
appTerm
betaConv
trans
trans
appThm
60
remove
94
ref
appTerm
betaConv
94
ref
59
ref
appTerm
betaConv
87
remove
appThm
93
ref
59
ref
appTerm
betaConv
trans
trans
95
def
appThm
66
remove
45
remove
assume
eqMp
94
ref
refl
96
def
appThm
eqMp
sym
72
ref
eqMp
97
def
proveHyp
deductAntisym
98
def
subst
proveHyp
"A"
15
ref
cons
nil
cons
99
def
"P"
5
ref
var
100
def
33
remove
nil
cons
cons
9
ref
20
ref
nil
cons
cons
nil
cons
101
def
cons
nil
cons
cons
nil
36
ref
7
ref
100
ref
varTerm
102
def
appTerm
103
def
nil
cons
104
def
cons
37
ref
102
ref
20
ref
appTerm
105
def
nil
cons
106
def
cons
nil
cons
cons
nil
cons
cons
107
def
54
ref
subst
107
remove
97
remove
77
remove
deductAntisym
108
def
subst
13
ref
105
remove
appTerm
refl
9
ref
59
ref
absTerm
109
def
20
ref
appTerm
betaConv
appThm
"p"
5
ref
var
110
def
10
ref
1
ref
5
ref
6
ref
nil
cons
cons
opType
constTerm
110
remove
varTerm
appTerm
109
remove
appTerm
absTerm
111
def
102
ref
appTerm
betaConv
112
def
nil
10
ref
1
ref
6
ref
1
ref
6
remove
4
ref
cons
opType
nil
cons
cons
opType
constTerm
7
ref
appTerm
111
remove
appTerm
axiom
102
remove
refl
appThm
113
def
103
ref
assume
eqMp
eqMp
20
ref
refl
114
def
appThm
eqMp
sym
72
ref
eqMp
eqMp
nil
78
ref
104
remove
cons
79
ref
106
remove
cons
nil
cons
cons
nil
cons
cons
92
ref
subst
deductAntisym
eqMp
115
def
subst
eqMp
eqMp
nil
36
ref
32
remove
nil
cons
cons
37
ref
13
ref
31
ref
appTerm
"Data.Bool.F"
const
3
ref
constTerm
116
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
nil
78
ref
31
ref
nil
cons
cons
nil
cons
nil
cons
cons
nil
36
ref
30
ref
81
ref
appTerm
117
def
nil
cons
118
def
cons
37
ref
13
ref
81
ref
appTerm
116
ref
appTerm
nil
cons
119
def
cons
nil
cons
cons
nil
cons
cons
120
def
54
ref
subst
120
remove
108
ref
subst
nil
36
ref
81
ref
nil
cons
121
def
cons
37
ref
116
ref
nil
cons
122
def
cons
nil
cons
cons
nil
cons
cons
38
ref
refl
123
def
13
ref
39
ref
appTerm
41
ref
appTerm
assume
124
def
appThm
49
remove
appThm
sym
nil
36
ref
75
ref
cons
125
def
37
ref
75
ref
cons
nil
cons
cons
nil
cons
cons
126
def
54
ref
subst
126
remove
108
ref
subst
76
remove
eqMp
nil
78
ref
75
remove
cons
80
remove
cons
nil
cons
cons
92
ref
subst
deductAntisym
eqMp
127
def
eqMp
nil
36
ref
42
remove
nil
cons
128
def
cons
37
ref
38
ref
41
remove
appTerm
129
def
39
ref
appTerm
nil
cons
130
def
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
129
ref
refl
124
remove
appThm
sym
127
remove
eqMp
eqMp
nil
125
remove
37
ref
68
remove
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
nil
78
ref
128
remove
cons
79
ref
130
remove
cons
nil
cons
cons
nil
cons
cons
131
def
14
ref
84
remove
94
ref
appTerm
betaConv
94
remove
81
ref
appTerm
betaConv
86
ref
appThm
93
remove
83
ref
appTerm
betaConv
trans
trans
appThm
95
remove
appThm
91
remove
96
remove
appThm
eqMp
sym
72
ref
eqMp
subst
eqMp
98
ref
131
remove
92
ref
subst
eqMp
deductAntisym
deductAntisym
subst
13
ref
117
ref
appTerm
refl
36
ref
40
ref
116
ref
appTerm
absTerm
132
def
81
ref
appTerm
betaConv
appThm
nil
63
ref
30
ref
appTerm
132
remove
appTerm
axiom
90
ref
appThm
eqMp
117
remove
assume
eqMp
nil
36
ref
38
ref
81
ref
appTerm
133
def
116
ref
appTerm
nil
cons
cons
37
ref
38
ref
116
ref
appTerm
81
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
36
ref
122
ref
cons
37
ref
121
ref
cons
nil
cons
cons
nil
cons
cons
134
def
54
ref
subst
134
remove
108
ref
subst
36
ref
39
remove
absTerm
135
def
81
ref
appTerm
136
def
betaConv
nil
13
ref
116
ref
appTerm
137
def
0
ref
62
remove
constTerm
138
def
135
ref
appTerm
139
def
appTerm
axiom
116
ref
assume
eqMp
nil
36
ref
139
remove
nil
cons
cons
37
ref
136
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
"A"
4
ref
cons
nil
cons
140
def
"P"
11
remove
var
141
def
135
remove
nil
cons
cons
"x"
3
ref
var
142
def
121
ref
cons
nil
cons
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
eqMp
nil
78
ref
122
ref
cons
79
ref
121
remove
cons
nil
cons
cons
nil
cons
cons
92
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
78
ref
118
remove
cons
79
ref
119
remove
cons
nil
cons
cons
nil
cons
cons
92
ref
subst
deductAntisym
eqMp
143
def
subst
eqMp
144
def
trans
appThm
144
remove
appThm
nil
67
ref
122
remove
cons
nil
cons
nil
cons
cons
145
def
67
ref
13
ref
137
remove
69
ref
appTerm
appTerm
30
ref
69
ref
appTerm
146
def
appTerm
absTerm
147
def
69
ref
appTerm
148
def
betaConv
nil
138
ref
147
ref
appTerm
149
def
axiom
nil
36
ref
149
remove
nil
cons
cons
37
ref
148
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
140
ref
141
ref
147
remove
nil
cons
cons
142
ref
69
ref
nil
cons
cons
nil
cons
150
def
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
subst
nil
13
ref
30
ref
116
ref
appTerm
appTerm
59
ref
appTerm
axiom
trans
trans
absThm
appThm
nil
67
ref
59
ref
nil
cons
cons
nil
cons
nil
cons
cons
151
def
67
ref
13
ref
7
ref
9
ref
69
ref
absTerm
appTerm
appTerm
69
ref
appTerm
absTerm
152
def
69
ref
appTerm
153
def
betaConv
nil
138
ref
152
ref
appTerm
154
def
axiom
nil
36
ref
154
remove
nil
cons
cons
37
ref
153
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
140
ref
141
ref
152
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
155
def
subst
156
def
trans
sym
72
ref
eqMp
nil
36
ref
7
ref
9
ref
13
ref
21
ref
28
ref
appTerm
appTerm
31
remove
appTerm
absTerm
appTerm
157
def
nil
cons
cons
37
ref
7
ref
"h"
2
ref
var
158
def
0
ref
1
ref
17
ref
4
ref
cons
opType
159
def
constTerm
160
def
"t"
16
ref
var
161
def
38
ref
7
ref
9
ref
13
ref
21
ref
26
ref
161
ref
varTerm
162
def
appTerm
163
def
appTerm
appTerm
21
ref
162
ref
appTerm
164
def
appTerm
absTerm
165
def
appTerm
166
def
appTerm
7
ref
9
ref
13
ref
21
ref
26
ref
"Data.List.::"
const
1
ref
2
ref
25
ref
nil
cons
167
def
cons
opType
constTerm
158
ref
varTerm
168
def
appTerm
169
def
162
ref
appTerm
170
def
appTerm
171
def
appTerm
appTerm
21
ref
170
ref
appTerm
172
def
appTerm
absTerm
appTerm
173
def
appTerm
174
def
absTerm
175
def
appTerm
176
def
absTerm
177
def
appTerm
178
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
100
ref
177
remove
nil
cons
cons
nil
cons
nil
cons
cons
13
ref
103
remove
appTerm
refl
112
remove
appThm
113
remove
eqMp
sym
179
def
subst
158
ref
nil
67
ref
176
remove
nil
cons
cons
nil
cons
nil
cons
cons
73
ref
subst
nil
"P"
17
ref
var
180
def
175
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
24
remove
cons
nil
cons
181
def
nil
nil
cons
182
def
cons
183
def
179
ref
subst
184
def
subst
161
ref
nil
67
ref
174
remove
nil
cons
cons
nil
cons
nil
cons
cons
73
ref
subst
nil
36
ref
166
remove
nil
cons
185
def
cons
186
def
37
ref
173
remove
nil
cons
187
def
cons
nil
cons
cons
nil
cons
cons
188
def
54
ref
subst
188
remove
108
ref
subst
8
ref
9
ref
14
ref
22
ref
161
ref
23
ref
171
ref
appTerm
"Data.Bool.cond"
const
189
def
1
ref
3
ref
1
ref
16
ref
167
remove
cons
opType
nil
cons
cons
opType
constTerm
190
def
19
ref
168
ref
appTerm
191
def
162
ref
appTerm
192
def
appTerm
163
ref
appTerm
169
ref
163
ref
appTerm
193
def
appTerm
194
def
appTerm
absTerm
195
def
162
ref
appTerm
196
def
betaConv
158
ref
160
ref
195
ref
appTerm
197
def
absTerm
198
def
168
ref
appTerm
199
def
betaConv
nil
7
ref
198
ref
appTerm
200
def
axiom
nil
36
ref
200
remove
nil
cons
cons
37
ref
199
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
99
ref
100
ref
198
remove
nil
cons
cons
9
ref
168
ref
nil
cons
cons
nil
cons
201
def
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
nil
36
ref
197
remove
nil
cons
cons
37
ref
196
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
181
ref
180
ref
195
remove
nil
cons
cons
"x"
16
ref
var
202
def
162
ref
nil
cons
203
def
cons
nil
cons
204
def
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
205
def
appThm
appThm
161
ref
13
ref
172
remove
appTerm
"Data.Bool.\\/"
const
12
remove
constTerm
206
def
10
ref
1
ref
2
ref
5
remove
nil
cons
cons
opType
constTerm
207
def
20
ref
appTerm
208
def
168
ref
appTerm
209
def
appTerm
164
ref
appTerm
210
def
appTerm
absTerm
211
def
162
ref
appTerm
212
def
betaConv
158
ref
160
ref
211
ref
appTerm
213
def
absTerm
214
def
168
ref
appTerm
215
def
betaConv
9
ref
7
ref
214
ref
appTerm
216
def
absTerm
217
def
20
ref
appTerm
218
def
betaConv
nil
7
ref
217
ref
appTerm
219
def
axiom
nil
36
ref
219
remove
nil
cons
cons
37
ref
218
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
99
ref
100
ref
217
remove
nil
cons
cons
101
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
nil
36
ref
216
remove
nil
cons
cons
37
ref
215
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
99
ref
100
ref
214
remove
nil
cons
cons
201
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
nil
36
ref
213
remove
nil
cons
cons
37
ref
212
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
181
ref
180
ref
211
remove
nil
cons
cons
204
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
220
def
appThm
absThm
appThm
sym
nil
100
ref
9
ref
13
ref
21
ref
194
ref
appTerm
appTerm
221
def
210
remove
appTerm
222
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
179
ref
subst
9
ref
nil
67
ref
222
remove
nil
cons
223
def
cons
nil
cons
nil
cons
cons
73
ref
subst
nil
36
ref
30
ref
209
ref
appTerm
nil
cons
224
def
cons
225
def
37
ref
223
ref
cons
nil
cons
226
def
cons
nil
cons
cons
227
def
54
ref
subst
227
remove
108
ref
subst
221
ref
refl
206
ref
refl
228
def
nil
225
remove
37
ref
13
ref
209
ref
appTerm
116
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
nil
78
ref
209
ref
nil
cons
229
def
cons
230
def
nil
cons
nil
cons
cons
143
ref
subst
eqMp
appThm
231
def
164
ref
refl
appThm
nil
67
ref
164
ref
nil
cons
cons
nil
cons
nil
cons
cons
67
ref
13
ref
206
ref
116
ref
appTerm
69
ref
appTerm
appTerm
69
ref
appTerm
absTerm
232
def
69
ref
appTerm
233
def
betaConv
nil
138
ref
232
ref
appTerm
234
def
axiom
nil
36
ref
234
remove
nil
cons
cons
37
ref
233
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
140
ref
141
ref
232
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
subst
235
def
trans
appThm
sym
nil
36
ref
13
ref
192
ref
appTerm
236
def
116
ref
appTerm
237
def
nil
cons
238
def
cons
239
def
37
ref
221
remove
164
ref
appTerm
nil
cons
240
def
cons
nil
cons
241
def
cons
nil
cons
cons
242
def
54
ref
subst
242
remove
108
ref
subst
13
ref
"_16352"
3
ref
var
243
def
13
ref
21
ref
190
ref
243
remove
varTerm
appTerm
163
ref
appTerm
193
ref
appTerm
appTerm
appTerm
164
ref
appTerm
absTerm
244
def
192
ref
appTerm
245
def
appTerm
refl
246
def
244
ref
116
ref
appTerm
betaConv
appThm
14
ref
245
remove
betaConv
appThm
247
def
13
ref
21
ref
190
ref
116
ref
appTerm
163
ref
appTerm
193
ref
appTerm
248
def
appTerm
appTerm
164
ref
appTerm
refl
appThm
trans
244
remove
refl
249
def
237
remove
assume
250
def
appThm
eqMp
sym
22
ref
nil
"t2"
16
ref
var
193
ref
nil
cons
251
def
cons
"t1"
16
ref
var
163
ref
nil
cons
252
def
cons
nil
cons
cons
nil
cons
cons
253
def
183
ref
"t2"
2
ref
var
254
def
207
ref
189
remove
1
ref
3
ref
1
ref
2
ref
1
ref
2
ref
15
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
255
def
116
ref
appTerm
"t1"
2
ref
var
256
def
varTerm
257
def
appTerm
254
ref
varTerm
258
def
appTerm
appTerm
258
ref
appTerm
absTerm
259
def
258
ref
appTerm
260
def
betaConv
256
ref
7
ref
259
ref
appTerm
261
def
absTerm
262
def
257
ref
appTerm
263
def
betaConv
nil
7
ref
262
ref
appTerm
264
def
axiom
nil
36
ref
264
remove
nil
cons
cons
37
ref
263
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
99
ref
100
ref
262
remove
nil
cons
cons
9
ref
257
ref
nil
cons
cons
nil
cons
265
def
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
nil
36
ref
261
remove
nil
cons
cons
37
ref
260
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
99
ref
100
ref
259
remove
nil
cons
cons
9
ref
258
ref
nil
cons
cons
nil
cons
266
def
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
subst
subst
267
def
appThm
nil
161
ref
252
ref
cons
268
def
nil
cons
nil
cons
cons
269
def
220
ref
subst
231
remove
165
ref
20
ref
appTerm
270
def
betaConv
nil
186
remove
37
ref
270
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
99
ref
100
ref
165
remove
nil
cons
cons
101
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
271
def
appThm
235
remove
trans
trans
trans
eqMp
eqMp
nil
78
ref
238
ref
cons
272
def
79
ref
240
ref
cons
nil
cons
273
def
cons
nil
cons
cons
92
ref
subst
deductAntisym
eqMp
nil
36
ref
236
remove
59
ref
appTerm
274
def
nil
cons
275
def
cons
276
def
241
remove
cons
nil
cons
cons
277
def
54
ref
subst
277
remove
108
ref
subst
246
remove
"_16350"
3
ref
var
278
def
13
ref
21
ref
190
ref
278
remove
varTerm
appTerm
163
ref
appTerm
193
ref
appTerm
appTerm
appTerm
164
ref
appTerm
absTerm
59
ref
appTerm
betaConv
appThm
247
remove
13
ref
21
ref
190
ref
59
ref
appTerm
163
ref
appTerm
193
ref
appTerm
279
def
appTerm
appTerm
164
remove
appTerm
refl
appThm
trans
249
remove
274
remove
assume
280
def
appThm
eqMp
sym
22
ref
253
remove
183
ref
254
remove
207
ref
255
remove
59
ref
appTerm
257
ref
appTerm
258
ref
appTerm
appTerm
257
ref
appTerm
absTerm
281
def
258
remove
appTerm
282
def
betaConv
256
remove
7
ref
281
ref
appTerm
283
def
absTerm
284
def
257
remove
appTerm
285
def
betaConv
nil
7
ref
284
ref
appTerm
286
def
axiom
nil
36
ref
286
remove
nil
cons
cons
37
ref
285
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
99
ref
100
ref
284
remove
nil
cons
cons
265
remove
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
nil
36
ref
283
remove
nil
cons
cons
37
ref
282
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
99
ref
100
ref
281
remove
nil
cons
cons
266
remove
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
subst
subst
287
def
appThm
271
ref
trans
eqMp
eqMp
nil
78
ref
275
remove
cons
288
def
273
remove
cons
nil
cons
cons
92
ref
subst
deductAntisym
eqMp
67
ref
206
ref
71
ref
appTerm
70
remove
116
ref
appTerm
appTerm
absTerm
289
def
192
ref
appTerm
290
def
betaConv
nil
138
ref
289
ref
appTerm
291
def
axiom
nil
36
ref
291
remove
nil
cons
cons
37
ref
290
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
140
ref
141
ref
289
remove
nil
cons
cons
142
ref
192
ref
nil
cons
292
def
cons
nil
cons
293
def
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
294
def
nil
288
ref
79
ref
238
ref
cons
295
def
"R"
3
ref
var
296
def
240
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
36
ref
38
ref
83
ref
appTerm
297
def
296
ref
varTerm
298
def
appTerm
299
def
nil
cons
cons
37
ref
298
ref
nil
cons
300
def
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
nil
36
ref
133
ref
298
ref
appTerm
nil
cons
cons
37
ref
38
ref
299
remove
appTerm
298
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
"r"
3
ref
var
301
def
38
ref
133
remove
301
ref
varTerm
302
def
appTerm
appTerm
303
def
38
ref
297
remove
302
ref
appTerm
appTerm
302
ref
appTerm
appTerm
absTerm
304
def
298
remove
appTerm
305
def
betaConv
13
ref
206
ref
81
ref
appTerm
306
def
83
ref
appTerm
307
def
appTerm
refl
37
ref
138
ref
301
ref
303
remove
38
ref
129
remove
302
ref
appTerm
appTerm
302
ref
appTerm
308
def
appTerm
absTerm
appTerm
absTerm
83
remove
appTerm
betaConv
appThm
63
remove
306
remove
appTerm
refl
36
ref
37
ref
138
ref
301
remove
38
ref
40
remove
302
remove
appTerm
appTerm
308
remove
appTerm
absTerm
appTerm
absTerm
absTerm
309
def
81
remove
appTerm
betaConv
appThm
nil
51
remove
206
ref
appTerm
309
remove
appTerm
axiom
90
remove
appThm
eqMp
86
remove
appThm
eqMp
307
remove
assume
eqMp
nil
36
ref
138
ref
304
ref
appTerm
nil
cons
cons
37
ref
305
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
140
ref
141
ref
304
remove
nil
cons
cons
142
ref
300
remove
cons
nil
cons
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
eqMp
eqMp
310
def
subst
proveHyp
proveHyp
proveHyp
eqMp
eqMp
nil
78
ref
224
ref
cons
79
ref
223
ref
cons
nil
cons
311
def
cons
nil
cons
cons
92
ref
subst
deductAntisym
eqMp
nil
36
ref
229
ref
cons
226
remove
cons
nil
cons
cons
312
def
54
ref
subst
312
remove
108
ref
subst
14
ref
19
remove
refl
209
ref
assume
313
def
appThm
314
def
194
ref
refl
appThm
appThm
228
ref
207
ref
refl
313
remove
appThm
168
ref
refl
appThm
nil
201
ref
nil
cons
cons
315
def
nil
67
ref
208
ref
20
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
73
ref
subst
114
remove
eqMp
316
def
subst
317
def
trans
appThm
314
remove
162
ref
refl
appThm
appThm
nil
67
ref
292
ref
cons
nil
cons
nil
cons
cons
318
def
67
ref
13
ref
206
ref
59
ref
appTerm
69
ref
appTerm
appTerm
59
ref
appTerm
absTerm
319
def
69
ref
appTerm
320
def
betaConv
nil
138
ref
319
ref
appTerm
321
def
axiom
nil
36
ref
321
remove
nil
cons
cons
37
ref
320
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
140
ref
141
ref
319
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
322
def
subst
trans
appThm
nil
67
ref
191
ref
194
ref
appTerm
nil
cons
323
def
cons
nil
cons
nil
cons
cons
67
ref
13
ref
71
remove
appTerm
69
ref
appTerm
absTerm
324
def
69
ref
appTerm
325
def
betaConv
nil
138
ref
324
ref
appTerm
326
def
axiom
nil
36
ref
326
remove
nil
cons
cons
37
ref
325
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
140
ref
141
ref
324
remove
nil
cons
cons
150
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
subst
trans
sym
nil
36
ref
30
remove
192
ref
appTerm
nil
cons
327
def
cons
328
def
37
ref
323
ref
cons
nil
cons
329
def
cons
nil
cons
cons
330
def
54
ref
subst
330
remove
108
ref
subst
191
remove
refl
331
def
190
ref
refl
332
def
nil
328
ref
37
ref
238
remove
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
nil
78
ref
292
ref
cons
333
def
nil
cons
nil
cons
cons
143
remove
subst
eqMp
334
def
appThm
163
ref
refl
335
def
appThm
193
ref
refl
336
def
appThm
267
ref
trans
337
def
appThm
nil
268
remove
201
ref
cons
nil
cons
cons
220
remove
subst
228
ref
317
remove
appThm
315
remove
271
remove
subst
338
def
334
ref
trans
appThm
145
remove
322
remove
subst
trans
trans
trans
sym
72
ref
eqMp
eqMp
nil
78
ref
327
ref
cons
339
def
79
ref
323
ref
cons
nil
cons
340
def
cons
nil
cons
cons
92
ref
subst
deductAntisym
eqMp
nil
36
ref
292
remove
cons
341
def
329
remove
cons
nil
cons
cons
342
def
54
ref
subst
342
remove
108
ref
subst
331
remove
332
ref
318
remove
73
ref
subst
192
ref
assume
eqMp
343
def
appThm
335
remove
appThm
336
remove
appThm
287
ref
trans
344
def
appThm
338
remove
343
remove
trans
trans
sym
72
ref
eqMp
eqMp
nil
333
ref
340
remove
cons
nil
cons
cons
92
ref
subst
deductAntisym
eqMp
67
ref
206
ref
69
ref
appTerm
345
def
146
remove
appTerm
absTerm
346
def
192
ref
appTerm
347
def
betaConv
nil
138
ref
346
ref
appTerm
348
def
axiom
349
def
nil
36
ref
348
remove
nil
cons
cons
350
def
37
ref
347
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
140
ref
141
ref
346
ref
nil
cons
cons
351
def
293
remove
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
352
def
nil
333
ref
79
ref
327
remove
cons
353
def
296
ref
323
remove
cons
nil
cons
cons
cons
nil
cons
cons
310
ref
subst
proveHyp
proveHyp
proveHyp
eqMp
eqMp
nil
230
ref
311
remove
cons
nil
cons
cons
92
ref
subst
deductAntisym
eqMp
346
remove
209
remove
appTerm
354
def
betaConv
349
remove
nil
350
remove
37
ref
354
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
140
ref
351
remove
142
ref
229
remove
cons
nil
cons
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
nil
230
remove
79
ref
224
remove
cons
296
ref
223
remove
cons
nil
cons
cons
cons
nil
cons
cons
310
ref
subst
proveHyp
proveHyp
proveHyp
eqMp
absThm
eqMp
eqMp
eqMp
nil
78
ref
185
remove
cons
79
ref
187
remove
cons
nil
cons
cons
nil
cons
cons
92
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
36
ref
43
ref
157
remove
appTerm
178
remove
appTerm
nil
cons
cons
37
ref
160
ref
"l"
16
ref
var
355
def
7
ref
9
ref
13
ref
21
ref
26
ref
355
ref
varTerm
356
def
appTerm
357
def
appTerm
appTerm
21
ref
356
ref
appTerm
358
def
appTerm
absTerm
359
def
appTerm
360
def
absTerm
361
def
appTerm
362
def
nil
cons
363
def
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
123
ref
43
ref
refl
364
def
361
ref
27
ref
appTerm
betaConv
appThm
8
ref
158
ref
160
ref
refl
365
def
161
ref
123
ref
361
ref
162
ref
appTerm
betaConv
appThm
361
ref
170
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
365
ref
355
ref
361
ref
356
ref
appTerm
366
def
betaConv
367
def
absThm
appThm
appThm
nil
"p"
17
ref
var
368
def
361
remove
nil
cons
369
def
cons
nil
cons
nil
cons
cons
368
ref
38
ref
43
ref
368
ref
varTerm
370
def
27
ref
appTerm
appTerm
7
ref
158
ref
160
ref
161
ref
38
ref
370
ref
162
ref
appTerm
appTerm
370
ref
170
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
appTerm
160
ref
355
ref
370
ref
356
ref
appTerm
absTerm
appTerm
appTerm
absTerm
371
def
370
ref
appTerm
372
def
betaConv
nil
0
ref
1
ref
159
ref
4
ref
cons
opType
constTerm
371
ref
appTerm
373
def
axiom
nil
36
ref
373
remove
nil
cons
cons
37
ref
372
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
"A"
18
remove
cons
nil
cons
"P"
159
remove
var
371
remove
nil
cons
cons
"x"
17
remove
var
370
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
374
def
subst
eqMp
eqMp
375
def
nil
362
remove
thm
365
ref
355
ref
nil
"t"
"Set.set"
typeOp
15
remove
opType
376
def
var
377
def
"Data.List.toSet"
const
1
ref
16
ref
376
ref
nil
cons
378
def
cons
opType
constTerm
379
def
356
ref
appTerm
380
def
nil
cons
cons
381
def
"s"
376
ref
var
382
def
379
ref
357
ref
appTerm
383
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
377
ref
13
ref
10
ref
1
ref
376
ref
1
ref
376
ref
4
ref
cons
opType
384
def
nil
cons
385
def
cons
opType
constTerm
386
def
382
ref
varTerm
387
def
appTerm
377
ref
varTerm
388
def
appTerm
389
def
appTerm
7
ref
9
ref
13
ref
"Set.member"
const
1
ref
2
ref
385
remove
cons
opType
constTerm
20
ref
appTerm
390
def
387
ref
appTerm
appTerm
390
ref
388
ref
appTerm
appTerm
absTerm
appTerm
391
def
appTerm
absTerm
392
def
388
ref
appTerm
393
def
betaConv
382
ref
0
ref
1
ref
384
ref
4
ref
cons
opType
constTerm
394
def
392
ref
appTerm
395
def
absTerm
396
def
387
ref
appTerm
397
def
betaConv
394
ref
refl
398
def
382
ref
398
remove
377
ref
nil
"y"
3
ref
var
391
ref
nil
cons
cons
142
ref
389
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
140
ref
182
remove
cons
399
def
"y"
2
remove
var
400
def
13
ref
208
remove
400
remove
varTerm
401
def
appTerm
appTerm
207
remove
401
ref
appTerm
20
ref
appTerm
appTerm
absTerm
402
def
401
ref
appTerm
403
def
betaConv
9
ref
7
ref
402
ref
appTerm
404
def
absTerm
405
def
20
ref
appTerm
406
def
betaConv
nil
7
ref
405
ref
appTerm
407
def
axiom
nil
36
ref
407
remove
nil
cons
cons
37
ref
406
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
99
ref
100
ref
405
remove
nil
cons
cons
101
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
nil
36
ref
404
remove
nil
cons
cons
37
ref
403
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
99
ref
100
ref
402
remove
nil
cons
cons
9
ref
401
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
subst
subst
absThm
appThm
absThm
appThm
sym
nil
394
ref
382
ref
394
ref
377
remove
13
ref
391
remove
appTerm
389
remove
appTerm
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
36
ref
394
remove
396
ref
appTerm
nil
cons
cons
37
ref
397
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
"A"
378
remove
cons
nil
cons
408
def
"P"
384
remove
var
409
def
396
remove
nil
cons
cons
"x"
376
remove
var
410
def
387
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
nil
36
ref
395
remove
nil
cons
cons
37
ref
393
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
408
remove
409
remove
392
remove
nil
cons
cons
410
remove
388
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
411
def
subst
8
ref
9
ref
14
ref
nil
355
ref
357
ref
nil
cons
cons
nil
cons
nil
cons
cons
9
ref
13
ref
390
remove
380
ref
appTerm
412
def
appTerm
358
ref
appTerm
413
def
absTerm
414
def
20
ref
appTerm
415
def
betaConv
355
ref
7
ref
414
ref
appTerm
416
def
absTerm
417
def
356
ref
appTerm
418
def
betaConv
365
ref
355
ref
8
ref
9
ref
413
remove
assume
sym
13
ref
358
ref
appTerm
412
remove
appTerm
419
def
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
nil
160
ref
355
ref
7
ref
9
ref
419
remove
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
36
ref
160
ref
417
ref
appTerm
nil
cons
cons
37
ref
418
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
181
ref
180
ref
417
remove
nil
cons
cons
202
ref
356
ref
nil
cons
cons
nil
cons
420
def
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
nil
36
ref
416
remove
nil
cons
cons
37
ref
415
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
99
ref
100
ref
414
remove
nil
cons
cons
101
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
421
def
subst
359
ref
20
ref
appTerm
422
def
betaConv
367
remove
375
remove
nil
36
ref
363
remove
cons
37
ref
366
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
181
ref
180
ref
369
remove
cons
420
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
nil
36
ref
360
remove
nil
cons
cons
37
ref
422
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
99
ref
100
ref
359
remove
nil
cons
cons
101
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
423
def
trans
appThm
421
ref
appThm
nil
142
remove
358
ref
nil
cons
cons
nil
cons
nil
cons
cons
399
remove
316
ref
subst
subst
424
def
trans
absThm
appThm
156
ref
trans
trans
absThm
appThm
151
remove
183
ref
155
remove
subst
subst
425
def
trans
sym
72
ref
eqMp
nil
160
ref
355
ref
386
ref
383
remove
appTerm
380
ref
appTerm
absTerm
appTerm
thm
26
ref
refl
426
def
29
ref
appThm
nil
36
ref
23
ref
26
ref
28
ref
appTerm
appTerm
28
ref
appTerm
427
def
nil
cons
cons
37
ref
7
ref
158
ref
160
ref
161
ref
38
ref
23
ref
26
ref
163
ref
appTerm
appTerm
163
ref
appTerm
428
def
appTerm
23
ref
26
ref
171
ref
appTerm
appTerm
171
ref
appTerm
429
def
appTerm
430
def
absTerm
431
def
appTerm
432
def
absTerm
433
def
appTerm
434
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
100
ref
433
remove
nil
cons
cons
nil
cons
nil
cons
cons
179
ref
subst
158
ref
nil
67
ref
432
remove
nil
cons
cons
nil
cons
nil
cons
cons
73
ref
subst
nil
180
ref
431
remove
nil
cons
cons
nil
cons
nil
cons
cons
184
ref
subst
161
ref
nil
67
ref
430
remove
nil
cons
cons
nil
cons
nil
cons
cons
73
ref
subst
nil
36
ref
428
ref
nil
cons
435
def
cons
37
ref
429
remove
nil
cons
436
def
cons
nil
cons
cons
nil
cons
cons
437
def
54
ref
subst
437
remove
108
ref
subst
23
ref
refl
438
def
426
ref
205
ref
appThm
appThm
205
ref
appThm
sym
nil
328
remove
37
ref
23
ref
26
ref
194
ref
appTerm
appTerm
194
ref
appTerm
nil
cons
439
def
cons
nil
cons
440
def
cons
nil
cons
cons
441
def
54
ref
subst
441
remove
108
ref
subst
438
ref
426
ref
337
ref
appThm
269
ref
205
ref
subst
332
remove
nil
355
ref
203
remove
cons
201
ref
cons
nil
cons
cons
423
ref
subst
334
remove
trans
appThm
428
remove
assume
442
def
appThm
169
remove
refl
442
ref
appThm
appThm
267
ref
trans
trans
trans
appThm
337
remove
appThm
nil
202
ref
251
remove
cons
nil
cons
nil
cons
cons
183
remove
316
remove
subst
443
def
subst
trans
sym
72
ref
eqMp
eqMp
nil
339
remove
79
ref
439
ref
cons
nil
cons
444
def
cons
nil
cons
cons
92
ref
subst
deductAntisym
eqMp
nil
341
remove
440
remove
cons
nil
cons
cons
445
def
54
ref
subst
445
remove
108
ref
subst
438
ref
426
ref
344
ref
appThm
442
remove
trans
appThm
344
remove
appThm
nil
202
ref
252
remove
cons
nil
cons
nil
cons
cons
443
ref
subst
trans
sym
72
ref
eqMp
eqMp
nil
333
ref
444
remove
cons
nil
cons
cons
92
ref
subst
deductAntisym
eqMp
352
remove
nil
333
remove
353
remove
296
ref
439
remove
cons
nil
cons
cons
cons
nil
cons
cons
310
ref
subst
proveHyp
proveHyp
proveHyp
eqMp
eqMp
nil
78
ref
435
remove
cons
79
ref
436
remove
cons
nil
cons
cons
nil
cons
cons
92
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
36
ref
43
ref
427
remove
appTerm
434
remove
appTerm
nil
cons
cons
37
ref
160
ref
355
ref
23
ref
26
ref
357
ref
appTerm
appTerm
357
ref
appTerm
absTerm
446
def
appTerm
447
def
nil
cons
448
def
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
123
ref
364
ref
446
ref
27
ref
appTerm
betaConv
appThm
8
ref
158
ref
365
ref
161
ref
123
ref
446
ref
162
ref
appTerm
betaConv
appThm
446
ref
170
ref
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
365
ref
355
ref
446
ref
356
ref
appTerm
449
def
betaConv
450
def
absThm
appThm
appThm
nil
368
ref
446
remove
nil
cons
451
def
cons
nil
cons
nil
cons
cons
374
ref
subst
eqMp
eqMp
452
def
nil
447
remove
thm
365
ref
355
ref
8
ref
9
ref
14
ref
22
remove
355
ref
23
ref
"Data.List.nub"
const
25
ref
constTerm
453
def
356
ref
appTerm
454
def
appTerm
"Data.List.reverse"
const
25
remove
constTerm
455
def
26
remove
455
ref
356
ref
appTerm
456
def
appTerm
457
def
appTerm
458
def
appTerm
absTerm
459
def
356
ref
appTerm
460
def
betaConv
nil
160
ref
459
ref
appTerm
461
def
axiom
nil
36
ref
461
remove
nil
cons
cons
37
ref
460
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
181
ref
180
ref
459
remove
nil
cons
cons
420
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
462
def
appThm
nil
355
ref
457
ref
nil
cons
cons
nil
cons
nil
cons
cons
463
def
9
ref
13
ref
21
ref
456
ref
appTerm
appTerm
358
ref
appTerm
absTerm
464
def
20
remove
appTerm
465
def
betaConv
355
ref
7
ref
464
ref
appTerm
466
def
absTerm
467
def
356
ref
appTerm
468
def
betaConv
nil
160
ref
467
ref
appTerm
469
def
axiom
nil
36
ref
469
remove
nil
cons
cons
37
ref
468
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
181
ref
180
ref
467
remove
nil
cons
cons
420
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
nil
36
ref
466
remove
nil
cons
cons
37
ref
465
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
99
ref
100
ref
464
remove
nil
cons
cons
101
remove
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
470
def
subst
nil
355
ref
456
ref
nil
cons
cons
nil
cons
nil
cons
cons
471
def
423
remove
subst
470
remove
trans
trans
trans
472
def
appThm
358
ref
refl
appThm
424
ref
trans
absThm
appThm
156
ref
trans
absThm
appThm
425
ref
trans
sym
72
ref
eqMp
nil
160
ref
355
ref
7
ref
9
ref
13
ref
21
remove
454
ref
appTerm
appTerm
358
remove
appTerm
absTerm
appTerm
absTerm
appTerm
thm
365
ref
355
ref
nil
381
remove
382
remove
379
remove
454
ref
appTerm
473
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
411
remove
subst
8
ref
9
remove
14
ref
nil
355
ref
454
ref
nil
cons
cons
nil
cons
nil
cons
cons
474
def
421
ref
subst
472
remove
trans
appThm
421
remove
appThm
424
remove
trans
absThm
appThm
156
remove
trans
trans
absThm
appThm
425
ref
trans
sym
72
ref
eqMp
nil
160
ref
355
ref
386
remove
473
remove
appTerm
380
remove
appTerm
absTerm
appTerm
thm
365
ref
355
ref
438
remove
474
remove
462
ref
subst
455
ref
refl
475
def
426
remove
475
remove
462
ref
appThm
463
ref
355
ref
23
ref
455
remove
456
ref
appTerm
appTerm
356
ref
appTerm
absTerm
476
def
356
ref
appTerm
477
def
betaConv
nil
160
ref
476
ref
appTerm
478
def
axiom
nil
36
ref
478
remove
nil
cons
cons
37
ref
477
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
181
ref
180
ref
476
remove
nil
cons
cons
420
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
subst
trans
appThm
471
ref
450
remove
452
remove
nil
36
ref
448
remove
cons
37
ref
449
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
181
ref
180
ref
451
remove
cons
420
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
subst
trans
appThm
trans
appThm
462
ref
appThm
nil
202
remove
458
remove
nil
cons
cons
nil
cons
nil
cons
cons
443
remove
subst
trans
absThm
appThm
425
remove
trans
sym
72
ref
eqMp
nil
160
ref
355
ref
23
remove
453
remove
454
ref
appTerm
appTerm
454
ref
appTerm
absTerm
appTerm
thm
"Number.Natural.<="
const
1
ref
"Number.Natural.natural"
typeOp
nil
opType
479
def
1
ref
479
ref
4
ref
cons
opType
480
def
nil
cons
cons
opType
481
def
constTerm
482
def
refl
483
def
"Data.List.length"
const
1
ref
16
remove
479
ref
nil
cons
484
def
cons
opType
constTerm
485
def
refl
486
def
29
remove
appThm
nil
10
remove
481
remove
constTerm
487
def
485
ref
27
ref
appTerm
488
def
appTerm
"Number.Natural.zero"
const
479
ref
constTerm
489
def
appTerm
axiom
490
def
trans
appThm
490
remove
appThm
nil
"n"
479
ref
var
491
def
489
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
67
ref
482
ref
491
ref
varTerm
492
def
appTerm
492
ref
appTerm
493
def
nil
cons
cons
nil
cons
nil
cons
cons
73
ref
subst
491
ref
493
remove
absTerm
494
def
492
ref
appTerm
495
def
betaConv
nil
0
remove
1
ref
480
ref
4
remove
cons
opType
constTerm
496
def
494
ref
appTerm
497
def
axiom
nil
36
ref
497
remove
nil
cons
cons
37
ref
495
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
"A"
484
ref
cons
nil
cons
498
def
"P"
480
remove
var
499
def
494
remove
nil
cons
cons
"x"
479
ref
var
500
def
492
ref
nil
cons
cons
nil
cons
501
def
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
eqMp
subst
trans
sym
72
ref
eqMp
nil
36
ref
482
ref
485
ref
28
remove
appTerm
appTerm
488
remove
appTerm
502
def
nil
cons
cons
37
ref
7
ref
158
ref
160
ref
161
ref
38
remove
482
ref
485
ref
163
ref
appTerm
503
def
appTerm
485
ref
162
ref
appTerm
504
def
appTerm
505
def
appTerm
482
ref
485
ref
171
remove
appTerm
appTerm
485
ref
170
ref
appTerm
506
def
appTerm
507
def
appTerm
508
def
absTerm
509
def
appTerm
510
def
absTerm
511
def
appTerm
512
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
108
ref
subst
proveHyp
nil
100
ref
511
remove
nil
cons
cons
nil
cons
nil
cons
cons
179
remove
subst
158
ref
nil
67
ref
510
remove
nil
cons
cons
nil
cons
nil
cons
cons
73
ref
subst
nil
180
ref
509
remove
nil
cons
cons
nil
cons
nil
cons
cons
184
ref
subst
161
ref
nil
67
ref
508
remove
nil
cons
cons
nil
cons
nil
cons
cons
73
ref
subst
nil
36
ref
505
ref
nil
cons
513
def
cons
37
ref
507
remove
nil
cons
514
def
cons
nil
cons
cons
nil
cons
cons
515
def
54
ref
subst
515
remove
108
ref
subst
483
ref
486
ref
205
remove
appThm
appThm
161
ref
487
ref
506
remove
appTerm
"Number.Natural.suc"
const
1
remove
479
ref
484
remove
cons
opType
constTerm
516
def
504
ref
appTerm
517
def
appTerm
absTerm
518
def
162
ref
appTerm
519
def
betaConv
158
ref
160
ref
518
ref
appTerm
520
def
absTerm
521
def
168
remove
appTerm
522
def
betaConv
nil
7
remove
521
ref
appTerm
523
def
axiom
nil
36
ref
523
remove
nil
cons
cons
37
ref
522
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
99
remove
100
remove
521
remove
nil
cons
cons
201
remove
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
nil
36
ref
520
remove
nil
cons
cons
37
ref
519
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
181
ref
180
ref
518
remove
nil
cons
cons
204
remove
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
524
def
appThm
sym
nil
239
remove
37
ref
482
ref
485
ref
194
remove
appTerm
appTerm
517
ref
appTerm
nil
cons
525
def
cons
nil
cons
526
def
cons
nil
cons
cons
527
def
54
ref
subst
527
remove
108
ref
subst
13
ref
"_16348"
3
ref
var
528
def
482
ref
485
ref
190
ref
528
remove
varTerm
appTerm
163
ref
appTerm
193
ref
appTerm
appTerm
appTerm
517
ref
appTerm
absTerm
529
def
192
remove
appTerm
530
def
appTerm
refl
531
def
529
ref
116
remove
appTerm
betaConv
appThm
14
remove
530
remove
betaConv
appThm
532
def
482
ref
485
ref
248
remove
appTerm
appTerm
517
ref
appTerm
refl
appThm
trans
529
remove
refl
533
def
250
remove
appThm
eqMp
sym
483
ref
486
ref
267
remove
appThm
269
remove
524
remove
subst
trans
appThm
517
ref
refl
534
def
appThm
nil
491
ref
504
ref
nil
cons
cons
535
def
"m"
479
remove
var
536
def
503
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
491
ref
13
ref
482
ref
516
ref
536
ref
varTerm
537
def
appTerm
appTerm
516
remove
492
ref
appTerm
538
def
appTerm
appTerm
482
ref
537
ref
appTerm
539
def
492
ref
appTerm
540
def
appTerm
absTerm
541
def
492
ref
appTerm
542
def
betaConv
536
ref
496
ref
541
ref
appTerm
543
def
absTerm
544
def
537
ref
appTerm
545
def
betaConv
nil
496
ref
544
ref
appTerm
546
def
axiom
nil
36
ref
546
remove
nil
cons
cons
37
ref
545
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
498
ref
499
ref
544
remove
nil
cons
cons
500
remove
537
ref
nil
cons
cons
nil
cons
547
def
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
nil
36
ref
543
remove
nil
cons
cons
37
ref
542
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
498
ref
499
ref
541
remove
nil
cons
cons
501
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
subst
nil
67
ref
513
ref
cons
nil
cons
nil
cons
cons
73
ref
subst
505
remove
assume
eqMp
548
def
trans
trans
sym
72
ref
eqMp
eqMp
eqMp
nil
272
remove
79
ref
525
ref
cons
nil
cons
549
def
cons
nil
cons
cons
92
ref
subst
deductAntisym
eqMp
nil
276
remove
526
remove
cons
nil
cons
cons
550
def
54
remove
subst
550
remove
108
remove
subst
531
remove
"_16346"
3
remove
var
551
def
482
ref
485
ref
190
remove
551
remove
varTerm
appTerm
163
remove
appTerm
193
remove
appTerm
appTerm
appTerm
517
ref
appTerm
absTerm
59
ref
appTerm
betaConv
appThm
532
remove
482
ref
485
ref
279
remove
appTerm
552
def
appTerm
517
ref
appTerm
refl
appThm
trans
533
remove
280
remove
appThm
eqMp
sym
nil
535
remove
536
ref
552
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
491
remove
13
ref
539
remove
538
ref
appTerm
appTerm
206
remove
487
ref
537
ref
appTerm
538
remove
appTerm
appTerm
540
remove
appTerm
appTerm
absTerm
553
def
492
remove
appTerm
554
def
betaConv
536
remove
496
ref
553
ref
appTerm
555
def
absTerm
556
def
537
remove
appTerm
557
def
betaConv
nil
496
remove
556
ref
appTerm
558
def
axiom
nil
36
ref
558
remove
nil
cons
cons
37
ref
557
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
498
ref
499
ref
556
remove
nil
cons
cons
547
remove
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
nil
36
ref
555
remove
nil
cons
cons
37
ref
554
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
498
remove
499
remove
553
remove
nil
cons
cons
501
remove
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
subst
228
remove
487
ref
refl
486
ref
287
remove
appThm
559
def
appThm
534
remove
appThm
appThm
483
ref
559
remove
appThm
504
remove
refl
appThm
548
remove
trans
appThm
nil
67
ref
487
ref
503
remove
appTerm
517
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
67
ref
13
remove
345
remove
59
ref
appTerm
appTerm
59
remove
appTerm
absTerm
560
def
69
remove
appTerm
561
def
betaConv
nil
138
remove
560
ref
appTerm
562
def
axiom
nil
36
ref
562
remove
nil
cons
cons
37
ref
561
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
140
remove
141
remove
560
remove
nil
cons
cons
150
remove
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
subst
trans
trans
sym
72
remove
eqMp
eqMp
eqMp
nil
288
ref
549
remove
cons
nil
cons
cons
92
ref
subst
deductAntisym
eqMp
294
remove
nil
288
remove
295
remove
296
remove
525
remove
cons
nil
cons
cons
cons
nil
cons
cons
310
remove
subst
proveHyp
proveHyp
proveHyp
eqMp
eqMp
nil
78
remove
513
remove
cons
79
remove
514
remove
cons
nil
cons
cons
nil
cons
cons
92
remove
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
nil
36
ref
43
remove
502
remove
appTerm
512
remove
appTerm
nil
cons
cons
37
ref
160
ref
355
ref
482
ref
485
ref
357
remove
appTerm
appTerm
485
ref
356
ref
appTerm
563
def
appTerm
absTerm
564
def
appTerm
565
def
nil
cons
566
def
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
123
ref
364
remove
564
ref
27
remove
appTerm
betaConv
appThm
8
remove
158
remove
365
ref
161
remove
123
remove
564
ref
162
remove
appTerm
betaConv
appThm
564
ref
170
remove
appTerm
betaConv
appThm
absThm
appThm
absThm
appThm
appThm
appThm
365
ref
355
ref
564
ref
356
ref
appTerm
567
def
betaConv
568
def
absThm
appThm
appThm
nil
368
remove
564
remove
nil
cons
569
def
cons
nil
cons
nil
cons
cons
374
remove
subst
eqMp
eqMp
570
def
nil
565
remove
thm
nil
180
ref
355
ref
482
ref
485
ref
454
remove
appTerm
appTerm
563
ref
appTerm
571
def
absTerm
572
def
nil
cons
cons
nil
cons
nil
cons
cons
184
remove
subst
355
ref
nil
67
remove
571
remove
nil
cons
cons
nil
cons
nil
cons
cons
73
remove
subst
483
remove
486
remove
462
remove
appThm
463
remove
355
ref
487
ref
485
ref
456
remove
appTerm
573
def
appTerm
563
ref
appTerm
574
def
absTerm
575
def
356
ref
appTerm
576
def
betaConv
nil
160
ref
575
ref
appTerm
577
def
axiom
578
def
nil
36
ref
577
remove
nil
cons
cons
37
ref
576
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
181
ref
180
ref
575
remove
nil
cons
cons
420
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
subst
trans
appThm
563
ref
refl
appThm
sym
482
remove
485
remove
457
remove
appTerm
appTerm
refl
355
ref
487
remove
563
remove
appTerm
573
remove
appTerm
579
def
absTerm
580
def
356
remove
appTerm
581
def
betaConv
365
remove
355
remove
579
remove
assume
sym
574
remove
assume
sym
deductAntisym
absThm
appThm
578
remove
eqMp
nil
36
ref
160
ref
580
ref
appTerm
nil
cons
cons
37
ref
581
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
ref
subst
proveHyp
181
ref
180
ref
580
remove
nil
cons
cons
420
ref
cons
nil
cons
cons
115
ref
subst
eqMp
eqMp
appThm
sym
471
remove
568
remove
570
remove
nil
36
remove
566
remove
cons
37
remove
567
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
98
remove
subst
proveHyp
181
remove
180
remove
569
remove
cons
420
remove
cons
nil
cons
cons
115
remove
subst
eqMp
eqMp
subst
eqMp
eqMp
eqMp
absThm
eqMp
nil
160
remove
572
remove
appTerm
thm