exact ⟨nodup.head, h a <| l.mem_cons_self a⟩
case cons
α : Type u
β : Type v
l' : List α
nodup' : Nodup l'
a : α
l : List α
nodup : Nodup (a :: l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬a_1 ∈ l'
IH : Nodup (l ++ l')
⊢ ¬a ∈ l ∧ ¬a ∈ l'
no goals