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)
ha : a ∈ List.filter p l
⊢ False
no goals