∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n n' : ℕ} [inst : Monad m] [LawfulMonad m] {xs : Vector α n}
  {ys : Vector α n'} {f : α → m PUnit.{u_1 + 1}},
  forM (xs ++ ys) f = do
    forM xs f
    forM ys f