Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ mul_nat x0 x1 = 0 ⟶ or (x0 = 0) (x1 = 0)

as obj
-

as prop
f3fbb..^{mul_nat_0_inv}

theory
HotG

stx
71eda..

address
TMLxg..^{mul_nat_0_inv}