∀ {α : Type u_1} {t : Batteries.RBNode α} {n : ℕ}
  (motive :
    (c : Batteries.RBColor) →
      (match c with
        | Batteries.RBColor.black => ∃ n', n = n' + 1 ∧ Batteries.RBNode.RedRed True t n'
        | Batteries.RBColor.red => ∃ c, t.Balanced c n) →
        Prop)
  (c : Batteries.RBColor)
  (h :
    match c with
    | Batteries.RBColor.black => ∃ n', n = n' + 1 ∧ Batteries.RBNode.RedRed True t n'
    | Batteries.RBColor.red => ∃ c, t.Balanced c n),
  (∀ (w : Batteries.RBColor) (h : t.Balanced w n), motive Batteries.RBColor.red ⋯) →
    (∀ (w : ℕ) (left : n = w + 1) (h : Batteries.RBNode.RedRed True t w), motive Batteries.RBColor.black ⋯) → motive c h