dsimp at h
case cons
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (map f (a :: l))
⊢ Nodup (a :: l)
case cons
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ Nodup (a :: l)