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