Proofgold Proposition

∀ x0 x1 . ordinal x0 ⟶ In x0 (Repl x1 (λ x2 . SetAdjoin x2 (Sing 1))) ⟶ False

type
prop

theory
HF

name
-

proof
PUQ8e..

Megalodon
ordinal_notin_tagged_Repl

proofgold address
TMLxx..^{ordinal_notin_tagged_Repl}

creator
2357 PrGxv../13bf9..

owner
2357 PrGxv../13bf9..

term root
bfcb0..