conv => rhs; simp only [data_cons, List.any_cons]
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → Bool
a : α
x : Array α
IH : any x p 0 (size x) = List.any x.data p
⊢ (p a || any x p 0 (size x)) = List.any (cons a x).data p
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → Bool
a : α
x : Array α
IH : any x p 0 (size x) = List.any x.data p
⊢ (p a || any x p 0 (size x)) = (p a || List.any x.data p)