{α : Type u_1} →
  (motive : Batteries.RBNode α → Batteries.RBNode α → Sort u_2) →
    (x x_1 : Batteries.RBNode α) →
      ((x : Batteries.RBNode α) → motive Batteries.RBNode.nil x) →
        ((x : Batteries.RBNode α) → (x = Batteries.RBNode.nil → False) → motive x Batteries.RBNode.nil) →
          ((a : Batteries.RBNode α) →
              (x : α) →
                (b c : Batteries.RBNode α) →
                  (y : α) →
                    (d : Batteries.RBNode α) →
                      motive (Batteries.RBNode.node Batteries.RBColor.red a x b)
                        (Batteries.RBNode.node Batteries.RBColor.red c y d)) →
            ((a : Batteries.RBNode α) →
                (x : α) →
                  (b c : Batteries.RBNode α) →
                    (y : α) →
                      (d : Batteries.RBNode α) →
                        motive (Batteries.RBNode.node Batteries.RBColor.black a x b)
                          (Batteries.RBNode.node Batteries.RBColor.black c y d)) →
              ((l : Batteries.RBNode α) →
                  (v : α) →
                    (r b : Batteries.RBNode α) →
                      (x : α) →
                        (c : Batteries.RBNode α) →
                          motive (Batteries.RBNode.node Batteries.RBColor.black l v r)
                            (Batteries.RBNode.node Batteries.RBColor.red b x c)) →
                ((a : Batteries.RBNode α) →
                    (x : α) →
                      (b l : Batteries.RBNode α) →
                        (v : α) →
                          (r : Batteries.RBNode α) →
                            motive (Batteries.RBNode.node Batteries.RBColor.red a x b)
                              (Batteries.RBNode.node Batteries.RBColor.black l v r)) →
                  motive x x_1