∀ {α : Type u_1} (motive : Batteries.RBNode α → Sort u_2) (l : Batteries.RBNode α)
  (h_1 :
    (a : Batteries.RBNode α) →
      (x : α) → (b : Batteries.RBNode α) → motive (Batteries.RBNode.node Batteries.RBColor.red a x b))
  (h_2 : (l : Batteries.RBNode α) → motive l) (a : Batteries.RBNode α) (x : α) (b : Batteries.RBNode α),
  l = Batteries.RBNode.node Batteries.RBColor.red a x b →
    (match l with
      | Batteries.RBNode.node Batteries.RBColor.red a x b => h_1 a x b
      | l => h_2 l) ≍
      h_1 a x b