Proofgold Proposition

∀ x0 . ordinal x0 ⟶ ordsucc x0 = add_SNo 1 x0

type
prop

theory
HotG

name
ordinal_ordsucc_SNo_eq

proof
PUVtn..

Megalodon
ordinal_ordsucc_SNo_eq

proofgold address
TMM3U..^{ordinal_ordsucc_SNo_eq}

creator
5161 Pr6Pc../6d0c8..

owner
5161 Pr6Pc../6d0c8..

term root
f0596..