Proofgold Object

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

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

theory
HotG

name
CD_add

definition
PUYQJ..

Megalodon
CD_add

proofgold address
TMKFt..^CD_add

creator
28412 PrQUS../a4ef5..

owner
28412 PrQUS../a4ef5..

term root
7a5ff..