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