intros _ hal h
α : Type u
β : Type v
a : α
l : List α
ha : ¬a ∈ l
hnodup : Nodup l
⊢ ∀ (a' : α), a' ∈ l → a ≠ a'
α : Type u
β : Type v
a : α
l : List α
ha : ¬a ∈ l
hnodup : Nodup l
a'✝ : α
hal : a'✝ ∈ l
h : a = a'✝
⊢ False