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