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