∀ {α : Type u_1} {cmp : α → α → Ordering} (l : Batteries.RBNode α) (x : α) (parent : Batteries.RBNode.Path α)
  (motive :
    ((List.Pairwise (Batteries.RBNode.cmpLT cmp) parent.listL ∧
          (List.Pairwise (Batteries.RBNode.cmpLT cmp) l.toList ∧ ∀ x_1 ∈ l, Batteries.RBNode.cmpLT cmp x_1 x) ∧
            (∀ x ∈ parent.listL, ∀ x_2 ∈ l, Batteries.RBNode.cmpLT cmp x x_2) ∧
              ∀ a ∈ parent.listL, Batteries.RBNode.cmpLT cmp a x) ∧
        List.Pairwise (Batteries.RBNode.cmpLT cmp) parent.listR ∧
          (∀ x ∈ parent.listL, ∀ y ∈ parent.listR, Batteries.RBNode.cmpLT cmp x y) ∧
            (∀ x ∈ l, ∀ a ∈ parent.listR, Batteries.RBNode.cmpLT cmp x a) ∧
              ∀ a ∈ parent.listR, Batteries.RBNode.cmpLT cmp x a) →
      Prop)
  (x_1 :
    (List.Pairwise (Batteries.RBNode.cmpLT cmp) parent.listL ∧
        (List.Pairwise (Batteries.RBNode.cmpLT cmp) l.toList ∧ ∀ x_1 ∈ l, Batteries.RBNode.cmpLT cmp x_1 x) ∧
          (∀ x ∈ parent.listL, ∀ x_2 ∈ l, Batteries.RBNode.cmpLT cmp x x_2) ∧
            ∀ a ∈ parent.listL, Batteries.RBNode.cmpLT cmp a x) ∧
      List.Pairwise (Batteries.RBNode.cmpLT cmp) parent.listR ∧
        (∀ x ∈ parent.listL, ∀ y ∈ parent.listR, Batteries.RBNode.cmpLT cmp x y) ∧
          (∀ x ∈ l, ∀ a ∈ parent.listR, Batteries.RBNode.cmpLT cmp x a) ∧
            ∀ a ∈ parent.listR, Batteries.RBNode.cmpLT cmp x a),
  (∀ (hL : List.Pairwise (Batteries.RBNode.cmpLT cmp) parent.listL)
      (hl : List.Pairwise (Batteries.RBNode.cmpLT cmp) l.toList) (lx : ∀ x_2 ∈ l, Batteries.RBNode.cmpLT cmp x_2 x)
      (Ll : ∀ x ∈ parent.listL, ∀ x_3 ∈ l, Batteries.RBNode.cmpLT cmp x x_3)
      (Lx : ∀ a ∈ parent.listL, Batteries.RBNode.cmpLT cmp a x)
      (hR : List.Pairwise (Batteries.RBNode.cmpLT cmp) parent.listR)
      (LR : ∀ x ∈ parent.listL, ∀ y ∈ parent.listR, Batteries.RBNode.cmpLT cmp x y)
      (lR : ∀ x ∈ l, ∀ a ∈ parent.listR, Batteries.RBNode.cmpLT cmp x a)
      (xR : ∀ a ∈ parent.listR, Batteries.RBNode.cmpLT cmp x a), motive ⋯) →
    motive x_1