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