Proofgold Object

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

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

theory
HotG

name
explicit_Field_minus

definition
PUefP..

Megalodon
explicit_Field_minus

proofgold address
TMYcE..^{explicit_Field_minus}

creator
4913 Pr6Pc../2cae4..

owner
4913 Pr6Pc../2cae4..

term root
5be57..