cases (Array.mem_push _ _ _).mp mem with
| inl mem => exact mem
| inr eq => exact absurd eq neq
α : Type u_1
a : Array α
x : α
hemp : ¬a.isEmpty = true
mem : x ∈ a.pop.push (a.back' hemp)
neq : x ≠ a.back' hemp
⊢ x ∈ a.pop
no goals