diff --git a/library/collection/List.scala b/library/collection/List.scala
index 61089979b2aec6afbc6437d2f2e81158bfe67892..1df1115eb34fb89bcd63b8f78e0060c668a9948c 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -229,27 +229,25 @@ sealed abstract class List[T] {
       res.content == this.content ++ Set(e)
   }
 
-  def find(e: T): Option[BigInt] = { this match {
-    case Nil() => None[BigInt]()
+  def indexOf(elem: T): BigInt = { this match {
+    case Nil() => BigInt(-1)
+    case Cons(h, t) if h == elem => BigInt(0)
     case Cons(h, t) =>
-      if (h == e) {
-        Some[BigInt](0)
-      } else {
-        t.find(e) match {
-          case None()  => None[BigInt]()
-          case Some(i) => Some(i+1)
-        }
-      }
-    }} ensuring { res => !res.isDefined || (this.content contains e) }
+      val rec = t.indexOf(elem)
+      if (rec == BigInt(-1)) BigInt(-1)
+      else rec + 1
+  }} ensuring { res =>
+    (res >= 0) == content.contains(elem)
+  }
 
   def init: List[T] = {
     require(!isEmpty)
-    ((this : @unchecked) match {
+    (this : @unchecked) 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)
@@ -284,7 +282,6 @@ sealed abstract class List[T] {
       None[List[T]]()
   }} ensuring { _.isDefined != this.isEmpty }
 
-
   def unique: List[T] = this match {
     case Nil() => Nil()
     case Cons(h, t) =>
diff --git a/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala b/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala
index c122f704823b9ee71f27c7739d14f9a4b406d771..72cf6715d8ab5cfc88e1907aac26238c50980c42 100644
--- a/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala
@@ -16,7 +16,7 @@ class LibraryVerificationSuite extends LeonRegressionSuite {
 
       val ctx = Main.processOptions(Seq("--functions=_")).copy(reporter = new TestSilentReporter())
 
-      val (ctx2, report) = pipeline.run(ctx, Nil)
+      val (_, report) = pipeline.run(ctx, Nil)
 
       assert(report.totalConditions === report.totalValid, "Only "+report.totalValid+" valid out of "+report.totalConditions)
   }