rw [←as.get_eq_getElem ⟨i, get_pop.aux as hi⟩]
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ as.pop[i] = as[i]
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ as.pop[i] = as.get ⟨i, ⋯⟩