one can use lemmas by conjoining their instances

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))
+  }
 }

testcases/UseContradictoryLemma.scala

+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)
+
+}