6
version
"Data.Bool.~"
const
"->"
typeOp
0
def
"bool"
typeOp
nil
opType
1
def
1
ref
nil
cons
2
def
cons
opType
3
def
constTerm
4
def
refl
5
def
"="
const
6
def
0
ref
"Number.Natural.natural"
typeOp
nil
opType
7
def
0
ref
7
ref
2
ref
cons
opType
8
def
nil
cons
9
def
cons
opType
10
def
constTerm
11
def
refl
12
def
"Data.Word.modulus"
"Number.Natural.^"
const
0
ref
7
ref
0
ref
7
ref
7
ref
nil
cons
13
def
cons
opType
14
def
nil
cons
cons
opType
15
def
constTerm
16
def
"Number.Natural.bit0"
const
14
ref
constTerm
17
def
"Number.Natural.bit1"
const
14
ref
constTerm
18
def
"Number.Natural.zero"
const
7
ref
constTerm
19
def
appTerm
20
def
appTerm
21
def
appTerm
"Data.Word.width"
const
7
ref
constTerm
22
def
appTerm
23
def
defineConst
24
def
pop
25
def
pop
24
ref
appThm
19
ref
refl
appThm
nil
"n"
7
ref
var
26
def
22
ref
nil
cons
cons
"m"
7
ref
var
27
def
21
remove
nil
cons
28
def
cons
nil
cons
cons
nil
cons
cons
26
ref
6
ref
0
ref
1
ref
3
ref
nil
cons
cons
opType
29
def
constTerm
30
def
11
ref
16
remove
27
ref
varTerm
31
def
appTerm
26
ref
varTerm
32
def
appTerm
appTerm
19
ref
appTerm
appTerm
"Data.Bool./\\"
const
29
ref
constTerm
33
def
11
ref
31
ref
appTerm
34
def
19
ref
appTerm
appTerm
4
ref
11
ref
32
ref
appTerm
35
def
19
ref
appTerm
appTerm
appTerm
appTerm
absTerm
36
def
32
ref
appTerm
37
def
betaConv
27
ref
"Data.Bool.!"
const
38
def
0
ref
8
ref
2
ref
cons
opType
39
def
constTerm
40
def
36
ref
appTerm
41
def
absTerm
42
def
31
ref
appTerm
43
def
betaConv
nil
40
ref
42
ref
appTerm
44
def
axiom
nil
"p"
1
ref
var
45
def
44
remove
nil
cons
cons
"q"
1
ref
var
46
def
43
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
30
ref
"Data.Bool.==>"
const
29
ref
constTerm
47
def
45
ref
varTerm
48
def
appTerm
49
def
46
ref
varTerm
50
def
appTerm
51
def
appTerm
refl
45
ref
46
ref
30
ref
33
ref
48
ref
appTerm
52
def
50
ref
appTerm
53
def
appTerm
54
def
48
ref
appTerm
absTerm
55
def
absTerm
56
def
48
ref
appTerm
betaConv
50
ref
refl
57
def
appThm
55
remove
50
ref
appTerm
betaConv
trans
appThm
nil
6
ref
0
ref
29
ref
0
ref
29
ref
2
ref
cons
opType
58
def
nil
cons
cons
opType
constTerm
59
def
47
ref
appTerm
56
remove
appTerm
axiom
48
ref
refl
60
def
appThm
57
ref
appThm
eqMp
61
def
sym
62
def
54
remove
refl
46
ref
6
ref
0
ref
58
ref
0
ref
58
remove
2
ref
cons
opType
nil
cons
cons
opType
constTerm
63
def
"f"
29
ref
var
64
def
64
ref
varTerm
65
def
48
ref
appTerm
50
ref
appTerm
absTerm
66
def
appTerm
64
ref
65
ref
"Data.Bool.T"
const
1
ref
constTerm
67
def
appTerm
67
ref
appTerm
absTerm
68
def
appTerm
absTerm
69
def
50
ref
appTerm
betaConv
appThm
6
ref
0
ref
3
ref
0
ref
3
ref
2
ref
cons
opType
70
def
nil
cons
cons
opType
constTerm
71
def
52
remove
appTerm
refl
45
ref
69
remove
absTerm
72
def
48
ref
appTerm
betaConv
appThm
nil
59
ref
33
ref
appTerm
72
ref
appTerm
axiom
73
def
60
remove
appThm
eqMp
57
ref
appThm
eqMp
74
def
sym
64
ref
65
ref
refl
nil
"t"
1
ref
var
75
def
48
ref
nil
cons
76
def
cons
nil
cons
nil
cons
cons
77
def
30
ref
75
ref
varTerm
78
def
appTerm
79
def
67
ref
appTerm
80
def
assume
sym
nil
67
ref
axiom
81
def
eqMp
78
ref
assume
81
ref
deductAntisym
deductAntisym
82
def
subst
48
ref
assume
83
def
eqMp
appThm
nil
75
ref
50
ref
nil
cons
84
def
cons
nil
cons
nil
cons
cons
85
def
82
ref
subst
50
ref
assume
eqMp
appThm
absThm
eqMp
86
def
nil
"P"
1
ref
var
87
def
76
ref
cons
"Q"
1
ref
var
88
def
84
remove
cons
nil
cons
cons
nil
cons
cons
30
ref
refl
89
def
64
ref
65
remove
87
ref
varTerm
90
def
appTerm
91
def
88
ref
varTerm
92
def
appTerm
absTerm
93
def
45
ref
46
ref
48
ref
absTerm
absTerm
94
def
appTerm
betaConv
94
ref
90
ref
appTerm
betaConv
92
ref
refl
95
def
appThm
46
ref
90
ref
absTerm
92
ref
appTerm
betaConv
trans
trans
appThm
68
ref
94
ref
appTerm
betaConv
94
ref
67
ref
appTerm
betaConv
67
ref
refl
96
def
appThm
46
ref
67
ref
absTerm
67
ref
appTerm
betaConv
trans
trans
appThm
30
ref
33
ref
90
ref
appTerm
97
def
92
ref
appTerm
98
def
appTerm
refl
46
ref
63
remove
64
remove
91
remove
50
ref
appTerm
absTerm
appTerm
68
ref
appTerm
absTerm
92
ref
appTerm
betaConv
appThm
71
ref
97
remove
appTerm
refl
72
remove
90
ref
appTerm
betaConv
appThm
73
remove
90
ref
refl
99
def
appThm
eqMp
95
ref
appThm
eqMp
98
remove
assume
eqMp
100
def
94
remove
refl
appThm
eqMp
sym
81
ref
eqMp
101
def
subst
deductAntisym
eqMp
61
remove
51
remove
assume
eqMp
sym
83
remove
eqMp
89
ref
66
remove
45
ref
46
ref
50
ref
absTerm
102
def
absTerm
103
def
appTerm
betaConv
103
ref
48
ref
appTerm
betaConv
57
remove
appThm
102
ref
50
ref
appTerm
betaConv
trans
trans
appThm
68
remove
103
ref
appTerm
betaConv
103
ref
67
ref
appTerm
betaConv
96
remove
appThm
102
ref
67
ref
appTerm
betaConv
trans
trans
104
def
appThm
74
remove
53
remove
assume
eqMp
103
ref
refl
105
def
appThm
eqMp
sym
81
ref
eqMp
106
def
proveHyp
deductAntisym
107
def
subst
proveHyp
"A"
13
remove
cons
nil
cons
108
def
"P"
8
ref
var
109
def
42
remove
nil
cons
cons
"x"
7
ref
var
110
def
31
ref
nil
cons
111
def
cons
nil
cons
112
def
cons
nil
cons
cons
nil
45
ref
38
ref
0
ref
0
ref
"A"
varType
113
def
2
ref
cons
opType
114
def
2
ref
cons
opType
115
def
constTerm
116
def
"P"
114
ref
var
varTerm
117
def
appTerm
118
def
nil
cons
119
def
cons
46
ref
117
ref
"x"
113
ref
var
120
def
varTerm
121
def
appTerm
122
def
nil
cons
123
def
cons
nil
cons
cons
nil
cons
cons
124
def
62
ref
subst
124
remove
106
remove
86
remove
deductAntisym
125
def
subst
30
ref
122
ref
appTerm
refl
120
ref
67
ref
absTerm
126
def
121
ref
appTerm
betaConv
appThm
"p"
114
ref
var
127
def
6
ref
0
ref
114
ref
115
ref
nil
cons
cons
opType
constTerm
127
ref
varTerm
128
def
appTerm
126
remove
appTerm
absTerm
129
def
117
ref
appTerm
betaConv
130
def
nil
6
ref
0
ref
115
ref
0
ref
115
ref
2
ref
cons
opType
131
def
nil
cons
cons
opType
constTerm
116
ref
appTerm
129
remove
appTerm
axiom
117
ref
refl
appThm
132
def
118
ref
assume
eqMp
eqMp
121
ref
refl
133
def
appThm
eqMp
sym
81
ref
eqMp
eqMp
nil
87
ref
119
remove
cons
88
ref
123
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
134
def
subst
eqMp
eqMp
nil
45
ref
41
remove
nil
cons
cons
46
ref
37
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
108
ref
109
ref
36
remove
nil
cons
cons
110
ref
32
ref
nil
cons
135
def
cons
nil
cons
136
def
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
subst
trans
appThm
sym
5
ref
33
ref
refl
137
def
"Number.Natural.suc"
const
14
remove
constTerm
138
def
refl
139
def
nil
26
ref
19
ref
nil
cons
140
def
cons
nil
cons
nil
cons
cons
141
def
nil
27
ref
18
remove
32
ref
appTerm
142
def
nil
cons
cons
nil
cons
nil
cons
cons
27
ref
11
ref
"Number.Natural.+"
const
15
remove
constTerm
143
def
31
ref
appTerm
144
def
19
ref
appTerm
appTerm
31
ref
appTerm
absTerm
145
def
31
ref
appTerm
146
def
betaConv
nil
40
ref
145
ref
appTerm
147
def
axiom
nil
45
ref
147
remove
nil
cons
cons
46
ref
146
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
108
ref
109
ref
145
remove
nil
cons
cons
112
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
subst
subst
appThm
141
ref
26
ref
11
ref
138
ref
142
ref
appTerm
appTerm
17
ref
138
ref
32
ref
appTerm
148
def
appTerm
149
def
appTerm
absTerm
150
def
32
ref
appTerm
151
def
betaConv
137
ref
40
ref
refl
152
def
26
ref
nil
110
ref
148
ref
nil
cons
153
def
cons
nil
cons
nil
cons
cons
108
ref
nil
nil
cons
154
def
cons
155
def
nil
75
ref
6
ref
0
ref
113
ref
114
ref
nil
cons
156
def
cons
opType
constTerm
121
ref
appTerm
121
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
82
ref
subst
133
remove
eqMp
157
def
subst
158
def
subst
absThm
appThm
nil
75
ref
67
ref
nil
cons
cons
nil
cons
nil
cons
cons
159
def
155
ref
75
ref
30
ref
116
ref
120
ref
78
ref
absTerm
appTerm
appTerm
78
ref
appTerm
absTerm
160
def
78
ref
appTerm
161
def
betaConv
nil
38
ref
70
remove
constTerm
162
def
160
ref
appTerm
163
def
axiom
nil
45
ref
163
remove
nil
cons
cons
46
ref
161
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
"A"
2
ref
cons
nil
cons
164
def
"P"
3
remove
var
165
def
160
remove
nil
cons
cons
"x"
1
ref
var
166
def
78
ref
nil
cons
cons
nil
cons
167
def
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
subst
subst
168
def
trans
appThm
137
ref
11
ref
138
ref
19
ref
appTerm
169
def
appTerm
170
def
refl
141
ref
26
ref
11
ref
142
ref
appTerm
138
ref
17
ref
32
ref
appTerm
171
def
appTerm
172
def
appTerm
absTerm
173
def
32
ref
appTerm
174
def
betaConv
nil
40
ref
173
ref
appTerm
175
def
axiom
nil
45
ref
175
remove
nil
cons
cons
46
ref
174
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
108
ref
109
ref
173
remove
nil
cons
cons
136
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
139
ref
26
ref
11
ref
171
remove
appTerm
143
ref
32
ref
appTerm
176
def
32
ref
appTerm
177
def
appTerm
178
def
absTerm
179
def
32
ref
appTerm
180
def
betaConv
181
def
12
ref
nil
11
ref
17
ref
19
ref
appTerm
appTerm
182
def
19
ref
appTerm
axiom
appThm
141
remove
26
ref
11
ref
143
ref
19
ref
appTerm
183
def
32
ref
appTerm
appTerm
32
ref
appTerm
absTerm
184
def
32
ref
appTerm
185
def
betaConv
nil
40
ref
184
ref
appTerm
186
def
axiom
nil
45
ref
186
remove
nil
cons
cons
46
ref
185
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
108
ref
109
ref
184
remove
nil
cons
cons
136
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
subst
187
def
appThm
nil
110
ref
140
ref
cons
nil
cons
nil
cons
cons
158
ref
subst
trans
sym
81
ref
eqMp
nil
45
ref
182
remove
183
remove
19
ref
appTerm
appTerm
188
def
nil
cons
cons
46
ref
40
ref
26
ref
47
ref
178
ref
appTerm
11
ref
149
remove
appTerm
189
def
143
ref
148
ref
appTerm
148
ref
appTerm
appTerm
190
def
appTerm
191
def
absTerm
192
def
appTerm
193
def
nil
cons
cons
nil
cons
cons
nil
cons
cons
125
ref
subst
proveHyp
nil
109
ref
192
remove
nil
cons
cons
nil
cons
nil
cons
cons
155
ref
30
ref
118
remove
appTerm
refl
130
remove
appThm
132
remove
eqMp
sym
subst
subst
26
ref
nil
75
ref
191
remove
nil
cons
cons
nil
cons
nil
cons
cons
82
remove
subst
nil
45
ref
178
ref
nil
cons
194
def
cons
46
ref
190
remove
nil
cons
195
def
cons
nil
cons
cons
nil
cons
cons
196
def
62
ref
subst
196
remove
125
ref
subst
12
ref
26
ref
189
remove
138
ref
172
ref
appTerm
appTerm
absTerm
197
def
32
ref
appTerm
198
def
betaConv
nil
40
ref
197
ref
appTerm
199
def
axiom
nil
45
ref
199
remove
nil
cons
cons
46
ref
198
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
108
ref
109
ref
197
remove
nil
cons
cons
136
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
139
ref
139
ref
178
remove
assume
appThm
appThm
trans
appThm
nil
26
ref
153
remove
cons
200
def
27
ref
135
remove
cons
nil
cons
201
def
cons
nil
cons
cons
26
ref
11
ref
143
ref
138
ref
31
ref
appTerm
appTerm
32
ref
appTerm
appTerm
138
ref
144
ref
32
ref
appTerm
202
def
appTerm
203
def
appTerm
absTerm
204
def
32
ref
appTerm
205
def
betaConv
27
ref
40
ref
204
ref
appTerm
206
def
absTerm
207
def
31
ref
appTerm
208
def
betaConv
nil
40
ref
207
ref
appTerm
209
def
axiom
nil
45
ref
209
remove
nil
cons
cons
46
ref
208
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
108
ref
109
ref
207
remove
nil
cons
cons
112
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
nil
45
ref
206
remove
nil
cons
cons
46
ref
205
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
108
ref
109
ref
204
remove
nil
cons
cons
136
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
210
def
subst
211
def
139
ref
nil
201
remove
nil
cons
cons
26
ref
11
ref
144
ref
148
ref
appTerm
appTerm
203
remove
appTerm
absTerm
212
def
32
ref
appTerm
213
def
betaConv
27
ref
40
ref
212
ref
appTerm
214
def
absTerm
215
def
31
ref
appTerm
216
def
betaConv
nil
40
ref
215
ref
appTerm
217
def
axiom
nil
45
ref
217
remove
nil
cons
cons
46
ref
216
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
108
ref
109
ref
215
remove
nil
cons
cons
112
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
nil
45
ref
214
remove
nil
cons
cons
46
ref
213
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
108
ref
109
ref
212
remove
nil
cons
cons
136
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
218
def
subst
appThm
219
def
trans
appThm
nil
110
ref
138
ref
138
ref
177
remove
appTerm
220
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
158
ref
subst
221
def
trans
sym
81
ref
eqMp
eqMp
nil
87
ref
194
remove
cons
88
ref
195
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
eqMp
nil
45
ref
33
ref
188
remove
appTerm
193
remove
appTerm
nil
cons
cons
46
ref
40
ref
179
ref
appTerm
nil
cons
222
def
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
47
ref
refl
223
def
137
ref
179
ref
19
ref
appTerm
betaConv
appThm
152
ref
26
ref
223
remove
181
ref
appThm
179
ref
148
ref
appTerm
betaConv
appThm
absThm
appThm
appThm
appThm
152
ref
26
ref
181
remove
absThm
appThm
appThm
nil
"p"
8
ref
var
224
def
179
remove
nil
cons
225
def
cons
nil
cons
nil
cons
cons
224
ref
47
ref
33
ref
224
remove
varTerm
226
def
19
ref
appTerm
appTerm
40
ref
26
ref
47
ref
226
ref
32
ref
appTerm
227
def
appTerm
226
ref
148
ref
appTerm
appTerm
absTerm
appTerm
appTerm
appTerm
40
ref
26
ref
227
remove
absTerm
appTerm
appTerm
absTerm
228
def
226
ref
appTerm
229
def
betaConv
nil
38
ref
0
ref
39
ref
2
ref
cons
opType
constTerm
228
ref
appTerm
230
def
axiom
nil
45
ref
230
remove
nil
cons
cons
46
ref
229
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
"A"
9
remove
cons
nil
cons
"P"
39
ref
var
228
remove
nil
cons
cons
"x"
8
remove
var
226
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
subst
eqMp
eqMp
nil
45
ref
222
remove
cons
46
ref
180
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
108
ref
109
ref
225
remove
cons
136
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
231
def
appThm
232
def
trans
233
def
subst
139
ref
187
remove
appThm
trans
appThm
nil
110
ref
169
remove
nil
cons
cons
nil
cons
nil
cons
cons
158
ref
subst
trans
appThm
137
ref
152
ref
26
ref
12
ref
232
remove
appThm
233
ref
appThm
nil
110
ref
220
remove
nil
cons
cons
nil
cons
nil
cons
cons
158
remove
subst
trans
absThm
appThm
168
ref
trans
appThm
152
ref
26
ref
12
remove
139
ref
233
remove
appThm
appThm
nil
200
remove
nil
cons
nil
cons
cons
231
remove
subst
211
remove
trans
219
remove
trans
appThm
221
remove
trans
absThm
appThm
168
remove
trans
appThm
159
remove
75
ref
30
ref
33
ref
67
ref
appTerm
78
ref
appTerm
appTerm
78
ref
appTerm
absTerm
234
def
78
ref
appTerm
235
def
betaConv
nil
162
ref
234
ref
appTerm
236
def
axiom
nil
45
ref
236
remove
nil
cons
cons
46
ref
235
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
164
ref
165
ref
234
remove
nil
cons
cons
167
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
237
def
subst
238
def
trans
appThm
238
ref
trans
appThm
238
remove
trans
sym
81
ref
eqMp
nil
87
ref
40
ref
26
ref
11
ref
148
ref
appTerm
148
remove
appTerm
absTerm
appTerm
nil
cons
cons
88
ref
33
ref
170
remove
20
ref
appTerm
239
def
appTerm
33
ref
40
ref
26
ref
11
ref
172
remove
appTerm
142
remove
appTerm
absTerm
appTerm
240
def
appTerm
40
ref
150
ref
appTerm
241
def
appTerm
242
def
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
89
ref
93
remove
103
ref
appTerm
betaConv
103
remove
90
ref
appTerm
betaConv
95
ref
appThm
102
remove
92
ref
appTerm
betaConv
trans
trans
appThm
104
remove
appThm
100
remove
105
remove
appThm
eqMp
sym
81
ref
eqMp
243
def
subst
proveHyp
244
def
nil
87
ref
239
remove
nil
cons
cons
88
ref
242
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
245
def
243
ref
subst
proveHyp
nil
87
ref
240
remove
nil
cons
cons
88
ref
241
remove
nil
cons
246
def
cons
nil
cons
cons
nil
cons
cons
243
remove
subst
proveHyp
nil
45
ref
246
remove
cons
46
ref
151
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
108
ref
109
ref
150
remove
nil
cons
cons
136
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
subst
17
remove
refl
244
remove
245
remove
101
ref
subst
proveHyp
appThm
trans
trans
247
def
nil
27
ref
20
remove
nil
cons
cons
26
ref
28
remove
cons
"p"
7
ref
var
248
def
140
remove
cons
nil
cons
cons
cons
nil
cons
cons
30
ref
"_9306"
7
ref
var
249
def
30
ref
11
ref
249
remove
varTerm
appTerm
248
remove
varTerm
250
def
appTerm
appTerm
"Data.Bool.F"
const
1
ref
constTerm
251
def
appTerm
absTerm
252
def
32
ref
appTerm
253
def
appTerm
refl
252
ref
138
ref
144
ref
250
ref
appTerm
254
def
appTerm
255
def
appTerm
betaConv
appThm
89
ref
253
remove
betaConv
appThm
30
ref
11
ref
255
ref
appTerm
256
def
250
ref
appTerm
257
def
appTerm
251
ref
appTerm
refl
appThm
trans
252
remove
refl
256
ref
32
ref
appTerm
assume
sym
appThm
eqMp
sym
nil
75
ref
257
remove
nil
cons
cons
nil
cons
nil
cons
cons
75
ref
30
ref
79
remove
251
ref
appTerm
258
def
appTerm
4
ref
78
ref
appTerm
259
def
appTerm
absTerm
260
def
78
ref
appTerm
261
def
betaConv
nil
162
ref
260
ref
appTerm
262
def
axiom
nil
45
ref
262
remove
nil
cons
cons
46
ref
261
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
164
ref
165
ref
260
remove
nil
cons
cons
167
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
subst
5
ref
nil
26
ref
250
ref
nil
cons
263
def
cons
27
ref
255
ref
nil
cons
264
def
cons
nil
cons
cons
nil
cons
cons
265
def
26
ref
30
ref
34
remove
32
ref
appTerm
266
def
appTerm
33
ref
"Number.Natural.<="
const
10
ref
constTerm
267
def
31
ref
appTerm
32
ref
appTerm
268
def
appTerm
267
ref
32
ref
appTerm
31
ref
appTerm
appTerm
269
def
appTerm
270
def
absTerm
271
def
32
ref
appTerm
272
def
betaConv
27
ref
40
ref
271
ref
appTerm
273
def
absTerm
274
def
31
ref
appTerm
275
def
betaConv
152
ref
27
ref
152
ref
26
ref
270
remove
assume
sym
30
ref
269
remove
appTerm
266
remove
appTerm
276
def
assume
sym
deductAntisym
absThm
appThm
absThm
appThm
nil
40
ref
27
ref
40
ref
26
ref
276
remove
absTerm
appTerm
absTerm
appTerm
axiom
eqMp
nil
45
ref
40
ref
274
ref
appTerm
nil
cons
cons
46
ref
275
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
108
ref
109
ref
274
remove
nil
cons
cons
112
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
nil
45
ref
273
remove
nil
cons
cons
46
ref
272
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
108
ref
109
ref
271
remove
nil
cons
cons
136
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
subst
appThm
nil
"t2"
1
ref
var
277
def
267
ref
250
ref
appTerm
255
ref
appTerm
nil
cons
cons
"t1"
1
ref
var
278
def
267
remove
255
remove
appTerm
250
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
277
ref
30
ref
4
ref
33
ref
278
ref
varTerm
279
def
appTerm
277
remove
varTerm
280
def
appTerm
appTerm
appTerm
"Data.Bool.\\/"
const
29
remove
constTerm
281
def
4
ref
279
ref
appTerm
appTerm
4
ref
280
ref
appTerm
appTerm
appTerm
absTerm
282
def
280
ref
appTerm
283
def
betaConv
278
remove
162
ref
282
ref
appTerm
284
def
absTerm
285
def
279
ref
appTerm
286
def
betaConv
nil
162
ref
285
ref
appTerm
287
def
axiom
nil
45
ref
287
remove
nil
cons
cons
46
ref
286
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
164
ref
165
ref
285
remove
nil
cons
cons
166
ref
279
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
nil
45
ref
284
remove
nil
cons
cons
46
ref
283
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
164
ref
165
ref
282
remove
nil
cons
cons
166
ref
280
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
subst
trans
trans
sym
281
ref
refl
265
ref
26
ref
30
ref
4
ref
268
remove
appTerm
appTerm
"Number.Natural.<"
const
10
remove
constTerm
288
def
32
ref
appTerm
31
ref
appTerm
appTerm
absTerm
289
def
32
ref
appTerm
290
def
betaConv
27
ref
40
ref
289
ref
appTerm
291
def
absTerm
292
def
31
ref
appTerm
293
def
betaConv
nil
40
ref
292
ref
appTerm
294
def
axiom
nil
45
ref
294
remove
nil
cons
cons
46
ref
293
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
108
ref
109
ref
292
remove
nil
cons
cons
112
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
nil
45
ref
291
remove
nil
cons
cons
46
ref
290
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
108
ref
109
ref
289
remove
nil
cons
cons
136
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
295
def
subst
nil
26
ref
264
remove
cons
27
ref
263
ref
cons
nil
cons
296
def
cons
nil
cons
cons
297
def
26
ref
30
ref
288
remove
31
ref
appTerm
32
ref
appTerm
appTerm
"Data.Bool.?"
const
298
def
39
remove
constTerm
299
def
"d"
7
ref
var
300
def
35
remove
144
remove
138
ref
300
ref
varTerm
301
def
appTerm
302
def
appTerm
appTerm
absTerm
appTerm
appTerm
absTerm
303
def
32
ref
appTerm
304
def
betaConv
27
ref
40
ref
303
ref
appTerm
305
def
absTerm
306
def
31
ref
appTerm
307
def
betaConv
nil
40
ref
306
ref
appTerm
308
def
axiom
nil
45
ref
308
remove
nil
cons
cons
46
ref
307
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
108
ref
109
ref
306
remove
nil
cons
cons
112
remove
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
nil
45
ref
305
remove
nil
cons
cons
46
ref
304
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
108
ref
109
ref
303
remove
nil
cons
cons
136
remove
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
309
def
subst
trans
299
ref
refl
310
def
300
ref
256
ref
refl
nil
26
ref
301
ref
nil
cons
cons
311
def
296
remove
cons
nil
cons
cons
218
ref
subst
appThm
absThm
appThm
trans
appThm
297
remove
295
remove
subst
265
remove
309
remove
subst
trans
310
remove
300
ref
11
ref
250
ref
appTerm
312
def
refl
nil
26
ref
302
remove
nil
cons
cons
27
ref
254
ref
nil
cons
313
def
cons
nil
cons
314
def
cons
nil
cons
cons
210
remove
subst
139
ref
nil
311
remove
314
remove
cons
nil
cons
cons
218
remove
subst
appThm
trans
appThm
absThm
appThm
trans
appThm
sym
nil
45
ref
281
ref
299
ref
300
ref
256
ref
138
ref
143
ref
250
remove
appTerm
315
def
301
ref
appTerm
appTerm
appTerm
316
def
absTerm
317
def
appTerm
318
def
appTerm
299
remove
300
ref
312
remove
138
ref
138
ref
143
ref
254
ref
appTerm
301
ref
appTerm
appTerm
appTerm
appTerm
319
def
absTerm
320
def
appTerm
321
def
appTerm
322
def
nil
cons
cons
nil
cons
nil
cons
cons
30
ref
48
ref
appTerm
323
def
refl
324
def
nil
75
ref
4
ref
48
ref
appTerm
325
def
nil
cons
326
def
cons
nil
cons
nil
cons
cons
75
ref
30
ref
47
ref
78
ref
appTerm
251
ref
appTerm
appTerm
259
ref
appTerm
absTerm
327
def
78
ref
appTerm
328
def
betaConv
nil
162
ref
327
ref
appTerm
329
def
axiom
nil
45
ref
329
remove
nil
cons
cons
46
ref
328
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
164
ref
165
ref
327
remove
nil
cons
cons
167
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
330
def
subst
appThm
sym
324
remove
77
ref
75
ref
30
ref
4
ref
259
ref
appTerm
appTerm
78
ref
appTerm
absTerm
331
def
78
ref
appTerm
332
def
betaConv
nil
162
ref
331
ref
appTerm
333
def
axiom
nil
45
ref
333
remove
nil
cons
cons
46
ref
332
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
164
ref
165
ref
331
remove
nil
cons
cons
167
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
subst
appThm
nil
166
ref
76
remove
cons
nil
cons
334
def
nil
cons
cons
164
ref
154
ref
cons
157
remove
subst
335
def
subst
trans
sym
81
ref
eqMp
eqMp
subst
sym
nil
45
ref
4
ref
322
remove
appTerm
336
def
nil
cons
337
def
cons
46
ref
251
ref
nil
cons
338
def
cons
nil
cons
339
def
cons
nil
cons
cons
340
def
62
ref
subst
340
remove
125
ref
subst
nil
40
ref
27
remove
40
ref
26
ref
11
ref
202
remove
appTerm
176
ref
31
ref
appTerm
appTerm
absTerm
appTerm
absTerm
341
def
appTerm
342
def
axiom
nil
45
ref
342
remove
nil
cons
343
def
cons
344
def
339
ref
cons
nil
cons
cons
345
def
107
ref
subst
proveHyp
345
ref
62
ref
subst
345
remove
125
ref
subst
nil
"_9309"
7
ref
var
346
def
263
remove
cons
"_9308"
7
ref
var
347
def
111
ref
cons
nil
cons
cons
nil
cons
cons
26
remove
11
ref
143
remove
347
remove
varTerm
348
def
appTerm
32
remove
appTerm
appTerm
176
remove
348
ref
appTerm
appTerm
absTerm
349
def
346
remove
varTerm
350
def
appTerm
351
def
betaConv
341
ref
348
ref
appTerm
352
def
betaConv
nil
344
remove
46
ref
352
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
108
ref
109
ref
341
remove
nil
cons
cons
110
ref
348
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
nil
45
ref
40
ref
349
ref
appTerm
nil
cons
cons
46
ref
351
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
108
ref
109
ref
349
remove
nil
cons
cons
110
ref
350
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
subst
nil
45
ref
11
ref
254
remove
appTerm
315
ref
31
remove
appTerm
353
def
appTerm
nil
cons
cons
46
ref
256
ref
138
ref
353
ref
appTerm
appTerm
nil
cons
354
def
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
nil
"_9313"
7
ref
var
355
def
353
remove
nil
cons
cons
"_9312"
7
ref
var
356
def
313
remove
cons
nil
cons
cons
nil
cons
cons
nil
45
ref
11
ref
356
remove
varTerm
357
def
appTerm
355
remove
varTerm
358
def
appTerm
359
def
nil
cons
360
def
cons
46
ref
11
ref
138
ref
357
remove
appTerm
appTerm
138
ref
358
remove
appTerm
appTerm
nil
cons
361
def
cons
nil
cons
cons
nil
cons
cons
362
def
62
ref
subst
362
remove
125
ref
subst
139
remove
359
remove
assume
appThm
eqMp
nil
87
ref
360
remove
cons
88
ref
361
remove
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
subst
eqMp
nil
45
ref
354
remove
cons
339
remove
cons
nil
cons
cons
107
ref
subst
proveHyp
nil
"_9310"
7
ref
var
363
def
111
remove
cons
nil
cons
nil
cons
cons
nil
45
ref
256
remove
138
remove
315
remove
363
remove
varTerm
364
def
appTerm
appTerm
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
30
ref
325
ref
appTerm
refl
77
remove
330
remove
subst
appThm
nil
166
ref
326
remove
cons
nil
cons
nil
cons
cons
335
ref
subst
trans
sym
81
ref
eqMp
subst
300
ref
4
ref
316
remove
appTerm
absTerm
365
def
364
ref
appTerm
366
def
betaConv
nil
45
ref
318
remove
nil
cons
cons
46
ref
321
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
45
ref
323
ref
251
ref
appTerm
367
def
nil
cons
368
def
cons
46
ref
30
ref
4
ref
281
ref
48
ref
appTerm
50
ref
appTerm
appTerm
appTerm
33
ref
325
remove
appTerm
4
ref
50
ref
appTerm
369
def
appTerm
appTerm
nil
cons
370
def
cons
nil
cons
371
def
cons
nil
cons
cons
372
def
62
ref
subst
372
remove
125
ref
subst
30
ref
"_534"
1
ref
var
373
def
30
ref
4
ref
281
ref
373
remove
varTerm
374
def
appTerm
50
ref
appTerm
appTerm
appTerm
33
ref
4
ref
374
remove
appTerm
appTerm
369
ref
appTerm
appTerm
absTerm
375
def
48
ref
appTerm
376
def
appTerm
refl
377
def
375
ref
251
ref
appTerm
betaConv
appThm
89
ref
376
remove
betaConv
appThm
378
def
30
ref
4
ref
281
ref
251
ref
appTerm
379
def
50
ref
appTerm
appTerm
appTerm
33
ref
4
ref
251
ref
appTerm
380
def
appTerm
369
ref
appTerm
appTerm
refl
appThm
trans
375
remove
refl
381
def
367
remove
assume
appThm
eqMp
sym
89
ref
5
ref
85
ref
75
ref
30
ref
379
remove
78
ref
appTerm
appTerm
78
ref
appTerm
absTerm
382
def
78
ref
appTerm
383
def
betaConv
nil
162
ref
382
ref
appTerm
384
def
axiom
nil
45
ref
384
remove
nil
cons
cons
46
ref
383
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
164
ref
165
ref
382
remove
nil
cons
cons
167
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
subst
appThm
appThm
137
ref
nil
30
ref
380
remove
appTerm
67
ref
appTerm
axiom
385
def
appThm
369
ref
refl
386
def
appThm
nil
75
ref
369
ref
nil
cons
387
def
cons
nil
cons
nil
cons
cons
388
def
237
remove
subst
trans
appThm
nil
166
ref
387
remove
cons
nil
cons
nil
cons
cons
335
remove
subst
trans
sym
81
ref
eqMp
eqMp
eqMp
nil
87
ref
368
ref
cons
88
ref
370
ref
cons
nil
cons
389
def
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
nil
45
ref
323
remove
67
ref
appTerm
390
def
nil
cons
391
def
cons
371
remove
cons
nil
cons
cons
392
def
62
remove
subst
392
remove
125
remove
subst
377
remove
"_532"
1
ref
var
393
def
30
ref
4
ref
281
ref
393
remove
varTerm
394
def
appTerm
50
ref
appTerm
appTerm
appTerm
33
ref
4
ref
394
remove
appTerm
appTerm
369
ref
appTerm
appTerm
absTerm
67
ref
appTerm
betaConv
appThm
378
remove
30
ref
4
ref
281
ref
67
ref
appTerm
395
def
50
ref
appTerm
appTerm
appTerm
33
ref
4
ref
67
ref
appTerm
396
def
appTerm
369
remove
appTerm
appTerm
refl
appThm
trans
381
remove
390
remove
assume
appThm
eqMp
sym
89
ref
5
ref
85
remove
75
ref
30
ref
395
remove
78
ref
appTerm
appTerm
67
remove
appTerm
absTerm
397
def
78
ref
appTerm
398
def
betaConv
nil
162
ref
397
ref
appTerm
399
def
axiom
nil
45
ref
399
remove
nil
cons
cons
46
ref
398
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
164
ref
165
ref
397
remove
nil
cons
cons
167
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
subst
appThm
nil
30
ref
396
remove
appTerm
251
ref
appTerm
axiom
400
def
trans
appThm
137
ref
400
remove
appThm
386
remove
appThm
388
remove
75
ref
30
ref
33
remove
251
ref
appTerm
78
ref
appTerm
appTerm
251
ref
appTerm
absTerm
401
def
78
ref
appTerm
402
def
betaConv
nil
162
ref
401
ref
appTerm
403
def
axiom
nil
45
ref
403
remove
nil
cons
cons
46
ref
402
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
164
ref
165
ref
401
remove
nil
cons
cons
167
ref
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
404
def
subst
trans
appThm
nil
75
ref
338
ref
cons
nil
cons
nil
cons
cons
75
ref
30
ref
30
ref
251
remove
appTerm
78
ref
appTerm
appTerm
259
remove
appTerm
absTerm
405
def
78
remove
appTerm
406
def
betaConv
nil
162
ref
405
ref
appTerm
407
def
axiom
nil
45
ref
407
remove
nil
cons
cons
46
ref
406
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
164
ref
165
ref
405
remove
nil
cons
cons
167
remove
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
subst
385
ref
trans
trans
sym
81
ref
eqMp
eqMp
eqMp
nil
87
ref
391
remove
cons
408
def
389
remove
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
75
ref
281
ref
80
remove
appTerm
258
remove
appTerm
absTerm
409
def
48
remove
appTerm
410
def
betaConv
nil
162
ref
409
ref
appTerm
411
def
axiom
nil
45
ref
411
remove
nil
cons
cons
46
ref
410
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
164
ref
165
ref
409
remove
nil
cons
cons
334
remove
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
nil
408
remove
88
ref
368
remove
cons
"R"
1
ref
var
412
def
370
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
45
ref
47
ref
92
ref
appTerm
413
def
412
remove
varTerm
414
def
appTerm
415
def
nil
cons
cons
46
ref
414
ref
nil
cons
416
def
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
nil
45
ref
47
ref
90
ref
appTerm
417
def
414
ref
appTerm
nil
cons
cons
46
ref
47
ref
415
remove
appTerm
414
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
"r"
1
remove
var
418
def
47
ref
417
remove
418
ref
varTerm
419
def
appTerm
appTerm
420
def
47
ref
413
remove
419
ref
appTerm
appTerm
419
ref
appTerm
appTerm
absTerm
421
def
414
remove
appTerm
422
def
betaConv
30
ref
281
ref
90
ref
appTerm
423
def
92
ref
appTerm
424
def
appTerm
refl
46
ref
162
ref
418
ref
420
remove
47
ref
47
ref
50
remove
appTerm
419
ref
appTerm
appTerm
419
ref
appTerm
425
def
appTerm
absTerm
appTerm
absTerm
92
remove
appTerm
betaConv
appThm
71
remove
423
remove
appTerm
refl
45
ref
46
ref
162
ref
418
remove
47
remove
49
remove
419
remove
appTerm
appTerm
425
remove
appTerm
absTerm
appTerm
absTerm
absTerm
426
def
90
remove
appTerm
betaConv
appThm
nil
59
remove
281
remove
appTerm
426
remove
appTerm
axiom
99
remove
appThm
eqMp
95
remove
appThm
eqMp
424
remove
assume
eqMp
nil
45
ref
162
remove
421
ref
appTerm
nil
cons
cons
46
ref
422
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
164
remove
165
remove
421
remove
nil
cons
cons
166
remove
416
remove
cons
nil
cons
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
eqMp
eqMp
subst
proveHyp
proveHyp
proveHyp
subst
137
remove
nil
109
ref
317
ref
nil
cons
cons
nil
cons
nil
cons
cons
155
remove
89
remove
5
ref
298
remove
115
ref
constTerm
427
def
refl
nil
"t"
114
ref
var
117
remove
nil
cons
428
def
cons
nil
cons
nil
cons
cons
"A"
113
ref
nil
cons
cons
"B"
2
ref
cons
nil
cons
cons
154
remove
cons
"t"
0
ref
113
remove
"B"
varType
nil
cons
cons
opType
429
def
var
430
def
6
remove
0
ref
429
ref
0
ref
429
ref
2
ref
cons
opType
431
def
nil
cons
cons
opType
constTerm
432
def
430
ref
varTerm
433
def
appTerm
120
ref
433
ref
121
ref
appTerm
absTerm
434
def
appTerm
435
def
absTerm
436
def
433
ref
appTerm
437
def
betaConv
38
ref
0
remove
431
ref
2
remove
cons
opType
constTerm
438
def
refl
430
ref
435
remove
assume
sym
432
remove
434
remove
appTerm
433
ref
appTerm
439
def
assume
sym
deductAntisym
absThm
appThm
nil
438
ref
430
remove
439
remove
absTerm
appTerm
axiom
eqMp
nil
45
ref
438
remove
436
ref
appTerm
nil
cons
cons
46
ref
437
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
"A"
429
ref
nil
cons
cons
nil
cons
"P"
431
remove
var
436
remove
nil
cons
cons
"x"
429
remove
var
433
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
subst
subst
appThm
appThm
appThm
116
ref
120
ref
4
ref
122
remove
appTerm
absTerm
appTerm
refl
appThm
sym
nil
127
ref
428
remove
cons
nil
cons
nil
cons
cons
127
remove
30
remove
4
ref
427
remove
120
ref
128
ref
121
remove
appTerm
440
def
absTerm
appTerm
appTerm
appTerm
116
remove
120
remove
4
ref
440
remove
appTerm
absTerm
appTerm
appTerm
absTerm
441
def
128
ref
appTerm
442
def
betaConv
nil
38
remove
131
remove
constTerm
441
ref
appTerm
443
def
axiom
nil
45
ref
443
remove
nil
cons
cons
46
ref
442
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
ref
subst
proveHyp
"A"
156
remove
cons
nil
cons
"P"
115
remove
var
441
remove
nil
cons
cons
"x"
114
remove
var
128
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
134
ref
subst
eqMp
eqMp
subst
eqMp
subst
444
def
subst
152
ref
300
ref
5
ref
317
remove
301
ref
appTerm
betaConv
appThm
absThm
appThm
trans
appThm
nil
109
ref
320
ref
nil
cons
cons
nil
cons
nil
cons
cons
444
remove
subst
152
remove
300
ref
5
remove
320
remove
301
remove
appTerm
betaConv
appThm
absThm
appThm
trans
appThm
trans
336
remove
assume
eqMp
nil
87
ref
40
ref
365
ref
appTerm
nil
cons
445
def
cons
88
ref
40
remove
300
remove
4
ref
319
remove
appTerm
absTerm
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
101
ref
subst
proveHyp
nil
45
remove
445
remove
cons
46
remove
366
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
107
remove
subst
proveHyp
108
remove
109
remove
365
remove
nil
cons
cons
110
remove
364
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
134
remove
subst
eqMp
eqMp
eqMp
subst
eqMp
eqMp
nil
87
ref
343
remove
cons
88
remove
338
remove
cons
nil
cons
446
def
cons
nil
cons
cons
101
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
87
remove
337
remove
cons
446
remove
cons
nil
cons
cons
101
remove
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
eqMp
subst
deductAntisym
247
remove
eqMp
appThm
4
ref
11
ref
22
remove
appTerm
19
ref
appTerm
appTerm
447
def
refl
appThm
nil
75
remove
447
remove
nil
cons
cons
nil
cons
nil
cons
cons
404
remove
subst
trans
appThm
385
remove
trans
sym
81
remove
eqMp
eqMp
nil
4
remove
11
remove
25
remove
7
remove
constTerm
appTerm
448
def
19
remove
appTerm
appTerm
thm
24
remove
nil
448
remove
23
remove
appTerm
thm