. refine nodup_cons_of_notmem_nodup _ ?_ IH
  intro ha
  exact nodup.head <| l.filter_sublist.subset ha
case cons.true
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (a :: List.filter p l)
no goals