Proofgold Term Root Disambiguation

λ x0 x1 . and (x1 ⊆ SNoElts_ x0) (∀ x2 . x2 ∈ x0 ⟶ exactly1of2 (SetAdjoin x2 (Sing 1) ∈ x1) (x2 ∈ x1))

as obj
c16a7..^SNo_

as prop
-

theory
HotG

stx
fab7c..

address
TMWTZ..^SNo_