Proofgold Proposition

∀ x0 . ordinal x0 ⟶ ∀ x1 . ordinal x1 ⟶ add_SNo x0 (ordsucc x1) = ordsucc (add_SNo x0 x1)

type
prop

theory
HotG

name
add_SNo_ordinal_SR

proof
PUi5E..

Megalodon
add_SNo_ordinal_SR

proofgold address
TMLPo..^{add_SNo_ordinal_SR}

creator
4962 Pr6Pc../b622b..

owner
4962 Pr6Pc../b622b..

term root
e7378..