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