Proofgold Term Root Disambiguation

∀ x0 x1 . iff (x1 ∈ prim4 x0) (x1 ⊆ x0)

as obj
-

as prop
d67d7..^PowerEq

theory
HotG

stx
cde1e..

address
TMTza..^PowerEq