∀ {α : Type u_1} {σ : Sort u_3} (motive : Batteries.RBNode α → σ → Sort u_2) (b : σ)
  (h_1 : (b : σ) → motive Batteries.RBNode.nil b)
  (h_2 :
    (c : Batteries.RBColor) →
      (l : Batteries.RBNode α) →
        (v : α) → (r : Batteries.RBNode α) → (b : σ) → motive (Batteries.RBNode.node c l v r) b),
  (match Batteries.RBNode.nil, b with
    | Batteries.RBNode.nil, b => h_1 b
    | Batteries.RBNode.node c l v r, b => h_2 c l v r b) =
    h_1 b