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