Proofgold Proposition

∀ x0 x1 . Subq x1 (SNoElts_ x0) ⟶ (∀ x2 . In x2 x0 ⟶ exactly1of2 (In (SetAdjoin x2 (Sing 1)) x1) (In x2 x1)) ⟶ SNo_ x0 x1

type
prop

theory
HF

name
-

proof
PUQ8e..

Megalodon
SNo__I

proofgold address
TMXj9..^SNo__I

creator
2357 PrGxv../9c405..

owner
2357 PrGxv../9c405..

term root
4a803..