∀ {α : Type u_1} (motive : Batteries.RBNode.Path α → Sort u_2) (h_1 : Unit → motive Batteries.RBNode.Path.root)
  (h_2 :
    (c : Batteries.RBColor) →
      (parent : Batteries.RBNode.Path α) →
        (v : α) → (r : Batteries.RBNode α) → motive (Batteries.RBNode.Path.left c parent v r))
  (h_3 :
    (c : Batteries.RBColor) →
      (l : Batteries.RBNode α) →
        (v : α) → (parent : Batteries.RBNode.Path α) → motive (Batteries.RBNode.Path.right c l v parent)),
  (match Batteries.RBNode.Path.root with
    | Batteries.RBNode.Path.root => h_1 ()
    | Batteries.RBNode.Path.left c parent v r => h_2 c parent v r
    | Batteries.RBNode.Path.right c l v parent => h_3 c l v parent) =
    h_1 ()