simp only [List.nodup_singleton a, true_and, ← mem_iff_mem_data, List.mem_singleton, forall_eq]
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (Nodup as ∧ List.Nodup [a] ∧ ∀ (a_1 : α), a_1 ∈ as.data → ∀ (b : α), b ∈ [a] → a_1 ≠ b) ↔ Nodup as ∧ ¬a ∈ as
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (Nodup as ∧ ∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a) ↔ Nodup as ∧ ¬a ∈ as