cases p a <;> cases q a <;> simp only [ite_true, ite_false, Nat.add_zero]
case cons
α : 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 + if (p a || q a) = true then 1 else 0) ≤
    (countP p l + if p a = true then 1 else 0) + (countP q l + if q a = true then 1 else 0)
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

case cons.false.true
α : 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 + 1 ≤ countP p l + (countP q l + 1)

case cons.true.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 + 1 ≤ countP p l + 1 + countP q l

case cons.true.true
α : 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 + 1 ≤ countP p l + 1 + (countP q l + 1)