Proofgold Term Root Disambiguation

∀ x0 x1 . iff (prim1 x1 (prim3 x0)) (∃ x2 . and (prim1 x1 x2) (prim1 x2 x0))

as obj
-

as prop
7a2c4..

theory
HoTg

stx
f69d8..

address
TMHRW..^UnionEq