{α : Type u_1} →
  (motive : Batteries.RBNode α → Sort u_2) →
    (x : Batteries.RBNode α) →
      (Unit → motive Batteries.RBNode.nil) →
        ((c : Batteries.RBColor) →
            (l : Batteries.RBNode α) → (v : α) → (r : Batteries.RBNode α) → motive (Batteries.RBNode.node c l v r)) →
          motive x