diff --git a/library/collection/List.scala b/library/collection/List.scala
index ef22189d776ac2b4e0f36a629c96f4cc79e4d8d7..436886cca2d4c7893092730151c3648f24569b24 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -310,6 +310,21 @@ sealed abstract class List[T] {
     (take(c), drop(c))
   }
 
+  def splitAtIndex(index: BigInt) : (List[T], List[T]) = { this match {
+    case Nil() => (Nil[T](), Nil[T]())
+    case Cons(h, rest) => {
+      if (index <= BigInt(0)) {
+        (Nil[T](), this)
+      } else {
+        val (left,right) = rest.splitAtIndex(index - 1)
+        (Cons[T](h,left), right)
+      }
+    }
+  }} ensuring { (res:(List[T],List[T])) =>
+    res._1 ++ res._2 == this &&
+    res._1 == take(index) && res._2 == drop(index)
+  }
+
   def updated(i: BigInt, y: T): List[T] = {
     require(0 <= i && i < this.size)
     this match {
diff --git a/testcases/verification/sorting/MergeSort.scala b/testcases/verification/list-algorithms/BasicMergeSort.scala
similarity index 100%
rename from testcases/verification/sorting/MergeSort.scala
rename to testcases/verification/list-algorithms/BasicMergeSort.scala
diff --git a/testcases/verification/list-algorithms/BasicMergeSortPar.scala b/testcases/verification/list-algorithms/BasicMergeSortPar.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e5620482d87cd48dee2fe74f7c2e1bcda5b473df
--- /dev/null
+++ b/testcases/verification/list-algorithms/BasicMergeSortPar.scala
@@ -0,0 +1,27 @@
+import leon.lang._
+import leon.collection._
+import leon.par._
+object MergeSortPar {
+
+  def merge[T](less: (T, T) => Boolean)(xs: List[T], ys: List[T]): List[T] = {
+    (xs, ys) match {
+      case (Nil(), _) => ys
+      case (_, Nil()) => xs
+      case (Cons(x,xtail), Cons(y,ytail)) =>
+        if (less(x, y))
+          x :: merge(less)(xtail, ys)
+        else
+          y :: merge(less)(xs, ytail)
+    }
+  } ensuring { res => res.content == xs.content ++ ys.content &&
+                      res.size == xs.size + ys.size }
+
+  def msort[T](less: (T, T) => Boolean)(l: List[T]): List[T] = {
+    if (l.size <= 1) l
+    else {
+      val (first, second) = l.evenSplit
+      val (s1, s2) = parallel(msort(less)(first), msort(less)(second))
+      merge(less)(s1, s2)
+    }
+  } ensuring { res => res.content == l.content && res.size == l.size }
+}