diff --git a/library/collection/List.scala b/library/collection/List.scala
index 8ae15c41da2046e97d67af9def330044ee78bedb..e4924f75e0db19f4bcd168949139cd97e373a2a3 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -5,6 +5,7 @@ package leon.collection
 import leon._
 import leon.lang._
 import leon.annotation._
+import leon.math._
 
 @library
 sealed abstract class List[T] {
@@ -23,12 +24,12 @@ sealed abstract class List[T] {
     case Cons(h, t) if h == v => true
     case Cons(_, t) => t.contains(v)
     case Nil() => false
-  }) ensuring { res => res == (content contains v) }
+  }) ensuring { _ == (content contains v) }
 
   def ++(that: List[T]): List[T] = (this match {
     case Nil() => that
     case Cons(x, xs) => Cons(x, xs ++ that)
-  }) ensuring { res => 
+  }) ensuring { res =>
     (res.content == this.content ++ that.content) && 
     (res.size == this.size + that.size)
   }
@@ -50,7 +51,7 @@ sealed abstract class List[T] {
     if (index == BigInt(0)) {
       head
     } else {
-       tail(index-1)
+      tail(index-1)
     }
   }
 
@@ -78,11 +79,13 @@ sealed abstract class List[T] {
       } else {
         Cons(h, t.take(i-1))
       }
-  }} ensuring { _.size == (
-    if      (i <= 0)         BigInt(0)
-    else if (i >= this.size) this.size 
-    else                     i
-  )}
+  }} ensuring { res =>
+    res.content.subsetOf(this.content) && (res.size == (
+      if      (i <= 0)         BigInt(0)
+      else if (i >= this.size) this.size
+      else                     i
+    ))
+  }
 
   def drop(i: BigInt): List[T] = { (this, i) match {
     case (Nil(), _) => Nil[T]()
@@ -92,11 +95,13 @@ sealed abstract class List[T] {
       } else {
         t.drop(i-1)
       }
-  }} ensuring { _.size == (
-    if      (i <= 0)         this.size
-    else if (i >= this.size) BigInt(0)
-    else                     this.size - i
-  )}
+  }} ensuring { res =>
+    res.content.subsetOf(this.content) && (res.size == (
+      if      (i <= 0)         this.size
+      else if (i >= this.size) BigInt(0)
+      else                     this.size - i
+    ))
+  }
 
   def slice(from: BigInt, to: BigInt): List[T] = {
     require(0 <= from && from <= to && to <= size)
@@ -159,7 +164,10 @@ sealed abstract class List[T] {
       }
     case Nil() =>
       Nil[T]()
-  }} ensuring { _.content == this.content -- Set(e) }
+  }} ensuring { res =>
+    res.size <= this.size &&
+    res.content == this.content -- Set(e)
+  }
 
   def --(that: List[T]): List[T] = { this match {
     case Cons(h, t) =>
@@ -170,7 +178,10 @@ sealed abstract class List[T] {
       }
     case Nil() =>
       Nil[T]()
-  }} ensuring { _.content == this.content -- that.content }
+  }} ensuring { res =>
+    res.size <= this.size &&
+    res.content == this.content -- that.content
+  }
 
   def &(that: List[T]): List[T] = { this match {
     case Cons(h, t) =>
@@ -181,15 +192,24 @@ sealed abstract class List[T] {
       }
     case Nil() =>
       Nil[T]()
-  }} ensuring { _.content == (this.content & that.content) }
+  }} ensuring { res =>
+    res.size <= this.size &&
+    res.content == (this.content & that.content)
+  }
 
-  def pad(s: BigInt, e: T): List[T] = (this, s) match {
+  def padTo(s: BigInt, e: T): List[T] = { (this, s) match {
     case (_, s) if s <= 0 =>
       this
     case (Nil(), s) =>
-      Cons(e, Nil().pad(s-1, e))
+      Cons(e, Nil().padTo(s-1, e))
     case (Cons(h, t), s) =>
-      Cons(h, t.pad(s-1, e))
+      Cons(h, t.padTo(s-1, e))
+  }} ensuring { res =>
+    if (s <= this.size)
+      res == this
+    else
+      res.size == s &&
+      res.content == this.content ++ Set(e)
   }
 
   def find(e: T): Option[BigInt] = { this match {
@@ -203,16 +223,20 @@ sealed abstract class List[T] {
           case Some(i) => Some(i+1)
         }
       }
-  }} ensuring { (res: Option[BigInt]) => res.isDefined == this.contains(e) }
+  }} ensuring { _.isDefined == this.contains(e) }
 
-  def init: List[T] = (this match {
-    case Cons(h, Nil()) =>
-      Nil[T]()
-    case Cons(h, t) =>
-      Cons[T](h, t.init)
-    case Nil() =>
-      Nil[T]()
-  }) ensuring ( (r: List[T]) => ((r.size < this.size) || (this.size == BigInt(0))) )
+  def init: List[T] = {
+    require(!isEmpty)
+    (this match {
+      case Cons(h, Nil()) =>
+        Nil[T]()
+      case Cons(h, t) =>
+        Cons[T](h, t.init)
+    })
+  } ensuring ( (r: List[T]) =>
+    r.size == this.size - 1 &&
+    r.content.subsetOf(this.content)
+  )
 
   def last: T = {
     require(!isEmpty)
@@ -220,21 +244,21 @@ sealed abstract class List[T] {
       case Cons(h, Nil()) => h
       case Cons(_, t) => t.last
     }
-  }
+  } ensuring { this.contains _ }
 
-  def lastOption: Option[T] = this match {
+  def lastOption: Option[T] = { this match {
     case Cons(h, t) =>
       t.lastOption.orElse(Some(h))
     case Nil() =>
       None()
-  }
+  }} ensuring { _.isDefined != this.isEmpty }
 
-  def firstOption: Option[T] = this match {
+  def firstOption: Option[T] = { this match {
     case Cons(h, t) =>
       Some(h)
     case Nil() =>
       None()
-  }
+  }} ensuring { _.isDefined != this.isEmpty }
 
   def unique: List[T] = this match {
     case Nil() => Nil()
@@ -256,17 +280,6 @@ sealed abstract class List[T] {
       Cons(Nil(), Nil())
   }
 
-  def count(e: T): BigInt = this match {
-    case Cons(h, t) =>
-      if (h == e) {
-        1 + t.count(e)
-      } else {
-        t.count(e)
-      }
-    case Nil() =>
-      BigInt(0)
-  }
-
   def evenSplit: (List[T], List[T]) = {
     val c = size/2
     (take(c), drop(c))
@@ -285,6 +298,9 @@ sealed abstract class List[T] {
           l
       }
     }
+  } ensuring { res =>
+    res.size == this.size + l.size &&
+    res.content == this.content ++ l.content
   }
 
   def replaceAt(pos: BigInt, l: List[T]): List[T] = {
@@ -300,15 +316,20 @@ sealed abstract class List[T] {
           l
       }
     }
+  } ensuring { res =>
+    res.content.subsetOf(l.content ++ this.content)
   }
 
   def rotate(s: BigInt): List[T] = {
     if (s < 0) {
-      rotate(size+s)
+      rotate(size + s)
+    } else if (s > size) {
+      rotate(s - size)
     } else {
-      val s2 = s % size
-      drop(s2) ++ take(s2)
+      drop(s) ++ take(s)
     }
+  } ensuring { res =>
+    res.size == this.size
   }
 
   def isEmpty = this match { 
@@ -320,7 +341,7 @@ sealed abstract class List[T] {
   def map[R](f: T => R): List[R] = { this match {
     case Nil() => Nil[R]()
     case Cons(h, t) => f(h) :: t.map(f)
-  }} ensuring { _.size == this.size}
+  }} ensuring { _.size == this.size }
 
   def foldLeft[R](z: R)(f: (R,T) => R): R = this match {
     case Nil() => z
@@ -332,10 +353,10 @@ sealed abstract class List[T] {
     case Cons(h, t) => f(h, t.foldRight(z)(f))
   }
  
-  def scanLeft[R](z: R)(f: (R,T) => R): List[R] = this match {
+  def scanLeft[R](z: R)(f: (R,T) => R): List[R] = { this match {
     case Nil() => z :: Nil()
     case Cons(h,t) => z :: t.scanLeft(f(z,h))(f)
-  }
+  }} ensuring { !_.isEmpty }
 
   def scanRight[R](z: R)(f: (T,R) => R): List[R] = { this match {
     case Nil() => z :: Nil[R]()
@@ -351,7 +372,29 @@ sealed abstract class List[T] {
     case Nil() => Nil[T]()
     case Cons(h, t) if p(h) => Cons(h, t.filter(p))
     case Cons(_, t) => t.filter(p)
-  }} ensuring { res => res.size <= this.size && res.forall(p) }
+  }} ensuring { res =>
+    res.size <= this.size &&
+    res.content.subsetOf(this.content) &&
+    res.forall(p)
+  }
+
+  def filterNot(p: T => Boolean): List[T] =
+    filter(!p(_)) ensuring { res =>
+      res.size <= this.size &&
+      res.content.subsetOf(this.content) &&
+      res.forall(!p(_))
+    }
+
+  def partition(p: T => Boolean): (List[T], List[T]) = { this match {
+    case Nil() => (Nil[T](), Nil[T]())
+    case Cons(h, t) =>
+      val (l1, l2) = t.partition(p)
+      if (p(h)) (h :: l1, l2)
+      else      (l1, h :: l2)
+  }} ensuring { res =>
+    res._1 == filter(p) &&
+    res._2 == filterNot(p)
+  }
 
   // In case we implement for-comprehensions
   def withFilter(p: T => Boolean) = filter(p)
@@ -369,20 +412,41 @@ sealed abstract class List[T] {
     case Cons(_, t) => t.find(p)
   }} ensuring { _.isDefined == exists(p) }
 
-  // FIXME: I keep getting these weird type errors
-  //def groupBy[R](f: T => R): Map[R, List[T]] = this match {
-  //  case Nil() => Map.empty[R, List[T]]
-  //  case Cons(h, t) =>
-  //    val key: R = f(h)
-  //    val rest: Map[R, List[T]] = t.groupBy(f)
-  //    val prev: List[T] = if (rest isDefinedAt key) rest(key) else Nil[T]()
-  //    (rest ++ Map((key, h :: prev))) : Map[R, List[T]]
-  //}
+  def groupBy[R](f: T => R): Map[R, List[T]] = this match {
+    case Nil() => Map.empty[R, List[T]]
+    case Cons(h, t) =>
+      val key: R = f(h)
+      val rest: Map[R, List[T]] = t.groupBy(f)
+      val prev: List[T] = if (rest isDefinedAt key) rest(key) else Nil[T]()
+      (rest ++ Map((key, h :: prev))) : Map[R, List[T]]
+  }
 
   def takeWhile(p: T => Boolean): List[T] = { this match {
     case Cons(h,t) if p(h) => Cons(h, t.takeWhile(p))
     case _ => Nil[T]()
-  }} ensuring { _ forall p }
+  }} ensuring { res =>
+    (res forall p) &&
+    (res.size <= this.size) &&
+    (res.content subsetOf this.content)
+  }
+
+  def dropWhile(p: T => Boolean): List[T] = { this match {
+    case Cons(h,t) if p(h) => t.dropWhile(p)
+    case _ => this
+  }} ensuring { res =>
+    (res.size <= this.size) &&
+    (res.content subsetOf this.content) &&
+    (res.isEmpty || !p(res.head))
+  }
+
+  def count(p: T => Boolean): BigInt = { this match {
+    case Nil() => BigInt(0)
+    case Cons(h, t) =>
+      (if (p(h)) BigInt(1) else BigInt(0)) + t.count(p)
+  }} ensuring {
+    _ == this.filter(p).size
+  }
+
 }
 
 @ignore
@@ -506,7 +570,19 @@ object ListSpecs {
   //  }) &&
   //  ((l1 ++ l2).reverse == (l2.reverse ++ l1.reverse))
   //}.holds
-  
+
+  //def associative[T,U](l1: List[T], l2: List[T], f: List[T] => U, op: (U,U) => U) = {
+  //  f(l1 ++ l2) == op(f(l1), f(l2))
+  //}
+  //
+  //def existsAssoc[T](l1: List[T], l2: List[T], p: T => Boolean) = {
+  //  associative[T, Boolean](l1, l2, _.exists(p), _ || _ )
+  //}.holds
+  //
+  //def forallAssoc[T](l1: List[T], l2: List[T], p: T => Boolean) = {
+  //  associative[T, Boolean](l1, l2, _.exists(p), _ && _ )
+  //}.holds
+
   //@induct
   //def folds[T,R](l : List[T], z : R, f : (R,T) => R) = {
   //  { l match {
@@ -522,7 +598,7 @@ object ListSpecs {
   //def scanVsFoldLeft[A,B](l : List[A], z: B, f: (B,A) => B): Boolean = {
   //  l.scanLeft(z)(f).last == l.foldLeft(z)(f)
   //}.holds
-  
+
   @induct
   def scanVsFoldRight[A,B](l: List[A], z: B, f: (A,B) => B): Boolean = {
     l.scanRight(z)(f).head == l.foldRight(z)(f)