Proofgold Term Root Disambiguation

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

as obj
-

as prop
1a029..^{eps_ordsucc_half_add}

theory
HotG

stx
26642..

address
TMXMZ..^{eps_ordsucc_half_add}