∀ {α : Type u_1} {cmp : α → α → Ordering}
  (motive :
    (x : Batteries.RBNode.Path α) →
      (x_1 : Batteries.RBNode α) →
        Batteries.RBNode.Ordered cmp x_1 →
          Batteries.RBNode.Path.Ordered cmp x →
            Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp x) x_1 → Prop)
  (x : Batteries.RBNode.Path α) (x_1 : Batteries.RBNode α) (x_2 : Batteries.RBNode.Ordered cmp x_1)
  (x_3 : Batteries.RBNode.Path.Ordered cmp x)
  (x_4 : Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp x) x_1),
  (∀ (x : Batteries.RBNode α) (ht : Batteries.RBNode.Ordered cmp x)
      (x_5 : Batteries.RBNode.Path.Ordered cmp Batteries.RBNode.Path.root)
      (x_6 : Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp Batteries.RBNode.Path.root) x),
      motive Batteries.RBNode.Path.root x ht x_5 x_6) →
    (∀ (parent : Batteries.RBNode.Path α) (x : α) (b a : Batteries.RBNode α) (ha : Batteries.RBNode.Ordered cmp a)
        (hp : Batteries.RBNode.Path.Ordered cmp parent)
        (xb : Batteries.RBNode.All (fun x_5 => Batteries.RBNode.cmpLT cmp x x_5) b)
        (xp : Batteries.RBNode.Path.RootOrdered cmp parent x)
        (bp : Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp parent) b)
        (hb : Batteries.RBNode.Ordered cmp b)
        (H :
          Batteries.RBNode.All
            (Batteries.RBNode.Path.RootOrdered cmp (Batteries.RBNode.Path.left Batteries.RBColor.red parent x b)) a),
        motive (Batteries.RBNode.Path.left Batteries.RBColor.red parent x b) a ha ⋯ H) →
      (∀ (a : Batteries.RBNode α) (x : α) (parent : Batteries.RBNode.Path α) (b : Batteries.RBNode α)
          (hb : Batteries.RBNode.Ordered cmp b) (hp : Batteries.RBNode.Path.Ordered cmp parent)
          (ax : Batteries.RBNode.All (fun x_5 => Batteries.RBNode.cmpLT cmp x_5 x) a)
          (xp : Batteries.RBNode.Path.RootOrdered cmp parent x)
          (ap : Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp parent) a)
          (ha : Batteries.RBNode.Ordered cmp a)
          (H :
            Batteries.RBNode.All
              (Batteries.RBNode.Path.RootOrdered cmp (Batteries.RBNode.Path.right Batteries.RBColor.red a x parent)) b),
          motive (Batteries.RBNode.Path.right Batteries.RBColor.red a x parent) b hb ⋯ H) →
        (∀ (parent : Batteries.RBNode.Path α) (x : α) (b a : Batteries.RBNode α) (ha : Batteries.RBNode.Ordered cmp a)
            (hp : Batteries.RBNode.Path.Ordered cmp parent)
            (xb : Batteries.RBNode.All (fun x_5 => Batteries.RBNode.cmpLT cmp x x_5) b)
            (xp : Batteries.RBNode.Path.RootOrdered cmp parent x)
            (bp : Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp parent) b)
            (hb : Batteries.RBNode.Ordered cmp b)
            (H :
              Batteries.RBNode.All
                (Batteries.RBNode.Path.RootOrdered cmp (Batteries.RBNode.Path.left Batteries.RBColor.black parent x b))
                a),
            motive (Batteries.RBNode.Path.left Batteries.RBColor.black parent x b) a ha ⋯ H) →
          (∀ (a : Batteries.RBNode α) (x : α) (parent : Batteries.RBNode.Path α) (b : Batteries.RBNode α)
              (hb : Batteries.RBNode.Ordered cmp b) (hp : Batteries.RBNode.Path.Ordered cmp parent)
              (ax : Batteries.RBNode.All (fun x_5 => Batteries.RBNode.cmpLT cmp x_5 x) a)
              (xp : Batteries.RBNode.Path.RootOrdered cmp parent x)
              (ap : Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp parent) a)
              (ha : Batteries.RBNode.Ordered cmp a)
              (H :
                Batteries.RBNode.All
                  (Batteries.RBNode.Path.RootOrdered cmp
                    (Batteries.RBNode.Path.right Batteries.RBColor.black a x parent))
                  b),
              motive (Batteries.RBNode.Path.right Batteries.RBColor.black a x parent) b hb ⋯ H) →
            motive x x_1 x_2 x_3 x_4