Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ add_SNo (minus_SNo x0) x0 = 0

as obj
-

as prop
44e25..^{add_SNo_minus_SNo_linv}

theory
HotG

stx
7edd8..

address
TMPWB..^{add_SNo_minus_SNo_linv}