Proofgold Term Root Disambiguation

∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ mul_SNo x0 (minus_SNo x1) = minus_SNo (mul_SNo x0 x1)

as obj
-

as prop
2e747..^{mul_minus_SNo_distrR}

theory
HotG

stx
d6a2f..

address
TMdKU..^{mul_minus_SNo_distrR}