Proofgold Term Root Disambiguation

λ x0 . and (struct_b x0) (unpack_b_o x0 (λ x1 . λ x2 : ι → ι → ι . and (explicit_Group x1 x2) (explicit_abelian x1 x2)))

as obj
a355b..^{struct_b_abelian_group}

as prop
-

theory
HotG

stx
fe083..

address
TMbjx..^{struct_b_abelian_group}