Proofgold Proposition

∀ x0 . nat_p x0 ⟶ x0 ∈ omega ⟶ add_SNo (eps_ (ordsucc x0)) (eps_ (ordsucc x0)) = eps_ x0

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_eps_ordsucc_half_add__11__1

proofgold address
TMahq..^{Conj_eps_ordsucc_half_add__11__1}

creator
35053 PrNpY../a583c..

owner
35061 PrNpY../2fd2d..

term root
c7520..