6
version
nil
"P"
"->"
typeOp
0
def
"Data.Option.option"
typeOp
"A"
varType
1
def
nil
cons
2
def
opType
3
def
"bool"
typeOp
nil
opType
4
def
nil
cons
5
def
cons
opType
6
def
var
7
def
"x"
3
ref
var
8
def
"="
const
9
def
0
ref
3
ref
6
ref
nil
cons
cons
opType
constTerm
10
def
"Data.Option.case.none.some"
const
11
def
0
ref
3
ref
0
ref
0
ref
1
ref
3
ref
nil
cons
12
def
cons
opType
13
def
0
ref
3
ref
12
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
"Data.Option.none"
const
3
ref
constTerm
14
def
appTerm
"Data.Option.some"
const
13
ref
constTerm
15
def
appTerm
16
def
8
ref
varTerm
17
def
appTerm
appTerm
17
ref
appTerm
18
def
absTerm
19
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
12
ref
cons
nil
cons
20
def
nil
nil
cons
21
def
cons
22
def
9
ref
0
ref
4
ref
0
ref
4
ref
5
ref
cons
opType
23
def
nil
cons
cons
opType
24
def
constTerm
25
def
"Data.Bool.!"
const
26
def
0
ref
0
ref
1
ref
5
ref
cons
opType
27
def
5
ref
cons
opType
28
def
constTerm
29
def
"P"
27
ref
var
30
def
varTerm
31
def
appTerm
32
def
appTerm
refl
"p"
27
ref
var
33
def
9
ref
0
ref
27
ref
28
ref
nil
cons
cons
opType
constTerm
33
ref
varTerm
34
def
appTerm
"x"
1
ref
var
35
def
"Data.Bool.T"
const
4
ref
constTerm
36
def
absTerm
37
def
appTerm
absTerm
38
def
31
ref
appTerm
betaConv
39
def
appThm
nil
9
ref
0
ref
28
ref
0
ref
28
ref
5
ref
cons
opType
nil
cons
cons
opType
constTerm
40
def
29
ref
appTerm
38
remove
appTerm
axiom
31
ref
refl
41
def
appThm
42
def
eqMp
sym
43
def
subst
subst
8
ref
nil
"t"
4
ref
var
44
def
18
ref
nil
cons
45
def
cons
nil
cons
nil
cons
cons
25
ref
44
ref
varTerm
46
def
appTerm
36
ref
appTerm
assume
sym
nil
36
ref
axiom
47
def
eqMp
46
remove
assume
47
ref
deductAntisym
deductAntisym
48
def
subst
8
ref
"Data.Bool.\\/"
const
24
ref
constTerm
49
def
10
ref
17
ref
appTerm
50
def
14
ref
appTerm
51
def
appTerm
"Data.Bool.?"
const
28
remove
constTerm
52
def
"a"
1
ref
var
53
def
50
remove
15
ref
53
ref
varTerm
54
def
appTerm
55
def
appTerm
56
def
absTerm
57
def
appTerm
58
def
appTerm
59
def
absTerm
60
def
17
ref
appTerm
61
def
betaConv
nil
26
ref
0
ref
6
remove
5
ref
cons
opType
constTerm
62
def
60
ref
appTerm
63
def
axiom
nil
"p"
4
ref
var
64
def
63
remove
nil
cons
cons
"q"
4
ref
var
65
def
61
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
25
ref
"Data.Bool.==>"
const
24
ref
constTerm
66
def
64
ref
varTerm
67
def
appTerm
68
def
65
ref
varTerm
69
def
appTerm
70
def
appTerm
refl
64
ref
65
ref
25
ref
"Data.Bool./\\"
const
24
ref
constTerm
71
def
67
ref
appTerm
72
def
69
ref
appTerm
73
def
appTerm
74
def
67
ref
appTerm
absTerm
75
def
absTerm
76
def
67
ref
appTerm
betaConv
69
ref
refl
77
def
appThm
75
remove
69
ref
appTerm
betaConv
trans
appThm
nil
9
ref
0
ref
24
ref
0
ref
24
ref
5
ref
cons
opType
78
def
nil
cons
cons
opType
constTerm
79
def
66
ref
appTerm
76
remove
appTerm
axiom
67
ref
refl
80
def
appThm
77
ref
appThm
eqMp
81
def
sym
82
def
74
remove
refl
65
ref
9
ref
0
ref
78
ref
0
ref
78
remove
5
ref
cons
opType
nil
cons
cons
opType
constTerm
83
def
"f"
24
remove
var
84
def
84
ref
varTerm
85
def
67
ref
appTerm
69
ref
appTerm
absTerm
86
def
appTerm
84
ref
85
ref
36
ref
appTerm
36
ref
appTerm
absTerm
87
def
appTerm
absTerm
88
def
69
ref
appTerm
betaConv
appThm
9
ref
0
ref
23
ref
0
ref
23
ref
5
ref
cons
opType
89
def
nil
cons
cons
opType
constTerm
90
def
72
remove
appTerm
refl
64
ref
88
remove
absTerm
91
def
67
ref
appTerm
betaConv
appThm
nil
79
ref
71
ref
appTerm
91
ref
appTerm
axiom
92
def
80
remove
appThm
eqMp
77
ref
appThm
eqMp
93
def
sym
84
ref
85
ref
refl
nil
44
ref
67
ref
nil
cons
94
def
cons
nil
cons
nil
cons
cons
48
ref
subst
67
ref
assume
95
def
eqMp
appThm
nil
44
ref
69
ref
nil
cons
96
def
cons
nil
cons
nil
cons
cons
48
ref
subst
69
ref
assume
eqMp
appThm
absThm
eqMp
97
def
nil
"P"
4
ref
var
98
def
94
remove
cons
"Q"
4
ref
var
99
def
96
remove
cons
nil
cons
cons
nil
cons
cons
25
ref
refl
100
def
84
ref
85
remove
98
ref
varTerm
101
def
appTerm
102
def
99
ref
varTerm
103
def
appTerm
absTerm
64
ref
65
ref
67
ref
absTerm
absTerm
104
def
appTerm
betaConv
104
ref
101
ref
appTerm
betaConv
103
ref
refl
105
def
appThm
65
ref
101
ref
absTerm
103
ref
appTerm
betaConv
trans
trans
appThm
87
ref
104
ref
appTerm
betaConv
104
ref
36
ref
appTerm
betaConv
36
ref
refl
106
def
appThm
65
ref
36
ref
absTerm
36
ref
appTerm
betaConv
trans
trans
appThm
25
ref
71
remove
101
ref
appTerm
107
def
103
ref
appTerm
108
def
appTerm
refl
65
ref
83
remove
84
remove
102
remove
69
ref
appTerm
absTerm
appTerm
87
ref
appTerm
absTerm
103
ref
appTerm
betaConv
appThm
90
ref
107
remove
appTerm
refl
91
remove
101
ref
appTerm
betaConv
appThm
92
remove
101
ref
refl
109
def
appThm
eqMp
105
ref
appThm
eqMp
108
remove
assume
eqMp
104
remove
refl
appThm
eqMp
sym
47
ref
eqMp
110
def
subst
111
def
deductAntisym
eqMp
81
remove
70
ref
assume
eqMp
sym
95
ref
eqMp
100
remove
86
remove
64
ref
65
ref
69
ref
absTerm
112
def
absTerm
113
def
appTerm
betaConv
113
ref
67
ref
appTerm
betaConv
77
remove
appThm
112
ref
69
ref
appTerm
betaConv
trans
trans
appThm
87
remove
113
ref
appTerm
betaConv
113
ref
36
ref
appTerm
betaConv
106
remove
appThm
112
remove
36
remove
appTerm
betaConv
trans
trans
appThm
93
remove
73
remove
assume
eqMp
113
remove
refl
appThm
eqMp
sym
47
ref
eqMp
114
def
proveHyp
deductAntisym
115
def
subst
proveHyp
20
remove
7
remove
60
remove
nil
cons
cons
8
ref
17
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
64
ref
32
ref
nil
cons
116
def
cons
65
ref
31
ref
35
ref
varTerm
117
def
appTerm
118
def
nil
cons
119
def
cons
nil
cons
cons
nil
cons
cons
120
def
82
ref
subst
120
remove
114
remove
97
remove
deductAntisym
121
def
subst
25
ref
118
ref
appTerm
refl
37
remove
117
ref
appTerm
betaConv
appThm
39
remove
42
remove
32
remove
assume
eqMp
eqMp
117
ref
refl
122
def
appThm
eqMp
sym
47
ref
eqMp
eqMp
nil
98
ref
116
remove
cons
99
ref
119
remove
cons
nil
cons
cons
nil
cons
cons
110
ref
subst
deductAntisym
eqMp
123
def
subst
eqMp
eqMp
nil
64
ref
59
remove
nil
cons
124
def
cons
65
ref
45
ref
cons
nil
cons
125
def
cons
nil
cons
cons
126
def
115
ref
subst
proveHyp
126
ref
82
ref
subst
126
remove
121
ref
subst
nil
30
ref
53
ref
66
ref
57
ref
54
ref
appTerm
127
def
appTerm
18
ref
appTerm
128
def
absTerm
nil
cons
cons
nil
cons
nil
cons
cons
43
remove
subst
53
ref
nil
44
ref
128
remove
nil
cons
cons
nil
cons
nil
cons
cons
48
ref
subst
nil
64
ref
127
ref
nil
cons
129
def
cons
125
ref
cons
nil
cons
cons
130
def
82
ref
subst
130
remove
121
ref
subst
127
ref
betaConv
127
remove
assume
eqMp
nil
64
ref
56
ref
nil
cons
131
def
cons
125
ref
cons
nil
cons
cons
132
def
115
ref
subst
proveHyp
132
ref
82
ref
subst
132
remove
121
ref
subst
10
remove
refl
133
def
16
remove
refl
134
def
56
remove
assume
135
def
appThm
nil
"f"
13
remove
var
15
remove
nil
cons
cons
"b"
3
ref
var
14
ref
nil
cons
136
def
cons
nil
cons
cons
nil
cons
cons
137
def
"A"
2
remove
cons
138
def
"B"
12
remove
cons
nil
cons
cons
21
remove
cons
139
def
53
remove
9
ref
0
ref
"B"
varType
140
def
0
ref
140
ref
5
ref
cons
opType
141
def
nil
cons
cons
opType
constTerm
142
def
11
remove
0
ref
140
ref
0
ref
0
ref
1
ref
140
ref
nil
cons
143
def
cons
opType
144
def
0
ref
3
remove
143
ref
cons
opType
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
"b"
140
ref
var
145
def
varTerm
146
def
appTerm
"f"
144
ref
var
147
def
varTerm
148
def
appTerm
149
def
55
ref
appTerm
appTerm
148
ref
54
ref
appTerm
appTerm
absTerm
150
def
54
ref
appTerm
151
def
betaConv
147
ref
29
ref
150
ref
appTerm
152
def
absTerm
153
def
148
ref
appTerm
154
def
betaConv
145
ref
26
ref
0
ref
0
ref
144
ref
5
ref
cons
opType
155
def
5
ref
cons
opType
constTerm
156
def
153
ref
appTerm
157
def
absTerm
158
def
146
ref
appTerm
159
def
betaConv
nil
26
ref
0
ref
141
ref
5
ref
cons
opType
constTerm
160
def
158
ref
appTerm
161
def
axiom
nil
64
ref
161
remove
nil
cons
cons
65
ref
159
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
115
ref
subst
proveHyp
"A"
143
remove
cons
nil
cons
162
def
"P"
141
remove
var
163
def
158
remove
nil
cons
cons
"x"
140
remove
var
146
ref
nil
cons
cons
nil
cons
164
def
cons
nil
cons
cons
123
ref
subst
eqMp
eqMp
nil
64
ref
157
remove
nil
cons
cons
65
ref
154
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
115
ref
subst
proveHyp
"A"
144
ref
nil
cons
cons
nil
cons
165
def
"P"
155
remove
var
166
def
153
remove
nil
cons
cons
"x"
144
remove
var
148
ref
nil
cons
cons
nil
cons
167
def
cons
nil
cons
cons
123
ref
subst
eqMp
eqMp
nil
64
ref
152
remove
nil
cons
cons
65
ref
151
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
115
ref
subst
proveHyp
138
remove
nil
cons
168
def
30
ref
150
remove
nil
cons
cons
35
ref
54
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
123
ref
subst
eqMp
eqMp
subst
subst
trans
appThm
135
remove
appThm
nil
8
ref
55
remove
nil
cons
cons
nil
cons
nil
cons
cons
22
remove
nil
44
remove
9
remove
0
remove
1
remove
27
remove
nil
cons
cons
opType
constTerm
117
ref
appTerm
117
ref
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
48
remove
subst
122
remove
eqMp
subst
169
def
subst
trans
sym
47
ref
eqMp
eqMp
nil
98
ref
131
remove
cons
99
ref
45
ref
cons
nil
cons
170
def
cons
nil
cons
cons
110
ref
subst
deductAntisym
eqMp
eqMp
eqMp
nil
98
ref
129
remove
cons
170
ref
cons
nil
cons
cons
110
ref
subst
deductAntisym
eqMp
eqMp
absThm
eqMp
nil
64
ref
29
ref
35
ref
66
ref
57
ref
117
ref
appTerm
appTerm
18
ref
appTerm
absTerm
appTerm
nil
cons
cons
65
ref
66
ref
58
ref
appTerm
18
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
115
ref
subst
proveHyp
168
remove
30
remove
57
remove
nil
cons
cons
170
ref
cons
nil
cons
cons
nil
64
ref
29
ref
35
ref
66
ref
118
remove
appTerm
171
def
103
ref
appTerm
absTerm
appTerm
nil
cons
172
def
cons
173
def
65
ref
66
ref
52
ref
31
ref
appTerm
174
def
appTerm
175
def
103
ref
appTerm
nil
cons
176
def
cons
nil
cons
cons
nil
cons
cons
177
def
82
ref
subst
177
remove
121
ref
subst
nil
64
ref
174
ref
nil
cons
178
def
cons
179
def
65
ref
103
ref
nil
cons
180
def
cons
nil
cons
181
def
cons
nil
cons
cons
182
def
82
ref
subst
182
remove
121
ref
subst
nil
173
remove
181
remove
cons
nil
cons
cons
115
ref
subst
65
ref
66
ref
29
ref
35
ref
171
remove
69
ref
appTerm
absTerm
appTerm
appTerm
69
ref
appTerm
absTerm
183
def
103
ref
appTerm
184
def
betaConv
nil
179
remove
65
ref
26
remove
89
remove
constTerm
185
def
183
ref
appTerm
186
def
nil
cons
187
def
cons
nil
cons
cons
nil
cons
cons
188
def
115
ref
subst
25
ref
174
remove
appTerm
189
def
refl
33
remove
185
ref
65
ref
66
ref
29
remove
35
remove
66
ref
34
remove
117
remove
appTerm
appTerm
69
ref
appTerm
absTerm
appTerm
appTerm
69
ref
appTerm
absTerm
appTerm
absTerm
190
def
31
remove
appTerm
betaConv
appThm
nil
40
remove
52
remove
appTerm
190
remove
appTerm
axiom
41
remove
appThm
eqMp
nil
64
ref
189
remove
186
ref
appTerm
nil
cons
cons
65
ref
175
remove
186
remove
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
115
ref
subst
proveHyp
188
remove
nil
64
ref
25
ref
67
remove
appTerm
69
ref
appTerm
191
def
nil
cons
192
def
cons
65
ref
70
remove
nil
cons
193
def
cons
nil
cons
cons
nil
cons
cons
194
def
82
ref
subst
194
remove
121
ref
subst
82
ref
121
ref
191
remove
assume
95
remove
eqMp
eqMp
111
remove
deductAntisym
eqMp
eqMp
nil
98
ref
192
remove
cons
99
ref
193
remove
cons
nil
cons
cons
nil
cons
cons
110
ref
subst
deductAntisym
eqMp
subst
eqMp
eqMp
nil
64
ref
187
remove
cons
65
ref
184
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
115
ref
subst
proveHyp
"A"
5
remove
cons
nil
cons
195
def
"P"
23
remove
var
196
def
183
remove
nil
cons
cons
"x"
4
ref
var
197
def
180
ref
cons
nil
cons
cons
nil
cons
cons
123
ref
subst
eqMp
eqMp
eqMp
eqMp
nil
98
ref
178
remove
cons
99
ref
180
remove
cons
nil
cons
cons
nil
cons
cons
110
ref
subst
deductAntisym
eqMp
eqMp
nil
98
ref
172
remove
cons
99
ref
176
remove
cons
nil
cons
cons
nil
cons
cons
110
ref
subst
deductAntisym
eqMp
subst
eqMp
nil
64
ref
51
ref
nil
cons
198
def
cons
125
remove
cons
nil
cons
cons
199
def
82
remove
subst
199
remove
121
remove
subst
133
remove
134
remove
51
remove
assume
200
def
appThm
137
remove
139
remove
147
remove
142
remove
149
remove
14
remove
appTerm
appTerm
146
ref
appTerm
absTerm
201
def
148
remove
appTerm
202
def
betaConv
145
remove
156
remove
201
ref
appTerm
203
def
absTerm
204
def
146
remove
appTerm
205
def
betaConv
nil
160
remove
204
ref
appTerm
206
def
axiom
nil
64
ref
206
remove
nil
cons
cons
65
ref
205
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
115
ref
subst
proveHyp
162
remove
163
remove
204
remove
nil
cons
cons
164
remove
cons
nil
cons
cons
123
ref
subst
eqMp
eqMp
nil
64
ref
203
remove
nil
cons
cons
65
ref
202
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
115
ref
subst
proveHyp
165
remove
166
remove
201
remove
nil
cons
cons
167
remove
cons
nil
cons
cons
123
ref
subst
eqMp
eqMp
subst
subst
trans
appThm
200
remove
appThm
nil
8
remove
136
remove
cons
nil
cons
nil
cons
cons
169
remove
subst
trans
sym
47
remove
eqMp
eqMp
nil
98
ref
198
remove
cons
207
def
170
ref
cons
nil
cons
cons
110
ref
subst
deductAntisym
eqMp
nil
207
remove
99
remove
58
remove
nil
cons
cons
"R"
4
ref
var
208
def
45
remove
cons
nil
cons
cons
cons
nil
cons
cons
nil
64
ref
66
ref
103
ref
appTerm
209
def
208
remove
varTerm
210
def
appTerm
211
def
nil
cons
cons
65
ref
210
ref
nil
cons
212
def
cons
nil
cons
cons
nil
cons
cons
115
ref
subst
nil
64
ref
66
ref
101
ref
appTerm
213
def
210
ref
appTerm
nil
cons
cons
65
ref
66
ref
211
remove
appTerm
210
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
115
ref
subst
"r"
4
remove
var
214
def
66
ref
213
remove
214
ref
varTerm
215
def
appTerm
appTerm
216
def
66
ref
209
remove
215
ref
appTerm
appTerm
215
ref
appTerm
appTerm
absTerm
217
def
210
remove
appTerm
218
def
betaConv
25
remove
49
ref
101
ref
appTerm
219
def
103
ref
appTerm
220
def
appTerm
refl
65
ref
185
ref
214
ref
216
remove
66
ref
66
ref
69
remove
appTerm
215
ref
appTerm
appTerm
215
ref
appTerm
221
def
appTerm
absTerm
appTerm
absTerm
103
remove
appTerm
betaConv
appThm
90
remove
219
remove
appTerm
refl
64
ref
65
ref
185
ref
214
remove
66
remove
68
remove
215
remove
appTerm
appTerm
221
remove
appTerm
absTerm
appTerm
absTerm
absTerm
222
def
101
remove
appTerm
betaConv
appThm
nil
79
remove
49
remove
appTerm
222
remove
appTerm
axiom
109
remove
appThm
eqMp
105
remove
appThm
eqMp
220
remove
assume
eqMp
nil
64
remove
185
remove
217
ref
appTerm
nil
cons
cons
65
remove
218
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
115
remove
subst
proveHyp
195
remove
196
remove
217
remove
nil
cons
cons
197
remove
212
remove
cons
nil
cons
cons
nil
cons
cons
123
remove
subst
eqMp
eqMp
eqMp
eqMp
subst
proveHyp
proveHyp
eqMp
nil
98
remove
124
remove
cons
170
remove
cons
nil
cons
cons
110
remove
subst
deductAntisym
eqMp
eqMp
eqMp
absThm
eqMp
nil
62
remove
19
remove
appTerm
thm