induction x using cons_induction with
| empty =>
  simp only [nodup_empty, not_mem_empty, not_false_eq_true, and_self, iff_true]
  exact nodup_singleton a
| cons b x IH =>
  simp only [push_cons_eq_cons_push, nodup_cons, mem_push, mem_cons, IH]
  simp only [not_or, and_assoc]
  apply and_congr_right'
  simp only [← and_assoc]; rewrite[and_comm (a:=x.Nodup)]
  apply and_congr_left'; apply and_congr_left'
  exact ⟨Ne.symm, Ne.symm⟩
α : Type u
inst✝ : DecidableEq α
x : Array α
a : α
⊢ Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
no goals