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