∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) (w : HNNExtension.NormalWord.ReducedWord G A B),
  HNNExtension.NormalWord.ReducedWord.prod φ w =
    HNNExtension.of w.head * (List.map (fun x => HNNExtension.t ^ ↑x.1 * HNNExtension.of x.2) w.toList).prod