Proofgold Term Root Disambiguation

λ x0 x1 x2 x3 . unpack_b_o x0 (λ x4 . λ x5 : ι → ι → ι . and (and (x2 ∈ x4) (x3 ∈ x4)) (x5 x2 (explicit_Group_inverse x4 x5 x3) ∈ ap x1 0))

as obj
6de52..^{normal_subgroup_equiv}

as prop
-

theory
HotG

stx
a0c68..

address
TMRAS..^{normal_subgroup_equiv}