diff --git a/leon.out/Conqueue-edited.scala b/leon.out/Conqueue-edited.scala
index 10ebf9aaa0eabc5adf6e0c57d533680b43c37a6e..3e9ba4df1a1526d86e5c46c10131cd230cd32121 100644
--- a/leon.out/Conqueue-edited.scala
+++ b/leon.out/Conqueue-edited.scala
@@ -7,6 +7,8 @@ import leon.lang.synthesis._
 import ConcTrees._
 import ConQ._
 import Conqueue._
+import conc.Conqueue
+import conc.ConcTrees
 
 object ConcTrees {
   abstract class Conc[T] { 
diff --git a/library/annotation/package.scala b/library/annotation/package.scala
index c65c16926e6c16072d856b4487271fdc50dc3651..a473add8225ce35d251051ba4c1f40a220562ce2 100644
--- a/library/annotation/package.scala
+++ b/library/annotation/package.scala
@@ -10,6 +10,8 @@ package object annotation {
   @ignore
   class induct     extends StaticAnnotation
   @ignore
+  class traceInduct     extends StaticAnnotation
+  @ignore
   class ignore     extends StaticAnnotation
   @ignore
   class extern     extends StaticAnnotation
diff --git a/library/lazy/package.scala b/library/lazy/package.scala
index 2a6a29cf2f11c4075db553f17047543d993d525a..f64cec65445e7ff5c5c6c6783f5fb7938d2c52ea 100644
--- a/library/lazy/package.scala
+++ b/library/lazy/package.scala
@@ -5,6 +5,7 @@ package leon.lazyeval
 import leon.annotation._
 import leon.lang._
 import scala.language.implicitConversions
+import scala.annotation.StaticAnnotation
 
 @library
 object $ {
@@ -48,6 +49,16 @@ object $ {
 
   @inline
   implicit def toWithState[T](x: T) = new WithState(x)
+
+  /**
+   * annotations for monotonicity proofs.
+   * Note implemented as of now.
+   * Let foo be the method that has the annotation.
+   * The given name `methodname` should have the following form:
+   *  m(arg1, ..., argn, substate-Set1,..., substate-Setn, superstate-Set1, ..., superstate-Setn)
+   */
+  @ignore
+  class monoproof(methodname: String) extends StaticAnnotation
 }
 
 @library
diff --git a/src/main/scala/leon/verification/TraceInductionTactic.scala b/src/main/scala/leon/verification/TraceInductionTactic.scala
new file mode 100644
index 0000000000000000000000000000000000000000..138148231874737a50f1cb54a3fdbee8cf422af4
--- /dev/null
+++ b/src/main/scala/leon/verification/TraceInductionTactic.scala
@@ -0,0 +1,38 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package verification
+
+import purescala.Definitions._
+import purescala.Expressions._
+
+/**
+ * This tactic applies only to non-recursive functions.
+ * Inducts over the recursive calls of the first recursive procedure, in the body of `funDef`
+ */
+class TraceInductionTactic(vctx: VerificationContext) extends Tactic(vctx) {
+  val description : String =
+
+  implicit protected val ctx = vctx.context
+
+  def generateVCs(fd: FunDef): Seq[VC] = {
+    generatePostconditions(fd) ++
+    generatePreconditions(fd) ++
+    generateCorrectnessConditions(fd)
+  }
+
+  def generatePostconditions(function: FunDef): Seq[VC]
+  def generatePreconditions(function: FunDef): Seq[VC]
+  def generateCorrectnessConditions(function: FunDef): Seq[VC]
+
+  protected def sizeLimit(s: String, limit: Int) = {
+    require(limit > 3)
+    // Crop the call to display it properly
+    val res = s.takeWhile(_ != '\n').take(limit)
+    if (res == s) {
+      res
+    } else {
+      res + " ..."
+    }
+  }
+}
diff --git a/testcases/lazy-datastructures/LazyMegeSort.scala b/testcases/lazy-datastructures/LazyMegeSort.scala
index 503dc8cb5fc8c289ec9cf47b1bf803c5446fd1d5..9ddca941efad67fe2434879fd11c2be0a97ff525 100644
--- a/testcases/lazy-datastructures/LazyMegeSort.scala
+++ b/testcases/lazy-datastructures/LazyMegeSort.scala
@@ -54,9 +54,7 @@ object MergeSort {
   } ensuring (res => res._2.size == l.size - n && res._1.size == n && stack <= 25 * l.size - 1)
 
   /*
-   * Note: merge is not recursive due to closures.
-   * However, concretizing merge may invoke merge or msort recursively.
-   * So proving standalone bound for merge requires preconditions.
+   * Proving standalone bound for merge requires preconditions.
    */
   def merge(a: $[LList], b: $[LList]): LList = (b.value match {
     case SNil() => a.value
diff --git a/testcases/lazy-datastructures/FibonacciMemoized.scala b/testcases/lazy-datastructures/Unproved/FibonacciMemoized.scala
similarity index 95%
rename from testcases/lazy-datastructures/FibonacciMemoized.scala
rename to testcases/lazy-datastructures/Unproved/FibonacciMemoized.scala
index 34490f82f797c22aeaea3638c45d60ebe495a10b..385c1498feb848fe4905eea2b859142c572fc009 100644
--- a/testcases/lazy-datastructures/FibonacciMemoized.scala
+++ b/testcases/lazy-datastructures/Unproved/FibonacciMemoized.scala
@@ -1,9 +1,10 @@
-package lazybenchmarks
+package Unproved
 
 import leon.lazyeval._
 import leon.lang._
 import leon.annotation._
 import leon.instrumentation._
+import scala.math.BigInt.int2bigInt
 //import leon.invariant._
 
 object FibMem {
diff --git a/testcases/lazy-datastructures/HammingProblem.scala b/testcases/lazy-datastructures/Unproved/HammingProblem.scala
similarity index 97%
rename from testcases/lazy-datastructures/HammingProblem.scala
rename to testcases/lazy-datastructures/Unproved/HammingProblem.scala
index 18ee1207a9a5669bbbcbe4cc3c67c7341c180d2f..79acc3ba6bd132a86efed9cc8c74a70a2dbe6a46 100644
--- a/testcases/lazy-datastructures/HammingProblem.scala
+++ b/testcases/lazy-datastructures/Unproved/HammingProblem.scala
@@ -1,9 +1,9 @@
-package lazybenchmarks
-
 import leon.lazyeval._
 import leon.lang._
 import leon.annotation._
 import leon.instrumentation._
+import leon.lazyeval.$.eagerToLazy
+import scala.math.BigInt.int2bigInt
 //import leon.invariant._
 
 /**
diff --git a/testcases/lazy-datastructures/ImplicitQueue.scala b/testcases/lazy-datastructures/Unproved/ImplicitQueue.scala
similarity index 99%
rename from testcases/lazy-datastructures/ImplicitQueue.scala
rename to testcases/lazy-datastructures/Unproved/ImplicitQueue.scala
index b69988cd5c20ab164c3d0631854716ddb7708f69..61f6302a14b970ba5a29de9786619528ebc33540 100644
--- a/testcases/lazy-datastructures/ImplicitQueue.scala
+++ b/testcases/lazy-datastructures/Unproved/ImplicitQueue.scala
@@ -3,6 +3,7 @@ import leon.lazyeval.$._
 import leon.lang._
 import leon.annotation._
 import leon.instrumentation._
+import scala.math.BigInt.int2bigInt
 
 /**
  * This is an version of the implicit recursive slowdwon queues of
diff --git a/testcases/lazy-datastructures/ConcTrees.scala b/testcases/lazy-datastructures/conc/ConcTrees.scala
similarity index 100%
rename from testcases/lazy-datastructures/ConcTrees.scala
rename to testcases/lazy-datastructures/conc/ConcTrees.scala
diff --git a/testcases/lazy-datastructures/Conqueue.scala b/testcases/lazy-datastructures/conc/Conqueue.scala
similarity index 99%
rename from testcases/lazy-datastructures/Conqueue.scala
rename to testcases/lazy-datastructures/conc/Conqueue.scala
index 7579f6dfe45764acc05246e4e5f45c5b33c134ff..80d77d21de300f6b0b2bd71f1ec6aa1e777058c3 100644
--- a/testcases/lazy-datastructures/Conqueue.scala
+++ b/testcases/lazy-datastructures/conc/Conqueue.scala
@@ -1,4 +1,4 @@
-package lazybenchmarks
+package conc
 
 import leon.lazyeval._
 import leon.lang._
@@ -7,6 +7,9 @@ import leon.annotation._
 import leon.instrumentation._
 import leon.lazyeval.$._
 
+import ConcTrees._
+import scala.math.BigInt.int2bigInt
+
 object ConcTrees {
 
   sealed abstract class Conc[T] {
@@ -30,8 +33,6 @@ object ConcTrees {
   case class Single[T](x: T) extends Conc[T]
   case class CC[T](left: Conc[T], right: Conc[T]) extends Conc[T]
 }
-
-import ConcTrees._
 object Conqueue {
 
   sealed abstract class ConQ[T] {