cases hcntr
case cons.h.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
h : ¬a ∈ x
a'✝ : α
ha : a'✝ ∈ x
hcntr : a = a'✝
⊢ False
case cons.h.mp.refl
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
h : ¬a ∈ x
ha : a ∈ x
⊢ False