dsimp [List.Nodup]
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)
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ∧ Nodup x ↔ List.Pairwise (fun x x_1 => ¬x = x_1) (a :: x.data)