case inr h' =>
  simp at h'
  have : i + 1 - 1 ≤ a.size - 1 := Nat.sub_le_sub_right h _
  simp at this
  have : i = a.size - 1 := Nat.le_antisymm this h'
  simp [back', this]
α : 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]
no goals