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