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