pub fn map_union<T, U>()
Expand description
Distributivity of map
over union
.
logic
{}
ensures
forall<s: FSet<T>, t: FSet<T>, f: Mapping<T, U>> s.union(t).map(f) == s.map(f).union(t.map(f))
pub fn map_union<T, U>()
Distributivity of map
over union
.
logic
{}
ensures
forall<s: FSet<T>, t: FSet<T>, f: Mapping<T, U>> s.union(t).map(f) == s.map(f).union(t.map(f))