Proofgold Object

λ x0 x1 x2 . unpack_p_o x0 (λ x3 . λ x4 : ι → ο . unpack_p_o x1 (λ x5 . λ x6 : ι → ο . and (x2 ∈ setexp x5 x3) (∀ x7 . x7 ∈ x3 ⟶ x4 x7 ⟶ x6 (ap x2 x7))))

type
ι → ι → ι → ο

theory
HotG

name
UnaryPredHom

definition
PUdXV..

Megalodon
Hom_struct_p

proofgold address
TML5c..^Hom_struct_p

creator
9630 PrCx1../08622..

owner
9630 PrCx1../08622..

term root
5d020..