rwa [Array.getElem_eq_data_get]
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
i : Nat
hi : i < Array.size as.content
hx : ¬List.get as.content.data { val := i, isLt := hi } = x
⊢ as.content[i] ≠ x
no goals