rw [List.getLast_eq_get]
α : Type u
β : Type v
as : Array α
h : size as > 0
⊢ back' as h = List.getLast as.data (_ : as.data ≠ [])
α : Type u
β : Type v
as : Array α
h : size as > 0
⊢ back' as h =
    List.get as.data { val := List.length as.data - 1, isLt := (_ : List.length as.data - 1 < List.length as.data) }