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