rewrite [any_cons]
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ any (cons b x) (fun x => a == x) 0 (size (cons b x)) = true ↔ a = b ∨ a ∈ x
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ (a == b || any x (fun x => a == x) 0 (size x)) = true ↔ a = b ∨ a ∈ x