simp only [push_empty_eq_cons, any_cons, any_empty, Bool.or_false, Bool.false_or]
case empty
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
p : α → Bool
⊢ any (push #[] a) p 0 (size (push #[] a)) = (any #[] p 0 (size #[]) || p a)
no goals