Proofgold Term Root Disambiguation

∀ x0 . OSNo x0 ⟶ add_OSNo (minus_OSNo x0) x0 = 0

as obj
-

as prop
8767d..^{add_OSNo_minus_OSNo_linv}

theory
HotG

stx
5c6b2..

address
TMPdN..^{add_OSNo_minus_OSNo_linv}