intro i hi
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : ¬x ∈ as
⊢ ∀ (i : Nat) (h : i < Array.size as.content), as.content[i] ≠ x
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : ¬x ∈ as
i : Nat
hi : i < Array.size as.content
⊢ as.content[i] ≠ x