simp only [incrCounts, map, HAppend.hAppend, Append.append, List.append]
case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
h : ¬x ∈ map Prod.fst []
⊢ map Prod.fst (incrCounts [] x) = map Prod.fst [] ++ [x]
no goals