diff --git a/library/lang/package.scala b/library/lang/package.scala
index a80e25cbae866b35fc766d300b40ce46701700e0..a598c251e702d2cf3253a2ebbd4278c24fce22dd 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -7,16 +7,16 @@ import scala.language.implicitConversions
 
 package object lang {
   @ignore
-  sealed class IsValid(val property : Boolean) {
+  implicit class BooleanDecorations(val underlying: Boolean) {
     def holds : Boolean = {
-      assert(property)
-      property
+      assert(underlying)
+      underlying
+    }
+    def ==> (that: Boolean): Boolean = {
+      !underlying || that
     }
   }
 
-  @ignore
-  implicit def any2IsValid(x: Boolean) : IsValid = new IsValid(x)
-
   @ignore
   object InvariantFunction {
     def invariant(x: Boolean): Unit = ()
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 06ab50a2eb19dcf6c8263bd2e647a3e4209ecfca..3d8df24e1c00cd11beda6feec4b80be51229bcf3 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -155,12 +155,31 @@ trait ASTExtractors {
 
     object ExHoldsExpression {
       def unapply(tree: Select) : Option[Tree] = tree match {
-        case Select(Apply(ExSymbol("leon", "lang", "any2IsValid"), realExpr :: Nil), ExNamed("holds")) =>
-            Some(realExpr)
+        case Select(
+          Apply(ExSelected("leon", "lang", "package", "BooleanDecorations"), realExpr :: Nil),
+          ExNamed("holds")
+        ) => Some(realExpr)
         case _ => None
        }
     }
 
+    object ExImplies {
+      def unapply(tree: Apply) : Option[(Tree, Tree)] = tree match {
+        case
+          Apply(
+            Select(
+              Apply(
+                ExSelected("leon", "lang", "package", "BooleanDecorations"),
+                lhs :: Nil
+              ),
+              ExNamed("$eq$eq$greater")
+            ),
+            rhs :: Nil
+          ) => Some((lhs, rhs))
+        case _ => None
+      }
+    }
+
     object ExRequiredExpression {
       /** Extracts the 'require' contract from an expression (only if it's the
        * first call in the block). */
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 3d89df12eeea67d12873af8d17734124d5d5be55..9e209b5d54f7ba0c02b8ee6c78b4757a9187b2f0 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1541,6 +1541,8 @@ trait CodeExtraction extends ASTExtractors {
           CaseClass(CaseClassType(libraryCaseClass(str.pos, "leon.lang.string.String"), Seq()), Seq(charList))
 
 
+        case ExImplies(lhs, rhs) =>
+          Implies(extractTree(lhs), extractTree(rhs)).setPos(current.pos)
 
         case c @ ExCall(rec, sym, tps, args) =>
           val rrec = rec match {