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