Proofgold Term Root Disambiguation

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

as obj
4a843..^{trivial_Group_p}

as prop
-

theory
HotG

stx
a0c68..

address
TMXgR..^{trivial_Group_p}