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.
Edited by Dorian Lesbre
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.