. simp [Nat.sub_add_cancel this]
  intro i h _
  rw [Array.get_push]
  split
  case inl h' => rw [Array.getElem_pop]
  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]
case h₂
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ ∀ (i : Nat) (hi₁ : i < (a.pop.push (a.back' hemp)).size) (hi₂ : i < a.size), (a.pop.push (a.back' hemp))[i] = a[i]
no goals