exact IH
case cons.false.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l ≤ countP p l + countP q l
no goals