Proofgold Term Root Disambiguation

λ x0 : ι → ι . nat_primrec 1 (λ x1 x2 . mul_SNo x2 (x0 x1))

as obj
05ecb..^Pi_SNo

as prop
-

theory
HotG

stx
afc5a..

address
TMRqa..^Pi_SNo