∀ {α : Type u_1} (motive : Batteries.RBNode α → Sort u_2) (a : Batteries.RBNode α) (x : α) (b : Batteries.RBNode α)
  (h_1 :
    (a : Batteries.RBNode α) →
      (x : α) → (b : Batteries.RBNode α) → motive (Batteries.RBNode.node Batteries.RBColor.black a x b))
  (h_2 :
    (a : Batteries.RBNode α) →
      (x : α) →
        (b : Batteries.RBNode α) →
          (y : α) →
            (c : Batteries.RBNode α) →
              motive
                (Batteries.RBNode.node Batteries.RBColor.red a x (Batteries.RBNode.node Batteries.RBColor.black b y c)))
  (h_3 : (l : Batteries.RBNode α) → motive l),
  (match Batteries.RBNode.node Batteries.RBColor.black a x b with
    | Batteries.RBNode.node Batteries.RBColor.black a x b => h_1 a x b
    | Batteries.RBNode.node Batteries.RBColor.red a x (Batteries.RBNode.node Batteries.RBColor.black b y c) =>
      h_2 a x b y c
    | l => h_3 l) =
    h_1 a x b