∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : α → m β) (as : Array α)
  (_x : (_ : ℕ) ×' Array β),
  Array.mapM.map._unary✝ f as _x =
    PSigma.casesOn _x fun i bs =>
      if hlt : i < as.size then do
        let __do_lift ← f as[i]
        Array.mapM.map._unary✝¹ f as ⟨i + 1, bs.push __do_lift⟩
      else pure bs