simp only [back'_eq_data_getLast, pop, push, size, getElem_eq_data_get, List.concat_eq_append]
α : Type u
as : Array α
h✝ : size as > 0
l : List α
h : size { data := l } > 0
⊢ push (pop { data := l }) (back' { data := l } h) = { data := l }
α : Type u
as : Array α
h✝ : size as > 0
l : List α
h : size { data := l } > 0
⊢ { data := List.dropLast l ++ [List.getLast l (_ : { data := l }.data ≠ [])] } = { data := l }