have : a.size - 1 < a.size := Nat.sub_lt_of_pos_le (by decide) this
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this : 0 < 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.pop.size < a.size