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