diff --git a/library/leon/lang/package.scala b/library/leon/lang/package.scala
index 8898b5637fdeff14b38610f187217e9f71b9037d..f9173b6fe0cf356c6314fb79ef9bf97641e26e07 100644
--- a/library/leon/lang/package.scala
+++ b/library/leon/lang/package.scala
@@ -13,7 +13,7 @@ package object lang {
     def holds : Boolean = {
       underlying
     } ensuring {
-      _ == true
+      (res: Boolean) => res
     }
     @inline
     def holds(becauseOfThat: Boolean) = {
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 5fb96861de6c6eeab14de3954bd2e05bc9a17612..1723807945564aa64d8dcb492c8d6deaa91db80b 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -177,7 +177,7 @@ trait ASTExtractors {
       }
     }
 
-    /** Matches the `holds` expression at the end of any boolean expression, and return the boolean expression.*/
+    /** Matches the `holds` expression at the end of any boolean expression, and returns the boolean expression.*/
     object ExHoldsExpression {
       def unapply(tree: Select) : Option[Tree] = tree match {
         case Select(
@@ -188,6 +188,33 @@ trait ASTExtractors {
        }
     }
     
+    /** Matches the `holds` expression at the end of any boolean expression with a proof as argument, and returns both of themn.*/
+    object ExHoldsWithProofExpression {
+      def unapply(tree: Apply) : Option[(Tree, Tree)] = tree match {
+        case Apply(Select(Apply(ExSelected("leon", "lang", "package", "BooleanDecorations"), body :: Nil), ExNamed("holds")), proof :: Nil) =>
+          Some((body, proof))
+        case _ => None
+       }
+    }
+    
+    /** Matches the `because` method at the end of any boolean expression, and return the assertion and the cause. If no "because" method, still returns the expression */
+    object ExMaybeBecauseExpressionWrapper {
+      def unapply(tree: Tree) : Some[Tree] = tree match {
+        case Apply(ExSelected("leon", "lang", "package", "because"), body :: Nil) =>
+          unapply(body)
+        case body => Some(body)
+       }
+    }
+    
+    /** Matches the `because` method at the end of any boolean expression, and return the assertion and the cause.*/
+    object ExBecauseExpression {
+      def unapply(tree: Apply) : Option[(Tree, Tree)] = tree match {
+        case Apply(Select(Apply(ExSelected("leon", "proof", "package", "boolean2ProofOps"), body :: Nil), ExNamed("because")), proof :: Nil) =>
+          Some((body, proof))
+        case _ => None
+       }
+    }
+    
     /** Matches the `bigLength` expression at the end of any string expression, and returns the expression.*/
     object ExBigLengthExpression {
       def unapply(tree: Apply) : Option[Tree] = tree match {
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 99ca8aa072982fe75065ca5dbcd1671442092ad8..92829ce8c9d522c98bdc6499ae7a8e5f341df355 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1164,6 +1164,13 @@ trait CodeExtraction extends ASTExtractors {
 
           Ensuring(b, closure)
 
+        case t @ ExHoldsWithProofExpression(body, ExMaybeBecauseExpressionWrapper(proof)) =>
+          val resId = FreshIdentifier("holds", BooleanType).setPos(current.pos)
+          val p = extractTreeOrNoTree(proof)
+          val post = Lambda(Seq(LeonValDef(resId)), And(Seq(p, Variable(resId)))).setPos(current.pos)
+          val b = extractTreeOrNoTree(body)
+          Ensuring(b, post)
+          
         case t @ ExHoldsExpression(body) =>
           val resId = FreshIdentifier("holds", BooleanType).setPos(current.pos)
           val post = Lambda(Seq(LeonValDef(resId)), Variable(resId)).setPos(current.pos)
@@ -1171,7 +1178,15 @@ trait CodeExtraction extends ASTExtractors {
           val b = extractTreeOrNoTree(body)
 
           Ensuring(b, post)
-
+          
+        // If the because statement encompasses a holds statement
+        case t @ ExBecauseExpression(ExHoldsExpression(body), proof) =>
+          val resId = FreshIdentifier("holds", BooleanType).setPos(current.pos)
+          val p = extractTreeOrNoTree(proof)
+          val post = Lambda(Seq(LeonValDef(resId)), And(Seq(p, Variable(resId)))).setPos(current.pos)
+          val b = extractTreeOrNoTree(body)
+          Ensuring(b, post)
+          
         case t @ ExComputesExpression(body, expected) =>
           val b = extractTreeOrNoTree(body).setPos(body.pos)
           val expected_expr = extractTreeOrNoTree(expected).setPos(expected.pos)