∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B}
  {motive : HNNExtension.NormalWord d → Sort u_4} (g : G) (u : ℤˣ) (w : HNNExtension.NormalWord d)
  (h1 : w.head ∈ d.set u)
  (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u')
  (ofGroup : (g : G) → motive (HNNExtension.NormalWord.ofGroup g))
  (cons :
    (g : G) →
      (u : ℤˣ) →
        (w : HNNExtension.NormalWord d) →
          (h1 : w.head ∈ d.set u) →
            (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u') →
              motive w → motive (HNNExtension.NormalWord.cons g u w h1 h2)),
  HNNExtension.NormalWord.consRecOn (HNNExtension.NormalWord.cons g u w h1 h2) ofGroup cons =
    cons g u w h1 h2 (HNNExtension.NormalWord.consRecOn w ofGroup cons)