Proofgold Object

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

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

theory
HoTg

name
explicit_Ring_minus

definition
PURd1..

Megalodon
-

proofgold address
TMZbQ..

creator
4786 PrGxv../bef62..

owner
4786 PrGxv../bef62..

term root
2f43e..