rewrite [Array.push_data]
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ List.Nodup (push as a).data ↔ Nodup as ∧ ¬a ∈ as
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ List.Nodup (as.data ++ [a]) ↔ Nodup as ∧ ¬a ∈ as