simp only [push_cons_eq_cons_push, any_cons, IH]
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)
⊢ any (push (cons b x) a) p 0 (size (push (cons b x) a)) = (any (cons b x) p 0 (size (cons b x)) || 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)