α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
l : List α
⊢ a = b → False
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
l : List α
⊢ count a (b :: l) = count a l
simp [count_cons']
no goals
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
l : List α
⊢ a = b → False
exact h