∀ {α : Type u_1} (cmp : α → α → Ordering) (v : α) {a b : Batteries.RBNode α}
  (motive :
    (n : ℕ) →
      (x : Batteries.RBNode α) →
        Batteries.RBNode.RedRed (a.isRed = Batteries.RBColor.red) x n →
          a.Balanced Batteries.RBColor.black n →
            b.Balanced Batteries.RBColor.black n →
              Batteries.RBNode.RedRed (b.isRed = Batteries.RBColor.red) (Batteries.RBNode.ins cmp v b) n → Prop)
  (n : ℕ) (x : Batteries.RBNode α) (ihl : Batteries.RBNode.RedRed (a.isRed = Batteries.RBColor.red) x n)
  (hl : a.Balanced Batteries.RBColor.black n) (hr : b.Balanced Batteries.RBColor.black n)
  (ihr : Batteries.RBNode.RedRed (b.isRed = Batteries.RBColor.red) (Batteries.RBNode.ins cmp v b) n),
  (∀ (hl : a.Balanced Batteries.RBColor.black 0) (hr : b.Balanced Batteries.RBColor.black 0)
      (ihr : Batteries.RBNode.RedRed (b.isRed = Batteries.RBColor.red) (Batteries.RBNode.ins cmp v b) 0),
      motive 0 Batteries.RBNode.nil ⋯ hl hr ihr) →
    (∀ (n : ℕ) (l : Batteries.RBNode α) (v_1 : α) (r : Batteries.RBNode α) (ha : l.Balanced Batteries.RBColor.black n)
        (hb : r.Balanced Batteries.RBColor.black n) (hl : a.Balanced Batteries.RBColor.black n)
        (hr : b.Balanced Batteries.RBColor.black n)
        (ihr : Batteries.RBNode.RedRed (b.isRed = Batteries.RBColor.red) (Batteries.RBNode.ins cmp v b) n),
        motive n (Batteries.RBNode.node Batteries.RBColor.red l v_1 r) ⋯ hl hr ihr) →
      (∀ (l : Batteries.RBNode α) (v_1 : α) (r : Batteries.RBNode α) (n : ℕ) (c₁ c₂ : Batteries.RBColor)
          (ha : l.Balanced c₁ n) (hb : r.Balanced c₂ n) (hl : a.Balanced Batteries.RBColor.black (n + 1))
          (hr : b.Balanced Batteries.RBColor.black (n + 1))
          (ihr : Batteries.RBNode.RedRed (b.isRed = Batteries.RBColor.red) (Batteries.RBNode.ins cmp v b) (n + 1)),
          motive (n + 1) (Batteries.RBNode.node Batteries.RBColor.black l v_1 r) ⋯ hl hr ihr) →
        (∀ (n : ℕ) (a_1 : Batteries.RBNode α) (c₁ : Batteries.RBColor) (b_1 : Batteries.RBNode α)
            (c₂ : Batteries.RBColor) (x : α) (h : a.isRed = Batteries.RBColor.red) (a_2 : a_1.Balanced c₁ n)
            (a_3 : b_1.Balanced c₂ n) (hl : a.Balanced Batteries.RBColor.black n)
            (hr : b.Balanced Batteries.RBColor.black n)
            (ihr : Batteries.RBNode.RedRed (b.isRed = Batteries.RBColor.red) (Batteries.RBNode.ins cmp v b) n),
            motive n (Batteries.RBNode.node Batteries.RBColor.red a_1 x b_1) ⋯ hl hr ihr) →
          motive n x ihl hl hr ihr