Proofgold Object

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

type
ι → ι → ι

theory
HotG

name
BinReln_product

definition
PUKcr..

Megalodon
-

proofgold address
TMaWR..

creator
11519 PrEBh../da3c1..

owner
11519 PrEBh../da3c1..

term root
d344d..