induction x using cons_induction with
| empty => simp only [nodup_empty, true_iff]; exact .nil
| cons a x IH =>
  simp only [nodup_cons, data_cons]
  dsimp [List.Nodup]; rewrite [List.pairwise_cons, IH]
  apply and_congr_left'
  simp only [← mem_iff_mem_data]
  constructor
  . intro h _ ha hcntr; cases hcntr
    exact h ha
  . intro h ha
    exact h a ha rfl
α : Type u
inst✝ : DecidableEq α
x : Array α
⊢ Nodup x ↔ List.Nodup x.data
no goals