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