induction l with
| nil => exact nodup'
| cons a l IH =>
  specialize IH nodup.tail fun a ha =>
    h a <| mem_cons_of_mem _ ha
  refine nodup_cons_of_notmem_nodup a ?_ IH
  simp only [append_eq, mem_append, not_or]
  exact ⟨nodup.head, h a <| l.mem_cons_self a⟩
α : Type u
β : Type v
l l' : List α
nodup : Nodup l
nodup' : Nodup l'
h : ∀ (a : α), a ∈ l → ¬a ∈ l'
⊢ Nodup (l ++ l')
no goals