Proofgold Object

λ x0 x1 . ∃ x2 . and (and (∀ x4 . prim1 x4 x0 ⟶ ∃ x5 . and (prim1 x5 x1) (prim1 (7ee77.. x4 x5) x2)) (∀ x4 . prim1 x4 x1 ⟶ ∃ x5 . and (prim1 x5 x0) (prim1 (7ee77.. x5 x4) x2))) (∀ x4 x5 x6 x7 . prim1 (7ee77.. x4 x5) x2 ⟶ prim1 (7ee77.. x6 x7) x2 ⟶ iff (x4 = x6) (x5 = x7))

type
ι → ι → ο

theory
HoTg

name
-

definition
PUgom..

Megalodon
-

proofgold address
TMWCk..

creator
1652 PrGxv../0ea0c..

owner
1652 PrGxv../0ea0c..

term root
bbda1..