cases decEq a.isEmpty true with
| isTrue hemp =>
  have := (Array.isEmpty_iff).mp hemp
  subst this
  simp at mem
| isFalse hemp =>
  rw [←Array.push_pop_eq a hemp]
  apply (Array.mem_push _ _ _).mpr
  exact Or.inl mem
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
⊢ x ∈ a
no goals