∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (a : ℤˣ × G)
  (l : List (ℤˣ × G)) (g : G)
  (chain : List.IsChain (fun a b => a.2 ∈ HNNExtension.toSubgroup A B a.1 → a.1 = b.1) (a :: l))
  (mem_set : ∀ (u : ℤˣ) (g_1 : G), (u, g_1) ∈ { head := g, toList := a :: l, chain := chain }.toList → g_1 ∈ d.set u),
  ∀ u' ∈ Option.map Prod.fst { head := a.2, toList := l, chain := ⋯, mem_set := ⋯ }.toList.head?,
    { head := a.2, toList := l, chain := ⋯, mem_set := ⋯ }.head ∈ HNNExtension.toSubgroup A B a.1 → a.1 = u'