[STATEMENT]
lemma count_notin[simp]: "x \<notin> set xs \<Longrightarrow> count_list xs x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> count_list xs x = 0
[PROOF STEP]
by(simp add: count_list_0_iff)