∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Array α}
  {f : (i : ℕ) → α → i < xs.size → m β}, Array.toList <$> xs.mapFinIdxM f = xs.toList.mapFinIdxM f