∀ {α : Type u_1} (motive : Batteries.RBNode α → Batteries.RBNode.Path α → Sort u_2) (c : Batteries.RBColor)
  (a : Batteries.RBNode α) (y : α) (b : Batteries.RBNode α) (path : Batteries.RBNode.Path α)
  (h_1 : (path : Batteries.RBNode.Path α) → motive Batteries.RBNode.nil path)
  (h_2 :
    (n : Batteries.RBNode α) →
      (c : Batteries.RBColor) →
        (a : Batteries.RBNode α) →
          (y : α) →
            (b : Batteries.RBNode α) →
              n = Batteries.RBNode.node c a y b →
                (path : Batteries.RBNode.Path α) → motive (Batteries.RBNode.node c a y b) path),
  (match Batteries.RBNode.node c a y b, path with
    | Batteries.RBNode.nil, path => h_1 path
    | n@h:(Batteries.RBNode.node c a y b), path => h_2 n c a y b h path) =
    h_2 (Batteries.RBNode.node c a y b) c a y b ⋯ path