intro h
case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
hnodup : Nodup []
⊢ ¬a ∈ List.erase [] a
case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
hnodup : Nodup []
h : a ∈ List.erase [] a
⊢ False