Function seq_range_union 

pub open spec fn seq_range_union<T: FiniteRange>(s: Seq<Range<T>>) -> Set<T>

{ s.map_values(|r: Range<T>| r.view_set()).to_set().flatten() }

The union of the sets denoted by a sequence of ranges.