Proofgold Object

λ x0 . λ x1 : ι → ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 = x1 x3 x2

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

theory
HotG

name
explicit_abelian

definition
PUMaE..

Megalodon
explicit_abelian

proofgold address
TMWoa..^{explicit_abelian}

creator
4924 Pr6Pc../7e204..

owner
4924 Pr6Pc../7e204..

term root
05d54..