∀ {α : Type u_1} (motive : Batteries.RBNode α → Prop) (x : Batteries.RBNode α),
  (∀ (a : Unit), motive Batteries.RBNode.nil) →
    (∀ (c : Batteries.RBColor) (a : Batteries.RBNode α) (v : α) (b : Batteries.RBNode α),
        motive (Batteries.RBNode.node c a v b)) →
      motive x