Proofgold Object

λ x0 . and (struct_u x0) (unpack_u_o x0 (λ x1 . λ x2 : ι → ι . ∀ x3 . x3 ∈ x1 ⟶ x2 (x2 x3) = x2 x3))

type
ι → ο

theory
HotG

name
-

definition
PURhD..

Megalodon
struct_u_idem

proofgold address
TMWUq..^{struct_u_idem}

creator
9725 PrCx1../f78d9..

owner
9725 PrCx1../f78d9..

term root
a6656..