simp at h'
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : ¬i < a.pop.size
⊢ 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
⊢ a.back' hemp = a[i]