Proofgold Object

λ x0 : ι → (ι → ι) → ι . λ x1 . In_rec_ii (λ x2 . λ x3 : ι → ι → ι . If_ii (ordinal x2) (λ x4 . If_i (prim1 x4 (56ded.. (4ae4a.. x2))) (x0 x4 (λ x5 . x3 (e4431.. x5) x5)) (prim0 (λ x5 . True))) (λ x4 . prim0 (λ x5 . True))) (e4431.. x1) x1

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

theory
HoTg

name
-

definition
PUTG4..

Megalodon
-

proofgold address
TMFyR..

creator
3831 PrGxv../23a85..

owner
3831 PrGxv../23a85..

term root
9f8e2..