Search for blocks/addresses/...
Proofgold Term Root Disambiguation
∀ x0 :
ι → ι
.
∀ x1 x2 .
nat_p
x1
⟶
nat_p
x2
⟶
(
∀ x3 .
x3
∈
u20
⟶
x0
x3
∈
u12
)
⟶
(
∀ x3 .
x3
∈
u12
⟶
or
(
equip
{x4 ∈
u20
|
x0
x4
=
x3
}
u1
)
(
equip
{x4 ∈
u20
|
x0
x4
=
x3
}
u2
)
)
⟶
equip
{x3 ∈
u12
|
equip
{x4 ∈
u20
|
x0
x4
=
x3
}
u1
}
x1
⟶
equip
{x3 ∈
u12
|
equip
{x4 ∈
u20
|
x0
x4
=
x3
}
u2
}
x2
⟶
and
(
x1
=
u4
)
(
x2
=
u8
)
as obj
-
as prop
eeb21..
theory
HotG
stx
62a5c..
address
TMNXo..