Proofgold Object

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

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

theory
HotG

name
CD_minus

definition
PUYQJ..

Megalodon
CD_minus

proofgold address
TMLCV..^CD_minus

creator
28412 PrQUS../b6b42..

owner
28412 PrQUS../b6b42..

term root
2d358..