Proofgold Term Root Disambiguation

λ x0 . {x1 ∈ prim4 (SNoElts_ x0)|∃ x2 . and (x2 ∈ x0) (SNo_ x2 x1)}

as obj
4680c..^SNoS_

as prop
-

theory
HotG

stx
fab7c..

address
TMYei..^SNoS_