induction x using cons_induction with
| empty => rfl
| cons a x IH =>
  conv => lhs; simp only [any_cons]
  conv => rhs; simp only [data_cons, List.any_cons]
  rw [IH]
α : Type u
m : Type → Type v
inst✝ : Monad m
x : Array α
p : α → Bool
⊢ any x p 0 (size x) = List.any x.data p
no goals