Proofgold Term Root Disambiguation

λ x0 x1 . unpack_b_i x0 (λ x2 . λ x3 : ι → ι → ι . pack_b (Sep x2 (quotient (normal_subgroup_equiv x0 x1))) (λ x4 x5 . canonical_elt (normal_subgroup_equiv x0 x1) (x3 x4 x5)))

as obj
ef67e..^{quotient_Group}

as prop
-

theory
HotG

stx
a0c68..

address
TMRMV..^{quotient_Group}