∀ {α : Type u_1} {cut : α → Ordering} {a : Batteries.RBNode α}
  (motive :
    (b : Batteries.RBNode α) →
      (n : ℕ) →
        Batteries.RBNode.DelProp b.isBlack (Batteries.RBNode.del cut b) n →
          a.Balanced Batteries.RBColor.black n →
            b.Balanced Batteries.RBColor.black n →
              Batteries.RBNode.DelProp a.isBlack (Batteries.RBNode.del cut a) n → Prop)
  (b : Batteries.RBNode α) (n : ℕ) (ihb : Batteries.RBNode.DelProp b.isBlack (Batteries.RBNode.del cut b) n)
  (ha : a.Balanced Batteries.RBColor.black n) (hb : b.Balanced Batteries.RBColor.black n)
  (iha : Batteries.RBNode.DelProp a.isBlack (Batteries.RBNode.del cut a) n),
  (∀ (x : ℕ)
      (x_1 : Batteries.RBNode.DelProp Batteries.RBNode.nil.isBlack (Batteries.RBNode.del cut Batteries.RBNode.nil) x)
      (ha : a.Balanced Batteries.RBColor.black x) (hb : Batteries.RBNode.nil.Balanced Batteries.RBColor.black x)
      (iha : Batteries.RBNode.DelProp a.isBlack (Batteries.RBNode.del cut a) x),
      motive Batteries.RBNode.nil x x_1 ha hb iha) →
    (∀ (l : Batteries.RBNode α) (v : α) (r : Batteries.RBNode α) (n : ℕ)
        (hb :
          Batteries.RBNode.RedRed True (Batteries.RBNode.del cut (Batteries.RBNode.node Batteries.RBColor.black l v r))
            n)
        (ha : a.Balanced Batteries.RBColor.black (n + 1))
        (hb_1 : (Batteries.RBNode.node Batteries.RBColor.black l v r).Balanced Batteries.RBColor.black (n + 1))
        (iha : Batteries.RBNode.DelProp a.isBlack (Batteries.RBNode.del cut a) (n + 1)),
        motive (Batteries.RBNode.node Batteries.RBColor.black l v r) (n + 1) ⋯ ha hb_1 iha) →
      motive b n ihb ha hb iha