Proofgold Object

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

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

theory
HoTg

name
nat_primrec

definition
PUKrN..

Megalodon
-

proofgold address
TMKwo..

creator
2749 PrGxv../67234..

owner
2749 PrGxv../67234..

term root
3be1c..