Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ mul_nat x0 x1 = 0 ⟶ or (x0 = 0) (x1 = 0)

as obj
-

as prop
c3e8e..^{mul_nat_0_inv}

theory
HotG

stx
7fa67..

address
TMMVa..^{mul_nat_0_inv}