Proofgold Object

λ x0 . λ x1 x2 : ι → ο . ∀ x3 . x3 ∈ x0 ⟶ iff (x1 x3) (x2 x3)

type
ι → (ι → ο) → (ι → ο) → ο

theory
HotG

name
PNoEq_

definition
PUQ2Y..

Megalodon
PNoEq_

proofgold address
TMFre..^PNoEq_

creator
4903 Pr6Pc../7f74a..

owner
4903 Pr6Pc../7f74a..

term root
d7d95..