Proofgold Object

λ x0 x1 . ∃ x2 . and (and (∀ x4 . x4 ∈ x0 ⟶ ∃ x5 . and (x5 ∈ x1) (KPair_alt7 x4 x5 ∈ x2)) (∀ x4 . x4 ∈ x1 ⟶ ∃ x5 . and (x5 ∈ x0) (KPair_alt7 x5 x4 ∈ x2))) (∀ x4 x5 x6 x7 . KPair_alt7 x4 x5 ∈ x2 ⟶ KPair_alt7 x6 x7 ∈ x2 ⟶ iff (x4 = x6) (x5 = x7))

type
ι → ι → ο

theory
HotG

name
-

definition
PUYSq..

Megalodon
-

proofgold address
TMGvi..

creator
4892 Pr6Pc../01cfd..

owner
4892 Pr6Pc../01cfd..

term root
83e7e..