∀ (motive : Batteries.RBColor → ℕ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive Batteries.RBColor.red n)
  (h_2 : (n : ℕ) → motive Batteries.RBColor.black n),
  (match Batteries.RBColor.black, n with
    | Batteries.RBColor.red, n => h_1 n
    | Batteries.RBColor.black, n => h_2 n) =
    h_2 n