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