exact Eq.symm <| Bool.or_assoc (p b) (x.any p) (p a)
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
p : α → Bool
b : α
x : Array α
IH : any (push x a) p 0 (size (push x a)) = (any x p 0 (size x) || p a)
⊢ (p b || (any x p 0 (size x) || p a)) = (p b || any x p 0 (size x) || p a)
no goals