Proofgold Object

λ x0 . λ x1 : ι → ι . prim0 (λ x2 . ∀ x3 . iff (prim1 x3 x2) (∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (x3 = x1 x5) ⟶ x4) ⟶ x4))

type
ι → (ι → ι) → ι

theory
HoTg

name
-

definition
PUdeW..

Megalodon
-

proofgold address
TMRs6..

creator
1652 PrGxv../dd729..

owner
1652 PrGxv../dd729..

term root
3041a..