. rw [Nat.add_assoc, Nat.add_comm _ 1, ← Nat.add_assoc]
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 p l + countP q l + 1 = countP p l + 1 + countP q l
no goals