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