Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι → ι . abelian_Group (pack_b x0 x1) ⟶ and (Group (pack_b x0 x1)) (explicit_abelian x0 x1)

type
prop

theory
HotG

name
abelian_Group_E

proof
PUMaE..

Megalodon
abelian_Group_E

proofgold address
TMQz7..^{abelian_Group_E}

creator
4924 Pr6Pc../cc53e..

owner
4924 Pr6Pc../cc53e..

term root
0ddfd..