induction x using cons_induction with
| empty =>
  simp only [not_mem_empty, data_toArray, List.not_mem_nil]
| cons v x IH =>
  rw [mem_cons, data_cons, List.mem_cons, IH]
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ a ∈ x ↔ a ∈ x.data
no goals