diff --git a/src/main/scala/leon/purescala/Quantification.scala b/src/main/scala/leon/purescala/Quantification.scala
index 847076f8b4e0cc5878a2f4b448e3880215148007..ba25faf4217083a24194871a74be7f648fa3f617 100644
--- a/src/main/scala/leon/purescala/Quantification.scala
+++ b/src/main/scala/leon/purescala/Quantification.scala
@@ -103,63 +103,54 @@ object Quantification {
 
     def apply(ctx: LeonContext, program: Program) = {
       program.definedFunctions.foreach { fd =>
-        if (fd.body.exists(b => exists {
-          case f: Forall => true
-          case _ => false
-        } (b))) ctx.reporter.warning("Universal quantification in function bodies is not supported in " + fd)
-
-        val foralls = (fd.precondition.toSeq ++ fd.postcondition.toSeq).flatMap { prec =>
-          collect[Forall] {
-            case f: Forall => Set(f)
-            case _ => Set.empty
-          } (prec)
-        }
+        val foralls = collect[Forall] {
+          case f: Forall => Set(f)
+          case _ => Set.empty
+        } (fd.fullBody)
 
         val free = fd.params.map(_.id).toSet ++ (fd.postcondition match {
           case Some(Lambda(args, _)) => args.map(_.id)
           case _ => Seq.empty
         })
 
-        object Matcher {
-          def unapply(e: Expr): Option[(Identifier, Seq[Expr])] = e match {
-            case QuantificationMatcher(Variable(id), args) if free(id) => Some(id -> args)
-            case _ => None
-          }
-        }
-
         for (Forall(args, TopLevelAnds(conjuncts)) <- foralls) {
           val quantified = args.map(_.id).toSet
 
           for (conjunct <- conjuncts) {
-            val matchers = collect[(Identifier, Seq[Expr])] {
-              case Matcher(id, args) => Set(id -> args)
+            val matchers = collect[(Expr, Seq[Expr])] {
+              case QuantificationMatcher(e, args) => Set(e -> args)
               case _ => Set.empty
             } (conjunct)
 
-            if (matchers.exists { case (id, args) =>
+            if (matchers.isEmpty)
+              ctx.reporter.warning("E-matching isn't possible without matchers!")
+
+            if (matchers.exists { case (_, args) =>
               args.exists(arg => arg match {
-                case Matcher(_, _) => false
+                case QuantificationMatcher(_, _) => false
                 case Variable(id) => false
                 case _ if (variablesOf(arg) & quantified).nonEmpty => true
                 case _ => false
               })
             }) ctx.reporter.warning("Matcher arguments must have simple form in " + conjunct)
 
-            val id2Quant = matchers.foldLeft(Map.empty[Identifier, Set[Identifier]]) {
+            val freeMatchers = matchers.collect { case (Variable(id), args) if free(id) => id -> args }
+
+            val id2Quant = freeMatchers.foldLeft(Map.empty[Identifier, Set[Identifier]]) {
               case (acc, (m, args)) => acc + (m -> (acc.getOrElse(m, Set.empty) ++ args.flatMap {
                 case Variable(id) if quantified(id) => Set(id)
                 case _ => Set.empty[Identifier]
               }))
             }
 
-            if (id2Quant.filter(_._2.nonEmpty).groupBy(_._2).size != 1)
+            if (id2Quant.filter(_._2.nonEmpty).groupBy(_._2).size >= 1)
               ctx.reporter.warning("Multiple matchers must provide bijective matching in " + conjunct)
 
             foldRight[Set[Identifier]] { case (m, children) =>
               val q = children.toSet.flatten
 
               m match {
-                case Matcher(_, args) =>
+                case QuantificationMatcher(_, args) =>
                   q -- args.flatMap {
                     case Variable(id) if quantified(id) => Set(id)
                     case _ => Set.empty[Identifier]
diff --git a/src/test/resources/regression/verification/purescala/invalid/BinarySearchTreeQuant.scala b/src/test/resources/regression/verification/purescala/invalid/BinarySearchTreeQuant.scala
new file mode 100644
index 0000000000000000000000000000000000000000..849de7d15c180c8d8ed945e2420043b36ba92152
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/BinarySearchTreeQuant.scala
@@ -0,0 +1,42 @@
+import leon.lang._
+import leon.collection._
+
+object BSTSimpler {
+  sealed abstract class Tree
+  case class Node(left: Tree, value: BigInt, right: Tree) extends Tree
+  case class Leaf() extends Tree
+
+  def content(tree: Tree): Set[BigInt] = tree match {
+    case Leaf() => Set.empty[BigInt]
+    case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+  }
+
+  def isBST(tree: Tree) : Boolean = tree match {
+    case Leaf() => true
+    case Node(left, v, right) => {
+      isBST(left) && isBST(right) &&
+      forall((x:BigInt) => (content(left).contains(x) ==> x < v - 10)) &&
+      forall((x:BigInt) => (content(right).contains(x) ==> v < x))
+    }
+  }
+
+  def emptySet(): Tree = Leaf()
+
+  def insert(tree: Tree, value: BigInt): Node = {
+    require(isBST(tree))
+    tree match {
+      case Leaf() => Node(Leaf(), value, Leaf())
+      case Node(l, v, r) => (if (v < value) {
+        Node(l, v, insert(r, value))
+      } else if (v > value) {
+        Node(insert(l, value), v, r)
+      } else {
+        Node(l, v, r)
+      })
+    }
+  } ensuring(res => isBST(res) && content(res) == content(tree) ++ Set(value))
+
+  def createRoot(v: BigInt): Node = {
+    Node(Leaf(), v, Leaf())
+  } ensuring (content(_) == Set(v))
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/BinarySearchTreeQuant.scala b/src/test/resources/regression/verification/purescala/valid/BinarySearchTreeQuant.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a435e69ca7a0574937f7368e499c5750983133b3
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/BinarySearchTreeQuant.scala
@@ -0,0 +1,42 @@
+import leon.lang._
+import leon.collection._
+
+object BSTSimpler {
+  sealed abstract class Tree
+  case class Node(left: Tree, value: BigInt, right: Tree) extends Tree
+  case class Leaf() extends Tree
+
+  def content(tree: Tree): Set[BigInt] = tree match {
+    case Leaf() => Set.empty[BigInt]
+    case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+  }
+
+  def isBST(tree: Tree) : Boolean = tree match {
+    case Leaf() => true
+    case Node(left, v, right) => {
+      isBST(left) && isBST(right) &&
+      forall((x:BigInt) => (content(left).contains(x) ==> x < v)) &&
+      forall((x:BigInt) => (content(right).contains(x) ==> v < x))
+    }
+  }
+
+  def emptySet(): Tree = Leaf()
+
+  def insert(tree: Tree, value: BigInt): Node = {
+    require(isBST(tree))
+    tree match {
+      case Leaf() => Node(Leaf(), value, Leaf())
+      case Node(l, v, r) => (if (v < value) {
+        Node(l, v, insert(r, value))
+      } else if (v > value) {
+        Node(insert(l, value), v, r)
+      } else {
+        Node(l, v, r)
+      })
+    }
+  } ensuring(res => isBST(res) && content(res) == content(tree) ++ Set(value))
+
+  def createRoot(v: BigInt): Node = {
+    Node(Leaf(), v, Leaf())
+  } ensuring (content(_) == Set(v))
+}
diff --git a/testcases/verification/datastructures/BinarySearchTreeQuant.scala b/testcases/verification/datastructures/BinarySearchTreeQuant.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a435e69ca7a0574937f7368e499c5750983133b3
--- /dev/null
+++ b/testcases/verification/datastructures/BinarySearchTreeQuant.scala
@@ -0,0 +1,42 @@
+import leon.lang._
+import leon.collection._
+
+object BSTSimpler {
+  sealed abstract class Tree
+  case class Node(left: Tree, value: BigInt, right: Tree) extends Tree
+  case class Leaf() extends Tree
+
+  def content(tree: Tree): Set[BigInt] = tree match {
+    case Leaf() => Set.empty[BigInt]
+    case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+  }
+
+  def isBST(tree: Tree) : Boolean = tree match {
+    case Leaf() => true
+    case Node(left, v, right) => {
+      isBST(left) && isBST(right) &&
+      forall((x:BigInt) => (content(left).contains(x) ==> x < v)) &&
+      forall((x:BigInt) => (content(right).contains(x) ==> v < x))
+    }
+  }
+
+  def emptySet(): Tree = Leaf()
+
+  def insert(tree: Tree, value: BigInt): Node = {
+    require(isBST(tree))
+    tree match {
+      case Leaf() => Node(Leaf(), value, Leaf())
+      case Node(l, v, r) => (if (v < value) {
+        Node(l, v, insert(r, value))
+      } else if (v > value) {
+        Node(insert(l, value), v, r)
+      } else {
+        Node(l, v, r)
+      })
+    }
+  } ensuring(res => isBST(res) && content(res) == content(tree) ++ Set(value))
+
+  def createRoot(v: BigInt): Node = {
+    Node(Leaf(), v, Leaf())
+  } ensuring (content(_) == Set(v))
+}
diff --git a/testcases/verification/quantification/invalid/BinarySearchTreeQuant.scala b/testcases/verification/quantification/invalid/BinarySearchTreeQuant.scala
new file mode 100644
index 0000000000000000000000000000000000000000..849de7d15c180c8d8ed945e2420043b36ba92152
--- /dev/null
+++ b/testcases/verification/quantification/invalid/BinarySearchTreeQuant.scala
@@ -0,0 +1,42 @@
+import leon.lang._
+import leon.collection._
+
+object BSTSimpler {
+  sealed abstract class Tree
+  case class Node(left: Tree, value: BigInt, right: Tree) extends Tree
+  case class Leaf() extends Tree
+
+  def content(tree: Tree): Set[BigInt] = tree match {
+    case Leaf() => Set.empty[BigInt]
+    case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+  }
+
+  def isBST(tree: Tree) : Boolean = tree match {
+    case Leaf() => true
+    case Node(left, v, right) => {
+      isBST(left) && isBST(right) &&
+      forall((x:BigInt) => (content(left).contains(x) ==> x < v - 10)) &&
+      forall((x:BigInt) => (content(right).contains(x) ==> v < x))
+    }
+  }
+
+  def emptySet(): Tree = Leaf()
+
+  def insert(tree: Tree, value: BigInt): Node = {
+    require(isBST(tree))
+    tree match {
+      case Leaf() => Node(Leaf(), value, Leaf())
+      case Node(l, v, r) => (if (v < value) {
+        Node(l, v, insert(r, value))
+      } else if (v > value) {
+        Node(insert(l, value), v, r)
+      } else {
+        Node(l, v, r)
+      })
+    }
+  } ensuring(res => isBST(res) && content(res) == content(tree) ++ Set(value))
+
+  def createRoot(v: BigInt): Node = {
+    Node(Leaf(), v, Leaf())
+  } ensuring (content(_) == Set(v))
+}
diff --git a/testcases/verification/quantification/invalid/HOInvocations.scala b/testcases/verification/quantification/invalid/HOInvocations.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5cd0afc42e447404d227dbfa43b3ea3f7f260678
--- /dev/null
+++ b/testcases/verification/quantification/invalid/HOInvocations.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object HOInvocations {
+  def switch(x: BigInt, f: (BigInt) => BigInt, g: (BigInt) => BigInt) = if(x > 0) f else g
+
+  def failling_1(f: (BigInt) => BigInt) = {
+    switch(-10, (x: BigInt) => x + 1, f)(2)
+  } ensuring { res => res > 0 }
+
+  def failling_2(x: BigInt, f: (BigInt) => BigInt, g: (BigInt) => BigInt) = {
+    require(x > 0 && forall((a: BigInt) => a > 0 ==> f(a) > 0))
+    switch(1, switch(x, f, g), g)(0)
+  } ensuring { res => res > 0 }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/quantification/invalid/Monotonic.scala b/testcases/verification/quantification/invalid/Monotonic.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bc9a1bc76855e21d514a10ebdf257235480b1e10
--- /dev/null
+++ b/testcases/verification/quantification/invalid/Monotonic.scala
@@ -0,0 +1,10 @@
+import leon.lang._
+
+object Monotonic {
+  def failling_1(f: BigInt => BigInt, g: BigInt => BigInt): BigInt => BigInt = {
+    require(forall((a: BigInt, b: BigInt) => (a > b ==> f(a) > f(b))))
+    (x: BigInt) => f(g(x))
+  } ensuring { res => forall((a: BigInt, b: BigInt) => a > b ==> res(a) > res(b)) }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/quantification/invalid/PositiveMap.scala b/testcases/verification/quantification/invalid/PositiveMap.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7b15cb2576e9119d27f77e158fddfee0e6e4bc98
--- /dev/null
+++ b/testcases/verification/quantification/invalid/PositiveMap.scala
@@ -0,0 +1,23 @@
+import leon.lang._
+
+object PositiveMap {
+  
+  abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case class Nil() extends List
+
+  def positive(list: List): Boolean = list match {
+    case Cons(head, tail) => if (head < 0) false else positive(tail)
+    case Nil() => true
+  }
+
+  def positiveMap_failling_1(f: (BigInt) => BigInt, list: List): List = {
+    require(forall((a: BigInt) => f(a) > -2))
+    list match {
+      case Cons(head, tail) => Cons(f(head), positiveMap_failling_1(f, tail))
+      case Nil() => Nil()
+    }
+  } ensuring { res => positive(res) }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/quantification/invalid/Postcondition.scala b/testcases/verification/quantification/invalid/Postcondition.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d942f446e9ce75f42545e4078b56b89962df540c
--- /dev/null
+++ b/testcases/verification/quantification/invalid/Postcondition.scala
@@ -0,0 +1,14 @@
+import leon.lang._
+
+object Postconditions {
+  def failling_1(f: BigInt => BigInt) = {
+    require(forall((a: BigInt) => a > 0 ==> f(a) > 0))
+    f(10)
+  } ensuring { res => forall((a: BigInt) => res > f(a)) }
+
+  def failling_2(f: BigInt => BigInt, x: BigInt) = {
+    require(x >= 0 && forall((a: BigInt) => a > 0 ==> f(a) < 0))
+    x
+  } ensuring { res => forall((a: BigInt) => res > f(a)) }
+
+}
diff --git a/testcases/verification/quantification/invalid/Simple.scala b/testcases/verification/quantification/invalid/Simple.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7a3446612bd910dfbe7389b0d83001606640457c
--- /dev/null
+++ b/testcases/verification/quantification/invalid/Simple.scala
@@ -0,0 +1,20 @@
+import leon.lang._
+
+object Simple {
+
+  def failling_1(f: BigInt => BigInt) = {
+    require(forall((a: BigInt) => a > 0 ==> f(a) > 0))
+    f(-1)
+  } ensuring { res => res > 0 }
+
+  def failling_2(f: BigInt => BigInt) = {
+    require(forall((a: BigInt) => a > 0 ==> f(a) > 1))
+    f(1) + f(2)
+  } ensuring { res => res > 4 }
+
+  def failling_4(f: BigInt => BigInt, g: BigInt => BigInt, x: BigInt) = {
+    require(forall((a: BigInt, b: BigInt) => f(a) + g(a) > 0))
+    if(x < 0) f(x) + g(x)
+    else x
+  } ensuring { res => res > 0 }
+}
diff --git a/testcases/verification/quantification/invalid/SizeInc.scala b/testcases/verification/quantification/invalid/SizeInc.scala
new file mode 100644
index 0000000000000000000000000000000000000000..970b3b53bddb295db19308e3443309f478ee15cc
--- /dev/null
+++ b/testcases/verification/quantification/invalid/SizeInc.scala
@@ -0,0 +1,17 @@
+import leon.lang._
+
+object SizeInc {
+  
+  abstract class List[A]
+  case class Cons[A](head: A, tail: List[A]) extends List[A]
+  case class Nil[A]() extends List[A]
+
+  def failling_1[A](x: List[A]): Int => Int = {
+    (i: Int) => x match {
+      case Cons(head, tail) => 1 + failling_1(tail)(i)
+      case Nil() => i
+    }
+  } ensuring { res => forall((a: Int) => res(a) > 0) }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/quantification/valid/BinarySearchTreeQuant.scala b/testcases/verification/quantification/valid/BinarySearchTreeQuant.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a435e69ca7a0574937f7368e499c5750983133b3
--- /dev/null
+++ b/testcases/verification/quantification/valid/BinarySearchTreeQuant.scala
@@ -0,0 +1,42 @@
+import leon.lang._
+import leon.collection._
+
+object BSTSimpler {
+  sealed abstract class Tree
+  case class Node(left: Tree, value: BigInt, right: Tree) extends Tree
+  case class Leaf() extends Tree
+
+  def content(tree: Tree): Set[BigInt] = tree match {
+    case Leaf() => Set.empty[BigInt]
+    case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+  }
+
+  def isBST(tree: Tree) : Boolean = tree match {
+    case Leaf() => true
+    case Node(left, v, right) => {
+      isBST(left) && isBST(right) &&
+      forall((x:BigInt) => (content(left).contains(x) ==> x < v)) &&
+      forall((x:BigInt) => (content(right).contains(x) ==> v < x))
+    }
+  }
+
+  def emptySet(): Tree = Leaf()
+
+  def insert(tree: Tree, value: BigInt): Node = {
+    require(isBST(tree))
+    tree match {
+      case Leaf() => Node(Leaf(), value, Leaf())
+      case Node(l, v, r) => (if (v < value) {
+        Node(l, v, insert(r, value))
+      } else if (v > value) {
+        Node(insert(l, value), v, r)
+      } else {
+        Node(l, v, r)
+      })
+    }
+  } ensuring(res => isBST(res) && content(res) == content(tree) ++ Set(value))
+
+  def createRoot(v: BigInt): Node = {
+    Node(Leaf(), v, Leaf())
+  } ensuring (content(_) == Set(v))
+}
diff --git a/testcases/verification/quantification/valid/Composition.scala b/testcases/verification/quantification/valid/Composition.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cd62eb8da69132b1825630d6a6d3885a06e951aa
--- /dev/null
+++ b/testcases/verification/quantification/valid/Composition.scala
@@ -0,0 +1,14 @@
+
+import leon.lang._
+
+object Composition {
+  def passing_1(f: (Int) => Int, g: (Int) => Int, x: Int): Int = {
+    require(g(1) == 2 && forall((a: Int) => f(g(a)) == a))
+    val a = g(x)
+    if(x == 1)
+      f(g(a))
+    else 2
+  } ensuring { _ == 2 }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/quantification/valid/HOInvocations.scala b/testcases/verification/quantification/valid/HOInvocations.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ba44b8fdc3e38542dd6e84664a717517a7392f5f
--- /dev/null
+++ b/testcases/verification/quantification/valid/HOInvocations.scala
@@ -0,0 +1,17 @@
+import leon.lang._
+
+object HOInvocations {
+  def switch(x: Int, f: (Int) => Int, g: (Int) => Int) = if(x > 0) f else g
+
+  def passing_1(f: (Int) => Int) = {
+    switch(10, (x: Int) => x + 1, f)(2)
+  } ensuring { res => res > 0 }
+
+  def passing_2(x: Int, f: (Int) => Int, g: (Int) => Int) = {
+    require(x > 0 && forall((a: Int) => a > 0 ==> f(a) > 0))
+    switch(1, switch(x, f, g), g)(1)
+  } ensuring { res => res > 0 }
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/quantification/valid/Monotonic.scala b/testcases/verification/quantification/valid/Monotonic.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cef6be60f2d6d27ffd2eae005f649a44b9d94a2a
--- /dev/null
+++ b/testcases/verification/quantification/valid/Monotonic.scala
@@ -0,0 +1,10 @@
+import leon.lang._
+
+object Monotonic {
+  def composeMonotonic(f: BigInt => BigInt, g: BigInt => BigInt): BigInt => BigInt = {
+    require(forall((a: BigInt, b: BigInt) => (a > b ==> f(a) > f(b)) && (a > b ==> g(a) > g(b))))
+    (x: BigInt) => f(g(x))
+  } ensuring { res => forall((a: BigInt, b: BigInt) => a > b ==> res(a) > res(b)) }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/quantification/valid/PositiveMap.scala b/testcases/verification/quantification/valid/PositiveMap.scala
new file mode 100644
index 0000000000000000000000000000000000000000..030e7095954a063b0d9b0e19ed15c0d6958e2304
--- /dev/null
+++ b/testcases/verification/quantification/valid/PositiveMap.scala
@@ -0,0 +1,33 @@
+
+import leon.lang._
+
+object PositiveMap {
+  
+  abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case class Nil() extends List
+
+  def positive(list: List): Boolean = list match {
+    case Cons(head, tail) => if (head < 0) false else positive(tail)
+    case Nil() => true
+  }
+
+  def positiveMap_passing_1(f: (BigInt) => BigInt, list: List): List = {
+    require(forall((a: BigInt) => f(a) > 0))
+    list match {
+      case Cons(head, tail) => Cons(f(head), positiveMap_passing_1(f, tail))
+      case Nil() => Nil()
+    }
+  } ensuring { res => positive(res) }
+
+  def positiveMap_passing_2(f: (BigInt) => BigInt, list: List): List = {
+    require(forall((a: BigInt) => f(a) > -1))
+    list match {
+      case Cons(head, tail) => Cons(f(head), positiveMap_passing_2(f, tail))
+      case Nil() => Nil()
+    }
+  } ensuring { res => positive(res) }
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/quantification/valid/Postcondition.scala b/testcases/verification/quantification/valid/Postcondition.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e044a9a3adc1214bb1ce917b6be3785be1fd93fe
--- /dev/null
+++ b/testcases/verification/quantification/valid/Postcondition.scala
@@ -0,0 +1,23 @@
+import leon.lang._
+
+object Postconditions {
+
+  def passing_1(f: BigInt => BigInt, x: BigInt) = {
+    require(x >= 0 && forall((a: BigInt) => f(a) < 0))
+    x
+  } ensuring { res => forall((a: BigInt) => res > f(a)) }
+
+  def passing_2(f: BigInt => BigInt, x: BigInt) = {
+    require(x >= 0 && forall((a: BigInt) => a > 0 ==> f(a) < 0))
+    x
+  } ensuring { res => forall((a: BigInt) => a > 0 ==> res > f(a)) }
+
+  def passing_3(f: BigInt => BigInt) = {
+    require(forall((a: BigInt) => f(a) > 0))
+    f
+  } ensuring { res => forall((a: BigInt) => res(a) > 0) }
+
+  def passing_4() = {
+    (x: BigInt) => x + 1
+  } ensuring { res => forall((a: BigInt) => res(a) > a) }
+}
diff --git a/testcases/verification/quantification/valid/Relations.scala b/testcases/verification/quantification/valid/Relations.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ebce8d5b595b68fe866c050436486087cac47476
--- /dev/null
+++ b/testcases/verification/quantification/valid/Relations.scala
@@ -0,0 +1,31 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.proof._
+
+object Relations {
+
+  case class Relation[A](r: (A, A) => Boolean)
+
+  def reflexive[A](rel: Relation[A]) = 
+    forall( (x: A) => rel.r(x, x) )
+
+  def symmetric[A](rel: Relation[A]) =
+    forall( (x:A, y:A) => rel.r(x, y) == rel.r(y, x) )
+  
+  def antisymmetric[A](rel: Relation[A]) = 
+    forall( (x:A, y:A) => ( rel.r(x,y) && rel.r(y,x) ) ==> (x == y) )
+  
+  def transitive[A](rel: Relation[A]) = 
+    forall( (x:A, y:A, z:A) => ( rel.r(x,y) && rel.r(y,z) ) ==> rel.r(x,z) )
+    
+  def po[A](rel: Relation[A]) =
+    reflexive(rel) &&
+    antisymmetric(rel) &&
+    transitive(rel)
+
+  def test = po(Relation[BigInt](_ <= _)).holds
+
+}
+
+
+
diff --git a/testcases/verification/quantification/valid/Simple.scala b/testcases/verification/quantification/valid/Simple.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5e7e9cb339037a0acc73a4f66e4c07bac61e7df1
--- /dev/null
+++ b/testcases/verification/quantification/valid/Simple.scala
@@ -0,0 +1,44 @@
+import leon.lang._
+
+object Simple {
+
+  def passing_1(f: BigInt => BigInt) = {
+    require(forall((a: BigInt) => a > 0 ==> f(a) > 0))
+    f(10)
+  } ensuring { res => res > 0 }
+
+  def passing_2(f: BigInt => BigInt) = {
+    require(forall((a: BigInt) => a > 0 ==> f(a) > 1))
+    f(1) + f(2)
+  } ensuring { res => res > 2 }
+
+  def passing_3(f: BigInt => BigInt) = {
+    require(forall((a: BigInt) => f(a) > 0 || f(a) < 0))
+    f(8)
+  } ensuring { res => res != 0 }
+
+  def passing_4(f: BigInt => BigInt, g: BigInt => BigInt, x: BigInt) = {
+    require(forall((a: BigInt, b: BigInt) => f(a) + f(b) > 0))
+    if(x <= 0) f(x) + f(x)
+    else x
+  } ensuring { res => res > 0 }
+
+  def passing_5(f: BigInt => BigInt, g: BigInt => Boolean): BigInt = {
+    require(forall((a: BigInt) => if(g(a)) { f(a) > 0 || f(a) < 0 } else { f(a) == 0 }))
+    if(g(8)) f(8)
+    else BigInt(1)
+  } ensuring { res => res != 0 }
+
+  def passing_6(f: BigInt => BigInt, x: BigInt) = {
+    require(x > 0 && forall((a: BigInt) => a > 0 ==> f(a) > 0))
+    if(x > 0) f(1)
+    else f(-1)
+  } ensuring { res => res > 0 }
+
+  def passing_7(f: BigInt => BigInt) = {
+    require(forall((a: BigInt) => a > 0 ==> f(a) > 0))
+    val a = f(-1)
+    f(2)
+  } ensuring { res => res > 0 }
+
+}
diff --git a/testcases/verification/quantification/valid/SizeInc.scala b/testcases/verification/quantification/valid/SizeInc.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9fe7ea96eb44bba951ff620507bad750c1560056
--- /dev/null
+++ b/testcases/verification/quantification/valid/SizeInc.scala
@@ -0,0 +1,26 @@
+import leon.lang._
+
+object SizeInc {
+  
+  abstract class List[A]
+  case class Cons[A](head: A, tail: List[A]) extends List[A]
+  case class Nil[A]() extends List[A]
+
+  def sizeInc[A](x: List[A]): BigInt => BigInt = {
+    (i: BigInt) => x match {
+      case Cons(head, tail) => 1 + sizeInc(tail)(i)
+      case Nil() => i
+    }
+  } ensuring { res => forall((a: BigInt) => a > 0 ==> res(a) > 0) }
+
+  def sizeInc2[A](x: BigInt): List[A] => BigInt = {
+    require(x > 0)
+
+    (list: List[A]) => list match {
+      case Cons(head, tail) => 1 + sizeInc2(x)(tail)
+      case Nil() => x
+    }
+  } ensuring { res => forall((a: List[A]) => res(a) > 0) }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/quantification/valid/Transitive.scala b/testcases/verification/quantification/valid/Transitive.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5e7bb03cd858c34f9876de1ecc723e010fdab162
--- /dev/null
+++ b/testcases/verification/quantification/valid/Transitive.scala
@@ -0,0 +1,12 @@
+import leon.lang._
+
+object Transitive {
+  
+  def multiAssoc(f: (Int, Int, Int) => Int): Boolean = {
+    require(forall { (a: Int, b: Int, c: Int, d: Int, e: Int) =>
+      f(f(a,b,c),d,e) == f(a,f(b,c,d),e) && f(a,f(b,c,d),e) == f(a,b,f(c,d,e))
+    })
+    f(f(1,2,3),4,5) == f(1,2,f(3,4,5))
+  }.holds
+
+}