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