diff --git a/testcases/RedBlackTree.scala b/testcases/RedBlackTree.scala
index 70f3d6316331e2d6e859e0892ea374293cc950ea..0952a11fedf832381651f2130eafa20503a60974 100644
--- a/testcases/RedBlackTree.scala
+++ b/testcases/RedBlackTree.scala
@@ -51,4 +51,9 @@ object RedBlackTree {
     case Node(Red(),l,v,r) => Node(Black(),l,v,r)
     case _ => n
   }
+
+  def flip(t : Tree) : Tree = t match {
+    case Empty() => Empty()
+    case Node(color,l,e,r) => Node(color,flip(r),e,flip(l))
+  }
 }
diff --git a/testcases/UseContradictoryLemma.scala b/testcases/UseContradictoryLemma.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f25cec124868e997d9bf1259e013478d96fff335
--- /dev/null
+++ b/testcases/UseContradictoryLemma.scala
@@ -0,0 +1,15 @@
+import scala.collection.immutable.Set
+import funcheck.Utils._
+import funcheck.Annotations._
+
+object UseContradictoryLemma {
+
+  def lemma1(x : Int) : Boolean = {
+    x == 1
+  } holds
+
+  def f(x : Int) : Int = { 
+    5
+  } ensuring (x => lemma1(x) && x == 1)
+
+}