{α : Type u_1} →
  (motive : Batteries.RBNode α → Option α → Sort u_2) →
    (x : Batteries.RBNode α) →
      (x_1 : Option α) →
        ((ub : Option α) → motive Batteries.RBNode.nil ub) →
          ((c : Batteries.RBColor) →
              (a : Batteries.RBNode α) →
                (y : α) → (b : Batteries.RBNode α) → (ub : Option α) → motive (Batteries.RBNode.node c a y b) ub) →
            motive x x_1