split
α : Type u_1
as : Array α
h : ¬size as = 0
⊢ ∃ a, (if h : 0 < size as then some as[0] else none) = some a
case inl
α : Type u_1
as : Array α
h : ¬size as = 0
h✝ : 0 < size as
⊢ ∃ a, some as[0] = some a

case inr
α : Type u_1
as : Array α
h : ¬size as = 0
h✝ : ¬0 < size as
⊢ ∃ a, False