∀ {α : Type u_1} {cmp : α → α → Ordering} (parent : Batteries.RBNode.Path α) (v : α) (r x : Batteries.RBNode α)
  (motive :
    (Batteries.RBNode.Path.Ordered cmp parent ∧
          Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp v x) r ∧
            Batteries.RBNode.Path.RootOrdered cmp parent v ∧
              Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp parent) r ∧ Batteries.RBNode.Ordered cmp r) ∧
        Batteries.RBNode.Ordered cmp x ∧
          Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp x v) x ∧
            Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp parent) x →
      Prop)
  (x_1 :
    (Batteries.RBNode.Path.Ordered cmp parent ∧
        Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp v x) r ∧
          Batteries.RBNode.Path.RootOrdered cmp parent v ∧
            Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp parent) r ∧ Batteries.RBNode.Ordered cmp r) ∧
      Batteries.RBNode.Ordered cmp x ∧
        Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp x v) x ∧
          Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp parent) x),
  (∀ (hp : Batteries.RBNode.Path.Ordered cmp parent)
      (xb : Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp v x) r)
      (xp : Batteries.RBNode.Path.RootOrdered cmp parent v)
      (bp : Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp parent) r) (hb : Batteries.RBNode.Ordered cmp r)
      (ha : Batteries.RBNode.Ordered cmp x) (ax : Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp x v) x)
      (ap : Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp parent) x), motive ⋯) →
    motive x_1