{α : Type u_1} →
  (motive : Batteries.RBNode α → Sort u_2) →
    (x : Batteries.RBNode α) →
      (Unit → motive Batteries.RBNode.nil) →
        ((a : Batteries.RBNode α) →
            (y : α) → (b : Batteries.RBNode α) → motive (Batteries.RBNode.node Batteries.RBColor.red a y b)) →
          ((a : Batteries.RBNode α) →
              (y : α) → (b : Batteries.RBNode α) → motive (Batteries.RBNode.node Batteries.RBColor.black a y b)) →
            motive x