Proofgold Term Root Disambiguation

λ x0 . nat_primrec 1 (λ x1 . mul_nat x0)

as obj
69aae..^exp_nat

as prop
-

theory
HF

stx
d1259..

address
TMQ1r..^exp_nat