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