Function unions_union

pub fn unions_union<T, U>()

Distributivity of unions over union.

logic

{}

ensures

forall<s1: FSet<T>, s2: FSet<T>, f: Mapping<T, FSet<U>>> s1.union(s2).unions(f) == s1.unions(f).union(s2.unions(f))

ensures

forall<s: FSet<T>, f: Mapping<T, FSet<U>>, g: Mapping<T, FSet<U>>>
    s.unions(|x| f.get(x).union(g.get(x))) == s.unions(f).union(s.unions(g))