rewrite [mem_iff_mem_val, Array.mem_iff_get]
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ a ∈ x ↔ ∃ i, x[↑i] = a
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i hi, x.val[i] = a) ↔ ∃ i, x[↑i] = a