∀ {α : Type u_1} {cut : α → Ordering} {path : Batteries.RBNode.Path α} (c : Batteries.RBColor) (a : Batteries.RBNode α)
  (y : α)
  (motive :
    (path' : Batteries.RBNode.Path α) →
      (t' : Batteries.RBNode α) →
        Batteries.RBNode.zoom cut Batteries.RBNode.nil (Batteries.RBNode.Path.right c a y path) = (t', path') → Prop)
  (path' : Batteries.RBNode.Path α) (t' : Batteries.RBNode α)
  (x : Batteries.RBNode.zoom cut Batteries.RBNode.nil (Batteries.RBNode.Path.right c a y path) = (t', path')),
  (∀ (a_1 : Unit), motive (Batteries.RBNode.Path.right c a y path) Batteries.RBNode.nil ⋯) → motive path' t' x