Function concat_union

pub fn concat_union<T>()

Distributivity of concat over union.

logic

{}

ensures

forall<s1: FSet<Seq<T>>, s2: FSet<Seq<T>>, t: FSet<Seq<T>>>
    FSet::concat(s1.union(s2), t) == FSet::concat(s1, t).union(FSet::concat(s2, t))

ensures

forall<s: FSet<Seq<T>>, t1: FSet<Seq<T>>, t2: FSet<Seq<T>>>
    FSet::concat(s, t1.union(t2)) == FSet::concat(s, t1).union(FSet::concat(s, t2))