∀ {α : Type u_1} (p : α → Prop) (x : Batteries.RBNode α),
  Batteries.RBNode.Any p x =
    match x with
    | Batteries.RBNode.nil => False
    | Batteries.RBNode.node c l v r => p v ∨ Batteries.RBNode.Any p l ∨ Batteries.RBNode.Any p r