∀ {α : Type u_1} {x : Batteries.RBNode α} {n : ℕ} {v : α} {t : Batteries.RBNode α}
  (motive : (∃ c, (x.balance2 v t).Balanced c (n + 1)) → Prop) (x_1 : ∃ c, (x.balance2 v t).Balanced c (n + 1)),
  (∀ (c : Batteries.RBColor) (h : (x.balance2 v t).Balanced c (n + 1)), motive ⋯) → motive x_1