{G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} →
      {d : HNNExtension.NormalWord.TransversalPair G A B} →
        (toReducedWord : HNNExtension.NormalWord.ReducedWord G A B) →
          (∀ (u : ℤˣ) (g : G), (u, g) ∈ toReducedWord.toList → g ∈ d.set u) → HNNExtension.NormalWord d