induction l with
| nil => exact .nil
| cons b l IH =>
  have ⟨hhead, (htail : l.Nodup)⟩ := pairwise_cons.mp hnodup
  dsimp [List.erase]
  match b == a with
  | true => dsimp; exact htail
  | false =>
    dsimp; refine pairwise_cons.mpr <| And.intro ?_ ?_
    . intro _ hb h; cases h
      exact hhead b (List.mem_of_mem_erase hb) rfl
    . exact IH htail
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
l : List α
hnodup : Nodup l
⊢ Nodup (List.erase l a)
no goals