simp [Array.isEmpty, Option.isSome_iff_exists, getElem?]
α : Type u_1
as : Array α
⊢ Option.isSome as[0]? = true ↔ ¬isEmpty as = true
α : Type u_1
as : Array α
⊢ (∃ a, (if h : 0 < size as then some as[0] else none) = some a) ↔ ¬size as = 0