Proofgold Term Root Disambiguation

∀ x0 . mul_nat x0 1 = x0

as obj
-

as prop
9b388..^mul_nat_1R

theory
HF

stx
b2d3f..

address
TMWym..^mul_nat_1R