rw [contains]
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
⊢ contains as x = true ↔ x ∈ as
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
⊢ Array.contains as.content x = true ↔ x ∈ as