∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (g : G) (u : ℤˣ) (w : HNNExtension.NormalWord d) (h1 : w.head ∈ d.set u)
  (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u'),
  HNNExtension.NormalWord.ReducedWord.prod φ (HNNExtension.NormalWord.cons g u w h1 h2).toReducedWord =
    HNNExtension.of g * (HNNExtension.t ^ ↑u * HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord)