Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ 0 ∈ x0 ⟶ 1 ∈ x1 ⟶ x0 ∈ mul_nat x0 x1

as obj
-

as prop
5d96a..^{mul_nat_0m_1n_In}

theory
HotG

stx
afc5a..

address
TMJ3U..^{mul_nat_0m_1n_In}