Proofgold Object

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

type
(ι → ι) → ι → ι

theory
HotG

name
Pi_nat

definition
PUPh4..

Megalodon
Pi_nat

proofgold address
TMdui..^Pi_nat

creator
29757 PrQUS../cac71..

owner
29757 PrQUS../cac71..

term root
a0b86..