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