∀ {α : Type u_1} (motive : Batteries.RBNode α → Batteries.RBNode α → Sort u_2) (l : Batteries.RBNode α) (v : α)
  (r b : Batteries.RBNode α) (x : α) (c : Batteries.RBNode α)
  (h_1 : (x : Batteries.RBNode α) → motive Batteries.RBNode.nil x)
  (h_2 : (x : Batteries.RBNode α) → motive x Batteries.RBNode.nil)
  (h_3 :
    (a : Batteries.RBNode α) →
      (x : α) →
        (b c : Batteries.RBNode α) →
          (y : α) →
            (d : Batteries.RBNode α) →
              motive (Batteries.RBNode.node Batteries.RBColor.red a x b)
                (Batteries.RBNode.node Batteries.RBColor.red c y d))
  (h_4 :
    (a : Batteries.RBNode α) →
      (x : α) →
        (b c : Batteries.RBNode α) →
          (y : α) →
            (d : Batteries.RBNode α) →
              motive (Batteries.RBNode.node Batteries.RBColor.black a x b)
                (Batteries.RBNode.node Batteries.RBColor.black c y d))
  (h_5 :
    (a l : Batteries.RBNode α) →
      (v : α) →
        (r : Batteries.RBNode α) →
          a = Batteries.RBNode.node Batteries.RBColor.black l v r →
            (b : Batteries.RBNode α) →
              (x : α) →
                (c : Batteries.RBNode α) →
                  motive (Batteries.RBNode.node Batteries.RBColor.black l v r)
                    (Batteries.RBNode.node Batteries.RBColor.red b x c))
  (h_6 :
    (a : Batteries.RBNode α) →
      (x : α) →
        (b c l : Batteries.RBNode α) →
          (v : α) →
            (r : Batteries.RBNode α) →
              c = Batteries.RBNode.node Batteries.RBColor.black l v r →
                motive (Batteries.RBNode.node Batteries.RBColor.red a x b)
                  (Batteries.RBNode.node Batteries.RBColor.black l v r)),
  (match Batteries.RBNode.node Batteries.RBColor.black l v r, Batteries.RBNode.node Batteries.RBColor.red b x c with
    | Batteries.RBNode.nil, x => h_1 x
    | x, Batteries.RBNode.nil => h_2 x
    | Batteries.RBNode.node Batteries.RBColor.red a x b, Batteries.RBNode.node Batteries.RBColor.red c y d =>
      h_3 a x b c y d
    | Batteries.RBNode.node Batteries.RBColor.black a x b, Batteries.RBNode.node Batteries.RBColor.black c y d =>
      h_4 a x b c y d
    | a@h:(Batteries.RBNode.node Batteries.RBColor.black l v r), Batteries.RBNode.node Batteries.RBColor.red b x c =>
      h_5 a l v r h b x c
    | Batteries.RBNode.node Batteries.RBColor.red a x b, c@h:(Batteries.RBNode.node Batteries.RBColor.black l v r) =>
      h_6 a x b c l v r h) =
    h_5 (Batteries.RBNode.node Batteries.RBColor.black l v r) l v r ⋯ b x c