Proofgold Object

λ x0 . and (Group x0) (∀ x1 . x1 ∈ ap x0 0 ⟶ ∀ x2 . x2 ∈ ap x0 0 ⟶ x1 = x2)

type
ι → ο

theory
HotG

name
trivial_Group_p

definition
PUMaE..

Megalodon
trivial_Group_p

proofgold address
TMMyf..^{trivial_Group_p}

creator
4924 Pr6Pc../30bd3..

owner
4924 Pr6Pc../30bd3..

term root
759fd..