Proofgold Object

λ x0 x1 . λ x2 : ι → ι . nat_primrec (4ae4a.. 4a7ef..) (λ x3 x4 . If_i (prim1 x3 x0) (4ae4a.. 4a7ef..) (7ce1c.. (x2 x3) x4)) (4ae4a.. x1)

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

theory
HoTg

name
-

definition
PUXVB..

Megalodon
-

proofgold address
TMaG1..

creator
3938 PrGxv../770d9..

owner
3938 PrGxv../770d9..

term root
ea2cd..