diff --git a/library/leon/collection/List.scala b/library/leon/collection/List.scala
index a7bf09527b530d64e1f29811f7074ef764ae694e..74cd509d042a150a4cce9c3bf71689678449f9d8 100644
--- a/library/leon/collection/List.scala
+++ b/library/leon/collection/List.scala
@@ -901,5 +901,10 @@ object ListSpecs {
         if (i < l1.size) l1.insertAt(i, y) ++ l2
         else l1 ++ l2.insertAt(i - l1.size, y)))
   }.holds
-
+  
+  /** A way to apply the forall axiom */
+  def applyForAll[T](l: List[T], i: BigInt, p: T => Boolean): Boolean = {
+    require(i >= 0 && i < l.length && l.forall(p))
+    p(l(i))
+  } holds
 }
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index ae2774a7e33e3da3b9563860880a395ee65a58bd..eff7346555b3a4a11127a37ea0adb9c6c1549e26 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1837,6 +1837,7 @@ object ExprOps extends GenTreeOps[Expr] {
   def hasSpec(e: Expr): Boolean = exists {
     case Require(_, _) => true
     case Ensuring(_, _) => true
+    case Let(i, e, b) => hasSpec(b)
     case _ => false
   } (e)
 
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 5da34c789a74a277827612a5a2fd43cbe65b9199..7567132ea11e717ffec71cdfe203f758dba9a776 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -400,7 +400,7 @@ object Expressions {
     * @param cases The cases to compare against
     */
   case class Passes(in: Expr, out: Expr, cases: Seq[MatchCase]) extends Expr {
-    require(cases.nonEmpty)
+    //require(cases.nonEmpty)
 
     val getType = leastUpperBound(cases.map(_.rhs.getType)) match {
       case None => Untyped