{G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} →
      {d : HNNExtension.NormalWord.TransversalPair G A B} →
        G →
          (u : ℤˣ) →
            (w : HNNExtension.NormalWord d) →
              w.head ∈ d.set u →
                (∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u') →
                  HNNExtension.NormalWord d