6
version
"A"
"->"
typeOp
0
def
"A"
varType
1
def
"B"
varType
nil
cons
cons
opType
2
def
nil
cons
cons
nil
cons
nil
nil
cons
cons
nil
"="
const
3
def
0
ref
0
ref
0
ref
1
ref
"bool"
typeOp
nil
opType
4
def
nil
cons
5
def
cons
opType
6
def
5
ref
cons
opType
7
def
0
ref
7
ref
5
ref
cons
opType
nil
cons
cons
opType
constTerm
"Data.Bool.!"
const
8
def
7
ref
constTerm
appTerm
"p"
6
ref
var
9
def
3
ref
0
ref
6
remove
7
remove
nil
cons
cons
opType
constTerm
9
remove
varTerm
appTerm
"x"
1
ref
var
10
def
"Data.Bool.T"
const
4
ref
constTerm
11
def
absTerm
appTerm
absTerm
appTerm
axiom
subst
"p"
0
ref
2
ref
5
ref
cons
opType
12
def
var
13
def
3
ref
0
ref
12
ref
0
ref
12
ref
5
ref
cons
opType
14
def
nil
cons
cons
opType
constTerm
15
def
13
remove
varTerm
appTerm
refl
"x"
2
ref
var
nil
3
ref
0
ref
4
ref
0
ref
4
ref
5
ref
cons
opType
16
def
nil
cons
cons
opType
constTerm
11
remove
appTerm
3
ref
0
ref
16
ref
0
ref
16
remove
5
remove
cons
opType
nil
cons
cons
opType
constTerm
17
def
"p"
4
ref
var
18
def
18
remove
varTerm
absTerm
19
def
appTerm
19
remove
appTerm
appTerm
axiom
absThm
appThm
absThm
trans
"t"
2
ref
var
20
def
3
remove
0
remove
2
ref
12
ref
nil
cons
cons
opType
constTerm
21
def
10
ref
20
remove
varTerm
22
def
10
remove
varTerm
appTerm
absTerm
appTerm
22
remove
appTerm
absTerm
23
def
refl
appThm
sym
nil
"a"
12
remove
var
24
def
15
remove
24
remove
varTerm
appTerm
"b"
2
ref
var
17
remove
"c"
4
remove
var
25
def
25
remove
varTerm
absTerm
26
def
appTerm
26
remove
appTerm
absTerm
appTerm
absTerm
"d"
2
remove
var
27
def
21
remove
"e"
1
remove
var
28
def
27
remove
varTerm
29
def
28
remove
varTerm
appTerm
absTerm
appTerm
29
remove
appTerm
absTerm
appTerm
axiom
eqMp
nil
8
remove
14
remove
constTerm
23
remove
appTerm
thm