∀ {α : 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) parent.listR ∧
            ∀ x ∈ parent.listL, ∀ y ∈ parent.listR, Batteries.RBNode.cmpLT cmp x y) ∧
        (∀ x_1 ∈ l, Batteries.RBNode.cmpLT cmp x_1 x) ∧
          ((∀ a ∈ parent.listL, Batteries.RBNode.cmpLT cmp a x) ∧ ∀ a ∈ parent.listR, Batteries.RBNode.cmpLT cmp x a) ∧
            ((∀ x ∈ l, ∀ a ∈ parent.listL, Batteries.RBNode.cmpLT cmp a x) ∧
                ∀ x ∈ l, ∀ a ∈ parent.listR, Batteries.RBNode.cmpLT cmp x a) ∧
              List.Pairwise (Batteries.RBNode.cmpLT cmp) l.toList →
      Prop)
  (x_1 :
    (List.Pairwise (Batteries.RBNode.cmpLT cmp) parent.listL ∧
        List.Pairwise (Batteries.RBNode.cmpLT cmp) parent.listR ∧
          ∀ x ∈ parent.listL, ∀ y ∈ parent.listR, Batteries.RBNode.cmpLT cmp x y) ∧
      (∀ x_1 ∈ l, Batteries.RBNode.cmpLT cmp x_1 x) ∧
        ((∀ a ∈ parent.listL, Batteries.RBNode.cmpLT cmp a x) ∧ ∀ a ∈ parent.listR, Batteries.RBNode.cmpLT cmp x a) ∧
          ((∀ x ∈ l, ∀ a ∈ parent.listL, Batteries.RBNode.cmpLT cmp a x) ∧
              ∀ x ∈ l, ∀ a ∈ parent.listR, Batteries.RBNode.cmpLT cmp x a) ∧
            List.Pairwise (Batteries.RBNode.cmpLT cmp) l.toList),
  (∀ (hL : List.Pairwise (Batteries.RBNode.cmpLT cmp) parent.listL)
      (hR : List.Pairwise (Batteries.RBNode.cmpLT cmp) parent.listR)
      (LR : ∀ x ∈ parent.listL, ∀ y ∈ parent.listR, Batteries.RBNode.cmpLT cmp x y)
      (lx : ∀ x_2 ∈ l, Batteries.RBNode.cmpLT cmp x_2 x) (Lx : ∀ a ∈ parent.listL, Batteries.RBNode.cmpLT cmp a x)
      (xR : ∀ a ∈ parent.listR, Batteries.RBNode.cmpLT cmp x a)
      (lL : ∀ x ∈ l, ∀ a ∈ parent.listL, Batteries.RBNode.cmpLT cmp a x)
      (lR : ∀ x ∈ l, ∀ a ∈ parent.listR, Batteries.RBNode.cmpLT cmp x a)
      (hl : List.Pairwise (Batteries.RBNode.cmpLT cmp) l.toList), motive ⋯) →
    motive x_1