induction l with
| nil => intro h; cases h
| cons b l IH =>
  dsimp [List.erase]
  have ⟨hhead, (htail : l.Nodup)⟩ := pairwise_cons.mp hnodup
  match hba : b == a with
  | true =>
    dsimp; cases of_decide_eq_true hba
    intro ha; exact hhead _ ha rfl
  | false =>
    dsimp; simp [not_or]
    apply And.intro
    . exact Ne.symm <| of_decide_eq_false hba
    . exact IH htail
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
l : List α
hnodup : Nodup l
⊢ ¬a ∈ List.erase l a
no goals