∀ {α : Type u_1} {c₀ : Batteries.RBColor} {n₀ : ℕ} {y : Batteries.RBNode α} {parent : Batteries.RBNode.Path α}
  (motive :
    (n : ℕ) →
      (t : Batteries.RBNode α) →
        Batteries.RBNode.RedRed (Batteries.RBColor.black = Batteries.RBColor.red) t n →
          y.Balanced Batteries.RBColor.black n →
            Batteries.RBNode.Path.Balanced c₀ n₀ parent Batteries.RBColor.red n →
              (∀ {t : Batteries.RBNode α},
                  Batteries.RBNode.RedRed (Batteries.RBColor.red = Batteries.RBColor.red) t n →
                    ∃ n, (parent.ins t).Balanced Batteries.RBColor.black n) →
                Prop)
  (n : ℕ) (t : Batteries.RBNode α) (ht : Batteries.RBNode.RedRed (Batteries.RBColor.black = Batteries.RBColor.red) t n)
  (hr : y.Balanced Batteries.RBColor.black n) (hp : Batteries.RBNode.Path.Balanced c₀ n₀ parent Batteries.RBColor.red n)
  (ih :
    ∀ {t : Batteries.RBNode α},
      Batteries.RBNode.RedRed (Batteries.RBColor.red = Batteries.RBColor.red) t n →
        ∃ n, (parent.ins t).Balanced Batteries.RBColor.black n),
  (∀ (hr : y.Balanced Batteries.RBColor.black 0)
      (hp : Batteries.RBNode.Path.Balanced c₀ n₀ parent Batteries.RBColor.red 0)
      (ih :
        ∀ {t : Batteries.RBNode α},
          Batteries.RBNode.RedRed (Batteries.RBColor.red = Batteries.RBColor.red) t 0 →
            ∃ n, (parent.ins t).Balanced Batteries.RBColor.black n),
      motive 0 Batteries.RBNode.nil ⋯ hr hp ih) →
    (∀ (x : ℕ) (l : Batteries.RBNode α) (v : α) (r : Batteries.RBNode α) (ha : l.Balanced Batteries.RBColor.black x)
        (hb : r.Balanced Batteries.RBColor.black x) (hr : y.Balanced Batteries.RBColor.black x)
        (hp : Batteries.RBNode.Path.Balanced c₀ n₀ parent Batteries.RBColor.red x)
        (ih :
          ∀ {t : Batteries.RBNode α},
            Batteries.RBNode.RedRed (Batteries.RBColor.red = Batteries.RBColor.red) t x →
              ∃ n, (parent.ins t).Balanced Batteries.RBColor.black n),
        motive x (Batteries.RBNode.node Batteries.RBColor.red l v r) ⋯ hr hp ih) →
      (∀ (l : Batteries.RBNode α) (v : α) (r : Batteries.RBNode α) (n : ℕ) (c₁ c₂ : Batteries.RBColor)
          (ha : l.Balanced c₁ n) (hb : r.Balanced c₂ n) (hr : y.Balanced Batteries.RBColor.black (n + 1))
          (hp : Batteries.RBNode.Path.Balanced c₀ n₀ parent Batteries.RBColor.red (n + 1))
          (ih :
            ∀ {t : Batteries.RBNode α},
              Batteries.RBNode.RedRed (Batteries.RBColor.red = Batteries.RBColor.red) t (n + 1) →
                ∃ n, (parent.ins t).Balanced Batteries.RBColor.black n),
          motive (n + 1) (Batteries.RBNode.node Batteries.RBColor.black l v r) ⋯ hr hp ih) →
        motive n t ht hr hp ih