simp [back', this]
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝¹ : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : a.size - 1 ≤ i
this✝ : i ≤ a.size - 1
this : i = a.size - 1
⊢ a.back' hemp = a[i]
no goals