Search for blocks/addresses/...
Proofgold Term Root Disambiguation
Sigma_nat
6
(
λ x1 .
mul_nat
(
ap
(
lam
6
(
λ x2 .
If_i
(
x2
=
0
)
1
(
If_i
(
x2
=
1
)
0
(
If_i
(
x2
=
2
)
0
(
If_i
(
x2
=
3
)
1
(
If_i
(
x2
=
4
)
0
1
)
)
)
)
)
)
x1
)
(
exp_nat
2
x1
)
)
=
41
as obj
-
as prop
0c734..
theory
HotG
stx
b3050..
address
TMHHJ..