simp only [getElem_eq_data_get, List.dropLast_eq_take, List.get_take]
α : Type u
as : Array α
i : Nat
hi : i < size (pop as)
⊢ { data := List.dropLast as.data }[i] = as[i]
α : Type u
as : Array α
i : Nat
hi : i < size (pop as)
⊢ List.get (List.take (List.length as.data - 1) as.data)
      { val := i, isLt := (_ : (fun xs i => i < size xs) { data := List.take (List.length as.data - 1) as.data } i) } =
    List.get as.data { val := i, isLt := (_ : i < size as) }