∀ {α : Type u_1} {cut : α → Ordering} {t : Batteries.RBNode α}
  (motive :
    (∃ n', Batteries.RBNode.RedRed (t.isBlack = Batteries.RBColor.black) (Batteries.RBNode.del cut t) n') → Prop)
  (x : ∃ n', Batteries.RBNode.RedRed (t.isBlack = Batteries.RBColor.black) (Batteries.RBNode.del cut t) n'),
  (∀ (w : ℕ) (h : Batteries.RBNode.RedRed (t.isBlack = Batteries.RBColor.black) (Batteries.RBNode.del cut t) w),
      motive ⋯) →
    motive x