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