Proofgold Proposition

∀ x0 x1 . ordinal x0 ⟶ In x1 x0 ⟶ or (In (ordsucc x1) x0) (x0 = ordsucc x1)

type
prop

theory
HF

name
-

proof
PUZ6J..

Megalodon
ordinal_ordsucc_In_eq

proofgold address
TMSZM..^{ordinal_ordsucc_In_eq}

creator
1604 PrGxv../9ec17..

owner
1604 PrGxv../9ec17..

term root
25398..