Proofgold Proposition

∀ x0 x1 . ordinal x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ add_SNo (ordsucc x0) x2 = ordsucc (add_SNo x0 x2)) ⟶ SNo x0 ⟶ SNo x1 ⟶ ordinal (add_SNo x0 x1) ⟶ ordinal (ordsucc x0) ⟶ SNo (ordsucc x0) ⟶ add_SNo (ordsucc x0) x1 = ordsucc (add_SNo x0 x1)

type
prop

theory
HotG

name
-

proof
PURzn..

Megalodon
Conj_add_SNo_ordinal_SL__14__0

proofgold address
TMPuz..^{Conj_add_SNo_ordinal_SL__14__0}

creator
35045 PrNpY../5bd7d..

owner
35047 PrNpY../fc54b..

term root
99b3d..