Proofgold Term Root Disambiguation

∀ x0 x1 . OSNo x0 ⟶ OSNo x1 ⟶ mul_OSNo (minus_OSNo x0) x1 = minus_OSNo (mul_OSNo x0 x1)

as obj
-

as prop
2ef89..^{minus_mul_OSNo_distrL}

theory
HotG

stx
5c6b2..

address
TMFVF..^{minus_mul_OSNo_distrL}