Proofgold Term Root Disambiguation

∀ x0 x1 . nat_p x0 ⟶ nat_p x1 ⟶ ∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x1 ⟶ In (add_nat x2 (mul_nat x3 x0)) (mul_nat x0 x1)

as obj
-

as prop
5fcca..^{add_mul_nat_lt}

theory
HF

stx
b2d3f..

address
TMUPv..^{add_mul_nat_lt}