Proofgold Object

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

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

theory
HotG

name
explicit_Ring_minus

definition
PUajT..

Megalodon
explicit_Ring_minus

proofgold address
TMHJ1..^{explicit_Ring_minus}

creator
4949 Pr6Pc../8eade..

owner
4949 Pr6Pc../8eade..

term root
2f43e..