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