have : 0 < a.size := zero_lt_size_of_not_empty hemp
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ a.pop.push (a.back' hemp) = a
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < a.size
⊢ a.pop.push (a.back' hemp) = a