Function map_union 

pub fn map_union<T, U>()

Distributivity of map over union.

(open)

{}

ensures

forall<s: FSet<T>, t: FSet<T>, f: Mapping<T, U>> s.union(t).map(f) == s.map(f).union(t.map(f))