cases hneg
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
hneg : x ∈ a.fst :: map Prod.fst as
⊢ False
case head
α : Type u_1
inst✝ : DecidableEq α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = a.fst
hout : ¬a.fst ∈ map Prod.fst as
⊢ False

case tail
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
a✝ : Mem x (map Prod.fst as)
⊢ False