Proofgold Term Root Disambiguation

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

as obj
-

as prop
ca45c..^{Conj_eps_ordsucc_half_add__11__1}

theory
HotG

stx
b740c..

address
TMKPz..^{Conj_eps_ordsucc_half_add__11__1}