simp [back', Array.mem_def, Array.getElem_eq_data_get]
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ a.back' hemp ∈ a
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ a.data.get ⟨a.size - 1, ⋯⟩ ∈ a.data