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