add flatmap postcondition

frontends/library/stainless/lang/Set.scala

@@ -36,26 +36,33 @@ object Set {
       new Set(set.theSet.map(f))
     }
 
-    @extern @pure
-    def flatMap[B](f: A => Set[B]): Set[B] = {
-      new Set(set.theSet.flatMap(f(_).theSet))
-    }
-
     @extern @pure
     def mapPost1[B](f: A => B)(a: A): Unit = {
       ()
-   }.ensuring { _ =>
+    }.ensuring { _ =>
       !set.contains(a) || map[B](f).contains(f(a))
     }
 
     @extern @pure
     def mapPost2[B](f: A => B)(b: B): A = {
       require(map[B](f).contains(b))
       (??? : A)
-   }.ensuring { (a:A) =>
+    }.ensuring { (a:A) =>
       b == f(a) && set.contains(a)
     }
 
+    @extern @pure
+    def flatMap[B](f: A => Set[B]): Set[B] = {
+      new Set(set.theSet.flatMap(f(_).theSet))
+    }
+
+    @extern @pure
+    def flatMapPost[B](f: A => B)(b: B) = {
+      (??? : A)
+    }.ensuring { _ =>
+      flatMap(f).contains(b) == set.exists(a => f(a).contains(b))
+    }
+
     @extern @pure
     def filter(p: A => Boolean): Set[A] = {
       new Set(set.theSet.filter(p))