Function vstd::seq_lib::lemma_seq_subrange_elements
source · pub broadcast proof fn lemma_seq_subrange_elements<A>(s: Seq<A>, start: int, stop: int, x: A)Expand description
requires
0 <= start <= stop <= s.len(),#[trigger] s.subrange(start, stop).contains(x)
<==> (exists |i: int| 0 <= start <= i < stop <= s.len() && #[trigger] s[i] == x),The subrange of a sequence contains only the elements within the indices start and stop
of the original sequence.