Proofgold Object

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

type
ι → ι → ο

theory
HotG

name
SNo_

definition
PUUwp..

Megalodon
SNo_

proofgold address
TMQpD..^SNo_

creator
4910 Pr6Pc../fa65e..

owner
4910 Pr6Pc../fa65e..

term root
4ab7e..