∀ {α : Type u_1} (motive : (n : ℕ) → (c : Batteries.RBColor) → (t : Batteries.RBNode α) → t.Balanced c n → Prop) (n : ℕ)
  (c : Batteries.RBColor) (t : Batteries.RBNode α) (x : t.Balanced c n),
  (∀ (a : Unit), motive 0 Batteries.RBColor.black Batteries.RBNode.nil ⋯) →
    (∀ (n : ℕ) (x y : Batteries.RBNode α) (v : α) (hl : x.Balanced Batteries.RBColor.black n)
        (hr : y.Balanced Batteries.RBColor.black n),
        motive n Batteries.RBColor.red (Batteries.RBNode.node Batteries.RBColor.red x v y) ⋯) →
      (∀ (x : Batteries.RBNode α) (c₁ : Batteries.RBColor) (n : ℕ) (y : Batteries.RBNode α) (c₂ : Batteries.RBColor)
          (v : α) (hl : x.Balanced c₁ n) (hr : y.Balanced c₂ n),
          motive (n + 1) Batteries.RBColor.black (Batteries.RBNode.node Batteries.RBColor.black x v y) ⋯) →
        motive n c t x