∀ {α : Type u_1} (motive : Batteries.RBNode.Path α → Batteries.RBNode α → Sort u_2) (a : Batteries.RBNode α) (y : α)
  (parent : Batteries.RBNode.Path α) (b : Batteries.RBNode α)
  (h_1 : (t : Batteries.RBNode α) → motive Batteries.RBNode.Path.root t)
  (h_2 :
    (parent : Batteries.RBNode.Path α) →
      (y : α) → (b a : Batteries.RBNode α) → motive (Batteries.RBNode.Path.left Batteries.RBColor.red parent y b) a)
  (h_3 :
    (a : Batteries.RBNode α) →
      (y : α) →
        (parent : Batteries.RBNode.Path α) →
          (b : Batteries.RBNode α) → motive (Batteries.RBNode.Path.right Batteries.RBColor.red a y parent) b)
  (h_4 :
    (parent : Batteries.RBNode.Path α) →
      (y : α) → (b a : Batteries.RBNode α) → motive (Batteries.RBNode.Path.left Batteries.RBColor.black parent y b) a)
  (h_5 :
    (a : Batteries.RBNode α) →
      (y : α) →
        (parent : Batteries.RBNode.Path α) →
          (b : Batteries.RBNode α) → motive (Batteries.RBNode.Path.right Batteries.RBColor.black a y parent) b),
  (match Batteries.RBNode.Path.right Batteries.RBColor.red a y parent, b with
    | Batteries.RBNode.Path.root, t => h_1 t
    | Batteries.RBNode.Path.left Batteries.RBColor.red parent y b, a => h_2 parent y b a
    | Batteries.RBNode.Path.right Batteries.RBColor.red a y parent, b => h_3 a y parent b
    | Batteries.RBNode.Path.left Batteries.RBColor.black parent y b, a => h_4 parent y b a
    | Batteries.RBNode.Path.right Batteries.RBColor.black a y parent, b => h_5 a y parent b) =
    h_3 a y parent b