unfold pop
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ as.pop.data.get ⟨i, hi⟩ = as.data.get ⟨i, ⋯⟩
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ { data := as.data.dropLast }.data.get ⟨i, hi⟩ = as.data.get ⟨i, ⋯⟩