Add set_omap to finite sets

Add omap-like function to finite sets, aka OCaml's filter_map operation.

I needed it to destruct a set of X + Y into a set of X and a set of Y.

Also add a few lemmas to reason about it.

stdpp/fin_sets.v

@@ -450,7 +450,7 @@ End map.
 
 (** * Bind *)
 Section set_bind.
-  Context `{FinSet B SB}.
+  Context `{Set_ B SB}.
 
   Local Notation set_bind := (set_bind (A:=A) (SA:=C) (SB:=SB)).