induction l with
| nil => exact (Nat.zero_add 0).symm
| cons a l IH =>
  simp only [countP_cons]
  specialize h a; revert h
  cases p a <;> cases q a <;> simp [IH]
  . rw [Nat.add_assoc]
  . rw [Nat.add_assoc, Nat.add_comm _ 1, ← Nat.add_assoc]
α : Type u
β : Type v
p q : α → Bool
l : List α
h : ∀ (a : α), (p a && q a) = false
⊢ countP (fun a => p a || q a) l = countP p l + countP q l
no goals