no goals
α : Type u
β : Type v
l l₁✝ l₂✝ : List α
r : α → α → Prop
a✝ b a : α
l₁ l₂ : List α
⊢ Nodup (l₁ ++ a :: l₂) ↔ Nodup (a :: (l₁ ++ l₂))
simp only [nodup_append, not_or, and_left_comm, and_assoc, nodup_cons, mem_append,
  disjoint_cons_right]