Proofgold Proposition

∀ x0 x1 . ordinal x0 ⟶ nIn (SetAdjoin x1 (Sing 1)) x0

type
prop

theory
HotG

name
tagged_notin_ordinal

proof
PUUwp..

Megalodon
tagged_notin_ordinal

proofgold address
TMVoj..^{tagged_notin_ordinal}

creator
4910 Pr6Pc../8a687..

owner
4910 Pr6Pc../8a687..

term root
b603b..