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