Search for blocks/addresses/...
Proofgold Term Root Disambiguation
∀ x0 .
nat_p
x0
⟶
1
∈
x0
⟶
∀ x1 .
(
x0
=
x1
⟶
∀ x2 : ο .
x2
)
⟶
∀ x2 x3 x4 .
SNo
x3
⟶
x4
∈
x3
⟶
SetAdjoin
x2
(
Sing
x0
)
=
SetAdjoin
x4
(
Sing
x1
)
⟶
∀ x5 : ο .
x5
as obj
-
as prop
f4add..
theory
HotG
stx
2a9bf..
address
TMJWQ..