Proofgold Object

λ x0 x1 . unpack_p_i x0 (λ x2 . λ x3 : ι → ο . unpack_p_i x1 (λ x4 . λ x5 : ι → ο . pack_p (setprod x2 x4) (λ x6 . and (x3 (ap x6 0)) (x5 (ap x6 1)))))

type
ι → ι → ι

theory
HotG

name
-

definition
PUfqD..

Megalodon
-

proofgold address
TMVLP..

creator
11516 PrEBh../a77e7..

owner
11516 PrEBh../a77e7..

term root
ec3b3..