{G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} →
      {d : HNNExtension.NormalWord.TransversalPair G A B} →
        HNNExtension.NormalWord d → HNNExtension.NormalWord.ReducedWord G A B