∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α) (f : (i : ℕ) → α → i < as.size → m β)
  (j : ℕ) (bs : Array β) (x : 0 + j = as.size), Array.mapFinIdxM.map as f 0 j x bs = pure bs