show (as.push a).data.Nodup ↔ as.Nodup ∧ a ∉ as
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ Nodup (push as a) ↔ Nodup as ∧ ¬a ∈ as
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ List.Nodup (push as a).data ↔ Nodup as ∧ ¬a ∈ as