diff --git a/src/main/scala/leon/solvers/templates/LambdaManager.scala b/src/main/scala/leon/solvers/templates/LambdaManager.scala
index e7282e4f18b293bc37dd4f560794f3a18ca4e271..930e2a6911796e73f388655dd830b8ad7c4ae80e 100644
--- a/src/main/scala/leon/solvers/templates/LambdaManager.scala
+++ b/src/main/scala/leon/solvers/templates/LambdaManager.scala
@@ -31,16 +31,29 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) {
     applicationsStack = map :: applicationsStack.tail
   }
 
+  private type FreeMap = Map[TypeTree, Set[T]]
+  private var freeLambdasStack : List[FreeMap] = List(Map.empty.withDefaultValue(Set.empty))
+  private def freeLambdas : FreeMap = freeLambdasStack.head
+  private def freeLambdas_=(map: FreeMap) : Unit = {
+    freeLambdasStack = map :: freeLambdasStack.tail
+  }
+
   def push(): Unit = {
     byIDStack = byID :: byIDStack
     byTypeStack = byType :: byTypeStack
     applicationsStack = applications :: applicationsStack
+    freeLambdasStack = freeLambdas :: freeLambdasStack
   }
 
   def pop(lvl: Int): Unit = {
     byIDStack = byIDStack.drop(lvl)
     byTypeStack = byTypeStack.drop(lvl)
     applicationsStack = applicationsStack.drop(lvl)
+    freeLambdasStack = freeLambdasStack.drop(lvl)
+  }
+
+  def registerFree(lambdas: Seq[(TypeTree, T)]): Unit = {
+    lambdas.foreach(p => freeLambdas += p._1 -> (freeLambdas(p._1) + p._2))
   }
 
   def instantiate(apps: Map[T, Set[App[T]]], lambdas: Map[T, LambdaTemplate[T]]) : (Seq[T], Map[T, Set[TemplateCallInfo[T]]], Map[(T, App[T]), Set[TemplateAppInfo[T]]]) = {
@@ -57,6 +70,9 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) {
     }
 
     for (lambda @ (idT, template) <- lambdas) {
+      // make sure concrete lambdas can't be equal to free lambdas
+      clauses ++= freeLambdas(template.tpe).map(pIdT => encoder.mkNot(encoder.mkEquals(pIdT, idT)))
+
       byID += idT -> template
       byType += template.tpe -> (byType(template.tpe) + (idT -> template))
 
diff --git a/src/main/scala/leon/solvers/templates/Templates.scala b/src/main/scala/leon/solvers/templates/Templates.scala
index c9273660c8b99259e72a959b39029987f1401564..f0c808a99a3266cddc06d501ef5cd0782e99c7de 100644
--- a/src/main/scala/leon/solvers/templates/Templates.scala
+++ b/src/main/scala/leon/solvers/templates/Templates.scala
@@ -229,6 +229,11 @@ class FunctionTemplate[T] private(
 
   private lazy val str : String = stringRepr()
   override def toString : String = str
+
+  override def instantiate(aVar: T, args: Seq[T]): (Seq[T], Map[T, Set[TemplateCallInfo[T]]], Map[(T, App[T]), Set[TemplateAppInfo[T]]]) = {
+    if (!isRealFunDef) lambdaManager.registerFree(tfd.params.map(_.tpe) zip args)
+    super.instantiate(aVar, args)
+  }
 }
 
 object LambdaTemplate {
diff --git a/src/test/resources/regression/verification/purescala/valid/Lists.scala b/src/test/resources/regression/verification/purescala/valid/Lists.scala
deleted file mode 100644
index 45c3adadc610f00fa2cf1494bacfe3a6ef6310a7..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/verification/purescala/valid/Lists.scala
+++ /dev/null
@@ -1,31 +0,0 @@
-import leon.lang._
-
-object Lists {
-  abstract class List
-  case class Cons(head: Int, tail: List) extends List
-  case class Nil() extends List
-
-  def exists(list: List, f: Int => Boolean): Boolean = list match {
-    case Cons(head, tail) => f(head) || exists(tail, f)
-    case Nil() => false
-  }
-
-  def forall(list: List, f: Int => Boolean): Boolean = list match {
-    case Cons(head, tail) => f(head) && forall(tail, f)
-    case Nil() => true
-  }
-
-  def exists_lemma(list: List, f: Int => Boolean): Boolean = {
-    exists(list, f) == !forall(list, x => !f(x))
-  }
-
-  def exists_lemma_induct(list: List, f: Int => Boolean): Boolean = {
-    list match {
-      case Nil() => exists_lemma(list, f)
-      case Cons(head, tail) => exists_lemma(list, f) && exists_lemma_induct(tail, f)
-    }
-  }.holds
-
-}
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/purescala/valid/Lists1.scala b/src/test/resources/regression/verification/purescala/valid/Lists1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..719c3d236009c96aa62986725df47ea20e3a906a
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Lists1.scala
@@ -0,0 +1,30 @@
+import leon.lang._
+import leon.collection._
+import leon.annotation._
+
+object Lists1 {
+
+  def exists[T](list: List[T], f: T => Boolean): Boolean = list match {
+    case Cons(head, tail) => f(head) || exists(tail, f)
+    case Nil() => false
+  }
+
+  def forall[T](list: List[T], f: T => Boolean): Boolean = list match {
+    case Cons(head, tail) => f(head) && forall(tail, f)
+    case Nil() => true
+  }
+
+  def exists_lemma[T](list: List[T], f: T => Boolean): Boolean = {
+    exists(list, f) == !forall(list, (x: T) => !f(x))
+  }
+
+  def exists_lemma_induct[T](list: List[T], f: T => Boolean): Boolean = {
+    list match {
+      case Nil() => exists_lemma(list, f)
+      case Cons(head, tail) => exists_lemma(list, f) && exists_lemma_induct(tail, f)
+    }
+  }.holds 
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/purescala/valid/Sets1.scala b/src/test/resources/regression/verification/purescala/valid/Sets1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e46ba25d05cae4c32c9be1798f535742f41e9bfd
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Sets1.scala
@@ -0,0 +1,23 @@
+import leon.lang._
+
+object Sets1 {
+  def set(i: Int): Int => Boolean = x => x == i
+
+  def complement(s: Int => Boolean): Int => Boolean = x => !s(x)
+
+  def union(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) || s2(x)
+
+  def intersection(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) && s2(x)
+
+  def associativity(sa1: Int => Boolean, sa2: Int => Boolean, sa3: Int => Boolean, x: Int): Boolean = {
+    val u1 = union(union(sa1, sa2), sa3)
+    val u2 = union(sa1, union(sa2, sa3))
+    u1(x) == u2(x)
+  }.holds
+
+  def lemma(s1: Int => Boolean, s2: Int => Boolean, x: Int): Boolean = {
+    val u1 = union(s1, s2)
+    val u2 = complement(intersection(complement(s1), complement(s2)))
+    u1(x) == u2(x)
+  }.holds
+}