Theorem: List.count_nil (One.lean)

State before:
α : Type u_1
inst✝ : BEq α
a : α
⊢ count a [] = 0
Tactic:
unfold count
State after:
α : Type u_1
inst✝ : BEq α
a : α
⊢ countp (fun x => x == a) [] = 0

State before:
α : Type u_1
inst✝ : BEq α
a : α
⊢ countp (fun x => x == a) [] = 0
Tactic:
apply countp_nil
State after:
no goals