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