Proofgold Term Root Disambiguation

∀ x0 . mul_nat x0 1 = x0

as obj
-

as prop
a3051..^mul_nat_1R

theory
HotG

stx
71eda..

address
TMRHC..^mul_nat_1R