// The following variant of set comprehensions allows us to form the final set
// elements by applying a function to the variables we quantify over.
function SetMap<A, B>(f: A -> B, s: set<A>): set<B> {
  set x | x in s :: f(x)
}

// Prove this size bound.
lemma SizeSetMap<A, B>(f: A -> B, s: set<A>)
  ensures |SetMap(f, s)| <= |s|