Proofgold Term Root Disambiguation

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

as obj
8e35a..^exp_nat

as prop
-

theory
HotG

stx
3b6f0..

address
TMQba..^exp_nat