dsimp [List.filter]
case cons
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup (List.filter p (a :: l))
case cons
α : Type u
β : Type v
p : α → Bool
a : α
l : List α
nodup : Nodup (a :: l)
IH : Nodup (List.filter p l)
⊢ Nodup
    (match p a with
    | true => a :: List.filter p l
    | false => List.filter p l)