Proofgold Proposition

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

type
prop

theory
HotG

name
add_SNo_ordinal_SL

proof
PUi5E..

Megalodon
add_SNo_ordinal_SL

proofgold address
TMcBJ..^{add_SNo_ordinal_SL}

creator
4962 Pr6Pc../e45f8..

owner
4962 Pr6Pc../e45f8..

term root
d55bd..