cases Decidable.em (a.1 = x) with
| inl heq =>
  apply absurd h
  apply not_not
  simp only [map, heq]
  apply List.Mem.head
| inr hneq =>
  simp only [hneq, ite_false, map]
  apply congrArg
  apply ih
  . intros hneg
    apply h
    apply List.Mem.tail _ hneg
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
⊢ map Prod.fst (if a.fst = x then (a.fst, a.snd + 1) :: as else (a.fst, a.snd) :: incrCounts as x) =
    a.fst :: map Prod.fst as ++ [x]
no goals