simp only [nodup_cons, data_cons]
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ Nodup (cons a x) ↔ List.Nodup (cons a x).data
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ∧ Nodup x ↔ List.Nodup (a :: x.data)