Proofgold Term Root Disambiguation

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

as obj
-

as prop
1f6ca..^{add_OSNo_minus_OSNo_rinv}

theory
HotG

stx
5c6b2..

address
TMFhu..^{add_OSNo_minus_OSNo_rinv}