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