∀ {α : Type u_1} {cmp : α → α → Ordering} {motive : (a : Batteries.RBNode α) → Batteries.RBNode.WF cmp a → Prop}
  {t : Batteries.RBNode α} {cut : α → Ordering} (a : Batteries.RBNode.WF cmp t),
  Batteries.RBNode.WF.below a → motive t a → Batteries.RBNode.WF.below ⋯