Proofgold Term Root Disambiguation

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

as obj
70d0e..^Pi_nat

as prop
-

theory
HotG

stx
00571..

address
TMVbW..^Pi_nat