Proofgold Term Root Disambiguation

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

as obj
-

as prop
bc1cf..

theory
HotG

stx
f6ee3..

address
TMHxu..