Proofgold Term Root Disambiguation

∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 . and (and (Group x3) (subgroup x1 x3)) (not (normal_subgroup x1 x3)) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0

as obj
-

as prop
f4475..^{nonnormal_subgroup}

theory
HotG

stx
a0c68..

address
TMaJX..^{nonnormal_subgroup}