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