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