refine .cons ?_ hnodup
α : Type u
β : Type v
a : α
l : List α
ha : ¬a ∈ l
hnodup : Nodup l
⊢ Nodup (a :: l)
α : Type u
β : Type v
a : α
l : List α
ha : ¬a ∈ l
hnodup : Nodup l
⊢ ∀ (a' : α), a' ∈ l → a ≠ a'