have : i + 1 - 1 ≤ a.size - 1 := Nat.sub_le_sub_right h _
α : 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
⊢ a.back' hemp = a[i]
α : 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 + 1 - 1 ≤ a.size - 1
⊢ a.back' hemp = a[i]