specialize IH nodup.tail fun a ha =>
  h a <| mem_cons_of_mem _ ha
case cons
α : Type u
β : Type v
l' : List α
nodup' : Nodup l'
a : α
l : List α
IH : Nodup l → (∀ (a : α), a ∈ l → ¬a ∈ l') → Nodup (l ++ l')
nodup : Nodup (a :: l)
h : ∀ (a_1 : α), a_1 ∈ a :: l → ¬a_1 ∈ l'
⊢ Nodup (a :: l ++ l')
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')
⊢ Nodup (a :: l ++ l')