Proofgold Proposition

∀ x0 . ordinal x0 ⟶ (∀ x1 . nat_p x1 ⟶ add_nat x0 x1 = add_SNo x0 x1) ⟶ ∀ x1 . x1 ∈ omega ⟶ add_nat x0 x1 = add_SNo x0 x1

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_add_nat_add_SNo__1__1

proofgold address
TMUWX..^{Conj_add_nat_add_SNo__1__1}

creator
35053 PrNpY../69085..

owner
35061 PrNpY../c9fca..

term root
d6ce0..