induction l with
| nil => exact .nil
| cons a l IH =>
  dsimp at h
  apply nodup_cons_of_notmem_nodup
  . intro ha; exact h.head <| List.mem_map_of_mem f ha
  . exact IH h.tail
α : Type u
β : Type v
f : α → β
l : List α
h : Nodup (map f l)
⊢ Nodup l
no goals