Proofgold Object

λ x0 x1 x2 . unpack_e_o x0 (λ x3 x4 . unpack_e_o x1 (λ x5 x6 . and (x2 ∈ setexp x5 x3) (ap x2 x4 = x6)))

type
ι → ι → ι → ο

theory
HotG

name
PtdSetHom

definition
PUdXV..

Megalodon
Hom_struct_e

proofgold address
TMYd8..^Hom_struct_e

creator
9630 PrCx1../fa62a..

owner
9630 PrCx1../fa62a..

term root
d6f68..