{G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} →
      {motive : HNNExtension.NormalWord.ReducedWord G A B → Sort u} →
        ((head : G) →
            (toList : List (ℤˣ × G)) →
              (chain : List.IsChain (fun a b => a.2 ∈ HNNExtension.toSubgroup A B a.1 → a.1 = b.1) toList) →
                motive { head := head, toList := toList, chain := chain }) →
          (t : HNNExtension.NormalWord.ReducedWord G A B) → motive t