∀ {α : Type u_1} {cmp : α → α → Ordering} (x y : α) (a : Batteries.RBNode α) (x_1 : α) (b : Batteries.RBNode α)
  (motive :
    Batteries.RBNode.Ordered cmp (Batteries.RBNode.node Batteries.RBColor.red a x_1 b) ∧
        Batteries.RBNode.All (fun x_2 => Batteries.RBNode.cmpLT cmp x x_2)
            (Batteries.RBNode.node Batteries.RBColor.red a x_1 b) ∧
          Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp x y)
            (Batteries.RBNode.node Batteries.RBColor.red a x_1 b) →
      Prop)
  (x_2 :
    Batteries.RBNode.Ordered cmp (Batteries.RBNode.node Batteries.RBColor.red a x_1 b) ∧
      Batteries.RBNode.All (fun x_2 => Batteries.RBNode.cmpLT cmp x x_2)
          (Batteries.RBNode.node Batteries.RBColor.red a x_1 b) ∧
        Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp x y)
          (Batteries.RBNode.node Batteries.RBColor.red a x_1 b)),
  (∀ (b'z : Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp x x_1) a)
      (c'z : Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp x_1 x) b) (hb' : Batteries.RBNode.Ordered cmp a)
      (hc' : Batteries.RBNode.Ordered cmp b) (xz : Batteries.RBNode.cmpLT cmp x x_1)
      (xb' : Batteries.RBNode.All (fun x_3 => Batteries.RBNode.cmpLT cmp x x_3) a)
      (right : Batteries.RBNode.All (fun x_3 => Batteries.RBNode.cmpLT cmp x x_3) b)
      (zy : Batteries.RBNode.cmpLT cmp x_1 y) (left : Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp x y) a)
      (c'y : Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp x y) b), motive ⋯) →
    motive x_2