6
version
"Number.Natural.*"
"*"
"->"
typeOp
0
def
"Number.Natural.natural"
typeOp
nil
opType
1
def
0
ref
1
ref
1
ref
nil
cons
2
def
cons
opType
3
def
nil
cons
4
def
cons
opType
5
def
var
6
def
nil
cons
cons
nil
cons
6
ref
"Data.Bool./\\"
const
0
ref
"bool"
typeOp
nil
opType
7
def
0
ref
7
ref
7
ref
nil
cons
8
def
cons
opType
9
def
nil
cons
cons
opType
10
def
constTerm
11
def
"Data.Bool.!"
const
12
def
0
ref
0
ref
1
ref
8
ref
cons
opType
13
def
8
ref
cons
opType
constTerm
14
def
"n"
1
ref
var
15
def
"="
const
16
def
0
ref
1
ref
13
ref
nil
cons
cons
opType
constTerm
17
def
6
ref
varTerm
18
def
"Number.Natural.zero"
const
1
ref
constTerm
19
def
appTerm
20
def
15
ref
varTerm
21
def
appTerm
appTerm
22
def
19
ref
appTerm
23
def
absTerm
24
def
appTerm
25
def
appTerm
14
ref
"m"
1
ref
var
26
def
14
ref
15
ref
17
ref
18
ref
"Number.Natural.suc"
const
3
ref
constTerm
27
def
26
ref
varTerm
28
def
appTerm
29
def
appTerm
30
def
21
ref
appTerm
appTerm
31
def
"Number.Natural.+"
const
5
ref
constTerm
32
def
18
ref
28
ref
appTerm
21
ref
appTerm
appTerm
21
ref
appTerm
33
def
appTerm
34
def
absTerm
35
def
appTerm
36
def
absTerm
37
def
appTerm
38
def
appTerm
absTerm
39
def
refl
40
def
16
ref
0
ref
5
ref
0
ref
5
ref
8
ref
cons
opType
41
def
nil
cons
cons
opType
constTerm
18
ref
appTerm
"select"
const
42
def
0
ref
41
ref
5
ref
nil
cons
43
def
cons
opType
constTerm
44
def
39
ref
appTerm
appTerm
assume
sym
appThm
39
ref
18
ref
appTerm
betaConv
45
def
trans
"A"
43
ref
cons
nil
cons
46
def
nil
nil
cons
47
def
cons
48
def
nil
16
ref
0
ref
0
ref
0
ref
"A"
varType
49
def
8
ref
cons
opType
50
def
8
ref
cons
opType
51
def
0
ref
51
ref
8
ref
cons
opType
nil
cons
cons
opType
constTerm
52
def
"Data.Bool.?"
const
53
def
51
ref
constTerm
54
def
appTerm
55
def
"p"
50
ref
var
56
def
56
ref
varTerm
57
def
42
remove
0
ref
50
ref
49
ref
nil
cons
58
def
cons
opType
constTerm
57
ref
appTerm
appTerm
absTerm
appTerm
axiom
subst
40
remove
appThm
"p"
41
ref
var
59
def
59
remove
varTerm
60
def
44
remove
60
remove
appTerm
appTerm
absTerm
39
ref
appTerm
betaConv
trans
53
ref
0
ref
41
ref
8
ref
cons
opType
61
def
constTerm
62
def
refl
"fn"
5
ref
var
63
def
11
ref
16
ref
0
ref
3
ref
0
ref
3
ref
8
ref
cons
opType
nil
cons
cons
opType
constTerm
64
def
63
remove
varTerm
65
def
19
ref
appTerm
appTerm
15
ref
19
ref
absTerm
66
def
appTerm
appTerm
refl
14
ref
refl
15
ref
64
ref
65
ref
27
remove
21
ref
appTerm
67
def
appTerm
appTerm
refl
"_2250"
3
ref
var
68
def
26
ref
15
ref
32
ref
68
remove
varTerm
21
ref
appTerm
appTerm
21
ref
appTerm
absTerm
absTerm
absTerm
69
def
65
remove
21
ref
appTerm
70
def
appTerm
betaConv
21
ref
refl
71
def
appThm
26
ref
"n'"
1
ref
var
72
def
32
ref
70
remove
72
ref
varTerm
73
def
appTerm
appTerm
73
ref
appTerm
absTerm
absTerm
21
ref
appTerm
betaConv
trans
appThm
absThm
appThm
appThm
absThm
appThm
nil
"f"
0
ref
3
ref
43
remove
cons
opType
var
69
remove
nil
cons
cons
"e"
3
remove
var
66
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
"A"
4
remove
cons
nil
cons
47
ref
cons
"f"
0
ref
49
ref
0
ref
1
ref
58
ref
cons
opType
74
def
nil
cons
75
def
cons
opType
76
def
var
77
def
"Data.Bool.?!"
const
78
def
0
ref
0
ref
74
ref
8
ref
cons
opType
79
def
8
ref
cons
opType
80
def
constTerm
"fn"
74
remove
var
81
def
11
ref
16
ref
0
ref
49
ref
50
ref
nil
cons
cons
opType
constTerm
82
def
81
remove
varTerm
83
def
19
ref
appTerm
appTerm
"e"
49
ref
var
84
def
varTerm
85
def
appTerm
appTerm
14
ref
15
ref
82
ref
83
ref
67
ref
appTerm
appTerm
77
remove
varTerm
86
def
83
remove
21
ref
appTerm
appTerm
21
ref
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
87
def
appTerm
88
def
absTerm
89
def
86
ref
appTerm
90
def
betaConv
84
remove
12
ref
0
ref
0
ref
76
ref
8
ref
cons
opType
91
def
8
ref
cons
opType
constTerm
89
ref
appTerm
92
def
absTerm
93
def
85
ref
appTerm
94
def
betaConv
nil
12
ref
51
ref
constTerm
95
def
93
ref
appTerm
96
def
axiom
nil
"p"
7
ref
var
97
def
96
remove
nil
cons
cons
"q"
7
ref
var
98
def
94
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
16
ref
10
ref
constTerm
99
def
"Data.Bool.==>"
const
10
ref
constTerm
100
def
97
ref
varTerm
101
def
appTerm
98
ref
varTerm
102
def
appTerm
103
def
appTerm
refl
97
ref
98
ref
99
ref
11
ref
101
ref
appTerm
104
def
102
ref
appTerm
105
def
appTerm
106
def
101
ref
appTerm
absTerm
107
def
absTerm
108
def
101
ref
appTerm
betaConv
102
ref
refl
109
def
appThm
107
remove
102
ref
appTerm
betaConv
trans
appThm
nil
16
ref
0
ref
10
ref
0
ref
10
ref
8
ref
cons
opType
110
def
nil
cons
cons
opType
constTerm
111
def
100
ref
appTerm
108
remove
appTerm
axiom
101
ref
refl
112
def
appThm
109
ref
appThm
eqMp
113
def
sym
114
def
106
remove
refl
98
ref
16
ref
0
ref
110
ref
0
ref
110
remove
8
ref
cons
opType
nil
cons
cons
opType
constTerm
115
def
"f"
10
remove
var
116
def
116
ref
varTerm
117
def
101
ref
appTerm
102
ref
appTerm
absTerm
118
def
appTerm
116
ref
117
ref
"Data.Bool.T"
const
7
ref
constTerm
119
def
appTerm
119
ref
appTerm
absTerm
120
def
appTerm
absTerm
121
def
102
ref
appTerm
betaConv
appThm
16
ref
0
ref
9
ref
0
ref
9
ref
8
ref
cons
opType
122
def
nil
cons
cons
opType
constTerm
123
def
104
remove
appTerm
refl
97
ref
121
remove
absTerm
124
def
101
ref
appTerm
betaConv
appThm
nil
111
remove
11
ref
appTerm
124
ref
appTerm
axiom
125
def
112
remove
appThm
eqMp
109
ref
appThm
eqMp
126
def
sym
116
ref
117
ref
refl
nil
"t"
7
ref
var
127
def
101
ref
nil
cons
128
def
cons
nil
cons
nil
cons
cons
99
ref
127
ref
varTerm
129
def
appTerm
119
ref
appTerm
assume
sym
nil
119
ref
axiom
130
def
eqMp
129
remove
assume
130
ref
deductAntisym
deductAntisym
131
def
subst
101
ref
assume
132
def
eqMp
appThm
nil
127
ref
102
ref
nil
cons
133
def
cons
nil
cons
nil
cons
cons
131
ref
subst
102
ref
assume
eqMp
appThm
absThm
eqMp
134
def
nil
"P"
7
ref
var
135
def
128
remove
cons
"Q"
7
ref
var
136
def
133
remove
cons
nil
cons
cons
nil
cons
cons
99
ref
refl
137
def
116
ref
117
remove
135
ref
varTerm
138
def
appTerm
139
def
136
ref
varTerm
140
def
appTerm
absTerm
141
def
97
ref
98
ref
101
ref
absTerm
absTerm
142
def
appTerm
betaConv
142
ref
138
ref
appTerm
betaConv
140
ref
refl
143
def
appThm
98
ref
138
ref
absTerm
140
ref
appTerm
betaConv
trans
trans
appThm
120
ref
142
ref
appTerm
betaConv
142
ref
119
ref
appTerm
betaConv
119
ref
refl
144
def
appThm
98
ref
119
ref
absTerm
119
ref
appTerm
betaConv
trans
trans
appThm
99
ref
11
ref
138
ref
appTerm
145
def
140
ref
appTerm
146
def
appTerm
refl
98
ref
115
remove
116
remove
139
remove
102
ref
appTerm
absTerm
appTerm
120
ref
appTerm
absTerm
140
ref
appTerm
betaConv
appThm
123
remove
145
remove
appTerm
refl
124
remove
138
ref
appTerm
betaConv
appThm
125
remove
138
ref
refl
appThm
eqMp
143
ref
appThm
eqMp
146
remove
assume
eqMp
147
def
142
remove
refl
appThm
eqMp
sym
130
ref
eqMp
148
def
subst
149
def
deductAntisym
eqMp
113
remove
103
ref
assume
eqMp
sym
132
ref
eqMp
137
ref
118
remove
97
ref
98
ref
102
ref
absTerm
150
def
absTerm
151
def
appTerm
betaConv
151
ref
101
ref
appTerm
betaConv
109
remove
appThm
150
ref
102
ref
appTerm
betaConv
trans
trans
appThm
120
remove
151
ref
appTerm
betaConv
151
ref
119
ref
appTerm
betaConv
144
remove
appThm
150
ref
119
ref
appTerm
betaConv
trans
trans
152
def
appThm
126
remove
105
remove
assume
eqMp
151
ref
refl
153
def
appThm
eqMp
sym
130
ref
eqMp
154
def
proveHyp
deductAntisym
155
def
subst
proveHyp
"A"
58
remove
cons
nil
cons
156
def
"P"
50
ref
var
157
def
93
remove
nil
cons
cons
"x"
49
ref
var
158
def
85
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
97
ref
95
ref
157
ref
varTerm
159
def
appTerm
160
def
nil
cons
161
def
cons
98
ref
159
ref
158
ref
varTerm
162
def
appTerm
163
def
nil
cons
164
def
cons
nil
cons
cons
nil
cons
cons
165
def
114
ref
subst
165
remove
154
remove
134
remove
deductAntisym
166
def
subst
99
ref
163
ref
appTerm
refl
158
ref
119
remove
absTerm
167
def
162
ref
appTerm
betaConv
appThm
56
ref
16
remove
0
remove
50
remove
51
ref
nil
cons
cons
opType
constTerm
57
ref
appTerm
167
remove
appTerm
absTerm
168
def
159
ref
appTerm
betaConv
169
def
nil
52
ref
95
ref
appTerm
168
remove
appTerm
axiom
159
ref
refl
170
def
appThm
171
def
160
ref
assume
eqMp
eqMp
162
ref
refl
appThm
eqMp
sym
130
ref
eqMp
eqMp
nil
135
ref
161
remove
cons
136
ref
164
ref
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
deductAntisym
eqMp
172
def
subst
eqMp
eqMp
nil
97
ref
92
remove
nil
cons
cons
98
ref
90
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
155
ref
subst
proveHyp
"A"
76
ref
nil
cons
cons
nil
cons
"P"
91
remove
var
89
remove
nil
cons
cons
"x"
76
remove
var
86
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
eqMp
eqMp
nil
97
ref
88
remove
nil
cons
cons
98
ref
53
remove
80
remove
constTerm
87
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
155
ref
subst
proveHyp
"A"
75
remove
cons
nil
cons
"P"
79
remove
var
87
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
97
ref
78
remove
51
remove
constTerm
173
def
159
ref
appTerm
174
def
nil
cons
175
def
cons
176
def
98
ref
54
ref
159
ref
appTerm
177
def
nil
cons
178
def
cons
nil
cons
cons
nil
cons
cons
179
def
114
ref
subst
179
remove
166
ref
subst
nil
176
remove
98
ref
11
ref
177
ref
appTerm
95
ref
158
ref
95
ref
"y"
49
remove
var
180
def
100
ref
11
ref
163
ref
appTerm
159
ref
180
ref
varTerm
181
def
appTerm
appTerm
appTerm
82
remove
162
ref
appTerm
181
ref
appTerm
182
def
appTerm
absTerm
appTerm
absTerm
appTerm
183
def
appTerm
184
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
185
def
155
ref
subst
99
ref
174
ref
appTerm
186
def
refl
56
ref
11
ref
54
remove
57
ref
appTerm
appTerm
95
ref
158
ref
95
ref
180
remove
100
ref
11
ref
57
ref
162
ref
appTerm
187
def
appTerm
57
remove
181
remove
appTerm
appTerm
appTerm
182
remove
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
188
def
159
ref
appTerm
betaConv
appThm
nil
52
remove
173
remove
appTerm
188
remove
appTerm
axiom
170
ref
appThm
eqMp
nil
97
ref
186
remove
184
ref
appTerm
nil
cons
cons
98
ref
100
ref
174
remove
appTerm
184
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
155
ref
subst
proveHyp
185
remove
nil
97
ref
99
ref
101
remove
appTerm
102
ref
appTerm
189
def
nil
cons
190
def
cons
98
ref
103
remove
nil
cons
191
def
cons
nil
cons
cons
nil
cons
cons
192
def
114
ref
subst
192
remove
166
ref
subst
114
ref
166
ref
189
remove
assume
132
remove
eqMp
eqMp
149
remove
deductAntisym
eqMp
eqMp
nil
135
ref
190
remove
cons
136
ref
191
remove
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
deductAntisym
eqMp
193
def
subst
eqMp
eqMp
nil
135
ref
178
ref
cons
194
def
136
ref
183
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
proveHyp
eqMp
nil
135
ref
175
remove
cons
136
ref
178
ref
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
deductAntisym
eqMp
subst
eqMp
subst
subst
eqMp
nil
97
ref
62
ref
6
ref
11
remove
64
ref
20
remove
appTerm
66
ref
appTerm
195
def
appTerm
196
def
14
ref
26
ref
64
ref
30
remove
appTerm
15
ref
33
remove
absTerm
197
def
appTerm
absTerm
198
def
appTerm
199
def
appTerm
200
def
absTerm
201
def
appTerm
202
def
nil
cons
cons
98
ref
62
remove
39
ref
appTerm
203
def
nil
cons
204
def
cons
nil
cons
205
def
cons
nil
cons
cons
155
ref
subst
nil
"P"
41
remove
var
206
def
6
ref
100
ref
201
ref
18
ref
appTerm
207
def
appTerm
203
ref
appTerm
208
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
48
remove
99
ref
160
remove
appTerm
refl
169
remove
appThm
171
remove
eqMp
sym
209
def
subst
subst
6
ref
nil
127
ref
208
remove
nil
cons
cons
nil
cons
nil
cons
cons
131
ref
subst
nil
97
ref
207
remove
nil
cons
210
def
cons
205
ref
cons
nil
cons
cons
211
def
114
ref
subst
211
remove
166
ref
subst
6
remove
196
remove
14
ref
15
ref
64
remove
18
ref
67
remove
appTerm
appTerm
72
remove
32
ref
18
ref
21
ref
appTerm
73
ref
appTerm
appTerm
73
remove
appTerm
absTerm
appTerm
absTerm
appTerm
appTerm
absTerm
18
ref
appTerm
212
def
betaConv
212
remove
assume
eqMp
nil
97
ref
200
remove
nil
cons
213
def
cons
205
remove
cons
nil
cons
cons
214
def
155
ref
subst
proveHyp
214
ref
114
ref
subst
214
remove
166
ref
subst
45
remove
sym
nil
135
ref
195
ref
nil
cons
cons
136
ref
199
remove
nil
cons
215
def
cons
nil
cons
cons
nil
cons
cons
216
def
148
ref
subst
nil
"P"
13
remove
var
217
def
24
remove
nil
cons
cons
nil
cons
nil
cons
cons
"A"
2
remove
cons
nil
cons
218
def
47
ref
cons
209
ref
subst
219
def
subst
15
ref
nil
127
ref
23
remove
nil
cons
cons
nil
cons
nil
cons
cons
131
ref
subst
22
remove
refl
66
remove
21
ref
appTerm
betaConv
appThm
195
remove
assume
71
ref
appThm
eqMp
eqMp
absThm
eqMp
proveHyp
nil
97
ref
25
remove
nil
cons
cons
98
ref
38
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
166
ref
subst
proveHyp
216
remove
137
remove
141
remove
151
ref
appTerm
betaConv
151
remove
138
remove
appTerm
betaConv
143
remove
appThm
150
remove
140
ref
appTerm
betaConv
trans
trans
appThm
152
remove
appThm
147
remove
153
remove
appThm
eqMp
sym
130
remove
eqMp
220
def
subst
nil
217
ref
37
remove
nil
cons
cons
nil
cons
nil
cons
cons
219
ref
subst
26
ref
nil
127
ref
36
remove
nil
cons
cons
nil
cons
nil
cons
cons
131
ref
subst
nil
217
ref
35
remove
nil
cons
cons
nil
cons
nil
cons
cons
219
remove
subst
15
ref
nil
127
ref
34
remove
nil
cons
cons
nil
cons
nil
cons
cons
131
ref
subst
31
remove
refl
197
remove
21
ref
appTerm
betaConv
appThm
198
ref
28
ref
appTerm
221
def
betaConv
nil
97
ref
215
remove
cons
98
ref
221
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
155
ref
subst
218
remove
217
remove
198
remove
nil
cons
cons
"x"
1
remove
var
28
ref
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
eqMp
eqMp
71
remove
appThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
proveHyp
eqMp
eqMp
46
ref
206
ref
39
remove
nil
cons
cons
"x"
5
ref
var
222
def
18
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
99
remove
177
ref
appTerm
223
def
refl
56
remove
12
ref
122
remove
constTerm
224
def
98
ref
100
ref
95
ref
158
ref
100
ref
187
remove
appTerm
102
ref
appTerm
absTerm
appTerm
appTerm
102
ref
appTerm
absTerm
appTerm
absTerm
225
def
159
remove
appTerm
betaConv
appThm
nil
55
remove
225
remove
appTerm
axiom
170
remove
appThm
eqMp
226
def
sym
nil
"P"
9
remove
var
227
def
136
ref
100
ref
95
ref
158
ref
100
ref
163
remove
appTerm
228
def
140
ref
appTerm
absTerm
229
def
appTerm
230
def
appTerm
140
ref
appTerm
231
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
"A"
8
remove
cons
nil
cons
232
def
47
remove
cons
209
remove
subst
subst
136
ref
nil
127
remove
231
remove
nil
cons
cons
nil
cons
nil
cons
cons
131
remove
subst
nil
97
ref
230
remove
nil
cons
233
def
cons
234
def
98
ref
140
ref
nil
cons
235
def
cons
nil
cons
236
def
cons
nil
cons
cons
237
def
114
ref
subst
237
ref
166
ref
subst
nil
97
ref
164
remove
cons
236
ref
cons
nil
cons
cons
155
ref
subst
229
ref
162
ref
appTerm
238
def
betaConv
nil
234
ref
98
ref
238
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
155
ref
subst
156
remove
157
remove
229
remove
nil
cons
cons
158
ref
162
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
172
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
135
ref
233
remove
cons
239
def
136
ref
235
ref
cons
nil
cons
240
def
cons
nil
cons
cons
148
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
subst
proveHyp
eqMp
nil
135
ref
213
remove
cons
136
ref
204
remove
cons
nil
cons
241
def
cons
nil
cons
cons
148
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
135
ref
210
remove
cons
241
ref
cons
nil
cons
cons
148
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
97
ref
12
remove
61
remove
constTerm
222
ref
100
ref
201
ref
222
remove
varTerm
appTerm
appTerm
203
ref
appTerm
absTerm
appTerm
nil
cons
cons
98
ref
100
ref
202
remove
appTerm
203
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
155
ref
subst
proveHyp
46
remove
206
remove
201
remove
nil
cons
cons
241
remove
cons
nil
cons
cons
nil
234
remove
98
ref
100
ref
177
remove
appTerm
242
def
140
ref
appTerm
nil
cons
243
def
cons
nil
cons
cons
nil
cons
cons
244
def
114
ref
subst
244
remove
166
ref
subst
nil
97
ref
178
remove
cons
245
def
236
remove
cons
nil
cons
cons
246
def
114
remove
subst
246
remove
166
remove
subst
237
remove
155
ref
subst
98
ref
100
remove
95
remove
158
remove
228
remove
102
ref
appTerm
absTerm
appTerm
appTerm
102
remove
appTerm
absTerm
247
def
140
remove
appTerm
248
def
betaConv
nil
245
remove
98
ref
224
remove
247
ref
appTerm
249
def
nil
cons
250
def
cons
nil
cons
cons
nil
cons
cons
251
def
155
ref
subst
226
remove
nil
97
ref
223
remove
249
ref
appTerm
nil
cons
cons
98
ref
242
remove
249
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
155
ref
subst
proveHyp
251
remove
193
remove
subst
eqMp
eqMp
nil
97
remove
250
remove
cons
98
remove
248
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
155
remove
subst
proveHyp
232
remove
227
remove
247
remove
nil
cons
cons
"x"
7
remove
var
235
remove
cons
nil
cons
cons
nil
cons
cons
172
remove
subst
eqMp
eqMp
eqMp
eqMp
nil
194
remove
240
remove
cons
nil
cons
cons
148
ref
subst
deductAntisym
eqMp
eqMp
nil
239
remove
136
ref
243
remove
cons
nil
cons
cons
nil
cons
cons
148
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
proveHyp
eqMp
eqMp
defineConstList
252
def
pop
253
def
pop
252
ref
nil
135
remove
14
ref
15
ref
17
ref
253
remove
hdTl
pop
5
remove
constTerm
254
def
19
ref
appTerm
21
ref
appTerm
appTerm
19
remove
appTerm
absTerm
appTerm
255
def
nil
cons
cons
136
remove
14
ref
26
remove
14
remove
15
remove
17
remove
254
ref
29
remove
appTerm
21
ref
appTerm
appTerm
32
remove
254
remove
28
remove
appTerm
21
ref
appTerm
appTerm
21
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
256
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
257
def
220
remove
subst
proveHyp
nil
256
remove
thm
252
remove
257
remove
148
remove
subst
proveHyp
nil
255
remove
thm