Proofgold Object

λ x0 : ι → ι . λ x1 : ι → (ι → ι) → ι → ι . In_rec_ii (λ x2 . λ x3 : ι → ι → ι . If_ii (prim3 x2 ∈ x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0)

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

theory
HotG

name
nat_primrec_ii

definition
PUZC8..

Megalodon
-

proofgold address
TMPK9..

creator
6992 Pr6Pc../a1d3e..

owner
6992 Pr6Pc../a1d3e..

term root
d1414..