Proofgold Term Root Disambiguation

∀ x0 x1 . nat_p x1 ⟶ 69aae.. x0 (ordsucc x1) = mul_nat x0 (69aae.. x0 x1)

as obj
-

as prop
f4890..^exp_nat_S

theory
HF

stx
e311e..

address
TMVPr..^exp_nat_S