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