pub proof fn lemma_seq_range_union_contains<T: FiniteRange>(s: Seq<Range<T>>, x: T)Expand description
ensures
seq_range_union(s).contains(x) <==> s.any(|r: Range<T>| r.view_set().contains(x)),An element belongs to the union of a sequence of ranges if and only if it belongs to at least one of those ranges.