Proofgold Term Root Disambiguation

λ x0 x1 . and (subgroup x0 x1) (unpack_b_o x1 (λ x2 . λ x3 : ι → ι → ι . unpack_b_o x0 (λ x4 . λ x5 : ι → ι → ι . explicit_normal x2 x3 x4)))

as obj
e2b28..^{normal_subgroup}

as prop
-

theory
HotG

stx
a0c68..

address
TMd7x..^{normal_subgroup}