simp [Array.pop]
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝ : 0 < a.size
this : a.size - 1 < a.size
⊢ a.pop.size < a.size
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝ : 0 < a.size
this : a.size - 1 < a.size
⊢ a.size - 1 < a.size