Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ mul_nat 1 x0 = x0

as obj
-

as prop
e6942..^mul_nat_1L

theory
HF

stx
b2d3f..

address
TMbip..^mul_nat_1L