Proofgold Proposition

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

type
prop

theory
HF

name
-

proof
PUQ8e..

Megalodon
tagged_ReplE

proofgold address
TMLNK..^tagged_ReplE

creator
2357 PrGxv../daac7..

owner
2357 PrGxv../daac7..

term root
87200..