∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (g : HNNExtension G A B φ) (w : HNNExtension.NormalWord d),
  HNNExtension.NormalWord.ReducedWord.prod φ (g • w).toReducedWord =
    g * HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord