induction x using cons_induction with
| empty =>
  simp only [push_empty_eq_cons, any_cons, any_empty, Bool.or_false, Bool.false_or]
| cons b x IH =>
  simp only [push_cons_eq_cons_push, any_cons, IH]
  exact Eq.symm <| Bool.or_assoc (p b) (x.any p) (p a)
α : Type u
m : Type → Type v
inst✝ : Monad m
x : Array α
a : α
p : α → Bool
⊢ any (push x a) p 0 (size (push x a)) = (any x p 0 (size x) || p a)
no goals