rw [←Array.push_pop_eq a hemp]
case isFalse
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
hemp : ¬a.isEmpty = true
⊢ x ∈ a
case isFalse
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
hemp : ¬a.isEmpty = true
⊢ x ∈ a.pop.push (a.back' hemp)