have h := ((List.Nodup.mem_erase_iff h).mp H).left
α : Type u_1
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : l.Nodup
H : a ∈ l.erase a
⊢ False
α : Type u_1
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h✝ : l.Nodup
H : a ∈ l.erase a
h : (a != a) = true
⊢ False