Proofgold Object

λ x0 . λ x1 : ι → ο . λ x2 x3 : ι → ι . λ x4 x5 : ι → ι → ι . λ x6 x7 . pair_tag x0 (x4 (x5 (CD_proj0 x0 x1 x6) (CD_proj0 x0 x1 x7)) (x2 (x5 (x3 (CD_proj1 x0 x1 x7)) (CD_proj1 x0 x1 x6)))) (x4 (x5 (CD_proj1 x0 x1 x7) (CD_proj0 x0 x1 x6)) (x5 (CD_proj1 x0 x1 x6) (x3 (CD_proj0 x0 x1 x7))))

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

theory
HotG

name
CD_mul

definition
PUYQJ..

Megalodon
CD_mul

proofgold address
TMJk2..^CD_mul

creator
28412 PrQUS../e9d31..

owner
28412 PrQUS../e9d31..

term root
f53b0..