induction l with
| nil => exact .nil
| cons a l IH =>
  specialize IH nodup.tail
  dsimp [List.filter]
  cases p a <;> dsimp
  . exact IH
  . refine nodup_cons_of_notmem_nodup _ ?_ IH
    intro ha
    exact nodup.head <| l.filter_sublist.subset ha
α : Type u
β : Type v
l : List α
nodup : Nodup l
p : α → Bool
⊢ Nodup (List.filter p l)
no goals