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