Proofgold Object

λ x0 . λ x1 : ι → ι → ι . In_rec_i (λ x2 . λ x3 : ι → ι . If_i (prim3 x2 ∈ x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0)

type
ι → (ι → ι → ι) → ι → ι

theory
HotG

name
nat_primrec

definition
PUfQZ..

Megalodon
nat_primrec

proofgold address
TMLxf..^nat_primrec

creator
4898 Pr6Pc../78a7c..

owner
4898 Pr6Pc../78a7c..

term root
3be1c..