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