rw [IH]
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)
no goals