simp only [nodup_empty, not_mem_empty, not_false_eq_true, and_self, iff_true]
case empty
α : Type u
inst✝ : DecidableEq α
a : α
⊢ Nodup (push #[] a) ↔ Nodup #[] ∧ ¬a ∈ #[]
case empty
α : Type u
inst✝ : DecidableEq α
a : α
⊢ Nodup (push #[] a)