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