Proofgold Object

λ x0 . and (struct_p x0) (unpack_p_o x0 (λ x1 . λ x2 : ι → ο . ∀ x3 : ο . (∀ x4 . and (x4 ∈ x1) (x2 x4) ⟶ x3) ⟶ x3))

type
ι → ο

theory
HotG

name
PtdPred

definition
PUhdQ..

Megalodon
struct_p_nonempty

proofgold address
TMP3V..^{struct_p_nonempty}

creator
9725 PrCx1../fcd25..

owner
9725 PrCx1../fcd25..

term root
8ef0c..