Proofgold Object

λ x0 : ι → ι → ι . λ x1 : ι → (ι → ι → ι) → ι → ι → ι . In_rec_iii (λ x2 . λ x3 : ι → ι → ι → ι . If_iii (prim3 x2 ∈ x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0)

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

theory
HotG

name
nat_primrec_iii

definition
PUZC8..

Megalodon
-

proofgold address
TMT1L..

creator
6992 Pr6Pc../dde04..

owner
6992 Pr6Pc../dde04..

term root
c00ac..