Proofgold Term Root Disambiguation

λ x0 . nat_primrec x0 (λ x1 . ordsucc)

as obj
29768..^add_nat

as prop
-

theory
HotG

stx
d0fc7..

address
TMQX4..^add_nat