∀ {α : Type u_1} {cut : α → Ordering} {cmp : α → α → Ordering} {f : α → α} {t : Batteries.RBNode α},
  Batteries.RBNode.OnRoot (fun x => Batteries.RBNode.cmpEq cmp (f x) x) (Batteries.RBNode.zoom cut t).1 →
    Batteries.RBNode.WF cmp t → Batteries.RBNode.WF cmp (Batteries.RBNode.modify cut f t)