∀ {c₀ : Batteries.RBColor} {n₀ : ℕ} {α : Type u_1}
  {motive :
    (a : Batteries.RBNode.Path α) →
      (a_1 : Batteries.RBColor) → (a_2 : ℕ) → Batteries.RBNode.Path.Balanced c₀ n₀ a a_1 a_2 → Prop},
  motive Batteries.RBNode.Path.root c₀ n₀ ⋯ →
    (∀ {y : Batteries.RBNode α} {n : ℕ} {parent : Batteries.RBNode.Path α} {v : α}
        (a : y.Balanced Batteries.RBColor.black n)
        (a_1 : Batteries.RBNode.Path.Balanced c₀ n₀ parent Batteries.RBColor.red n),
        motive parent Batteries.RBColor.red n a_1 →
          motive (Batteries.RBNode.Path.left Batteries.RBColor.red parent v y) Batteries.RBColor.black n ⋯) →
      (∀ {x : Batteries.RBNode α} {n : ℕ} {v : α} {parent : Batteries.RBNode.Path α}
          (a : x.Balanced Batteries.RBColor.black n)
          (a_1 : Batteries.RBNode.Path.Balanced c₀ n₀ parent Batteries.RBColor.red n),
          motive parent Batteries.RBColor.red n a_1 →
            motive (Batteries.RBNode.Path.right Batteries.RBColor.red x v parent) Batteries.RBColor.black n ⋯) →
        (∀ {y : Batteries.RBNode α} {c₂ : Batteries.RBColor} {n : ℕ} {parent : Batteries.RBNode.Path α} {v : α}
            {c₁ : Batteries.RBColor} (a : y.Balanced c₂ n)
            (a_1 : Batteries.RBNode.Path.Balanced c₀ n₀ parent Batteries.RBColor.black (n + 1)),
            motive parent Batteries.RBColor.black (n + 1) a_1 →
              motive (Batteries.RBNode.Path.left Batteries.RBColor.black parent v y) c₁ n ⋯) →
          (∀ {x : Batteries.RBNode α} {c₁ : Batteries.RBColor} {n : ℕ} {v : α} {parent : Batteries.RBNode.Path α}
              {c₂ : Batteries.RBColor} (a : x.Balanced c₁ n)
              (a_1 : Batteries.RBNode.Path.Balanced c₀ n₀ parent Batteries.RBColor.black (n + 1)),
              motive parent Batteries.RBColor.black (n + 1) a_1 →
                motive (Batteries.RBNode.Path.right Batteries.RBColor.black x v parent) c₂ n ⋯) →
            ∀ {a : Batteries.RBNode.Path α} {a_1 : Batteries.RBColor} {a_2 : ℕ}
              (t : Batteries.RBNode.Path.Balanced c₀ n₀ a a_1 a_2), motive a a_1 a_2 t