have := (Array.isEmpty_iff).mp hemp
case isTrue
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
hemp : a.isEmpty = true
⊢ x ∈ a
case isTrue
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
hemp : a.isEmpty = true
this : a = #[]
⊢ x ∈ a