case mp =>
  intro ⟨_, h⟩
  split at h
  case inl hs => exact Nat.not_eq_zero_of_lt hs
  case inr => contradiction
α : Type u_1
as : Array α
⊢ (∃ a, (if h : 0 < size as then some as[0] else none) = some a) → ¬size as = 0
no goals