Function vstd::seq_lib::lemma_seq_skip_of_skip
source · pub proof fn lemma_seq_skip_of_skip<A>(s: Seq<A>, m: int, n: int)Expand description
ensures
(0 <= m && 0 <= n && m + n <= s.len()) ==> s.skip(m).skip(n) =~= s.skip(m + n),If m + n is less than or equal to the length of sequence s, then skipping the first m elements
and then skipping the first n elements of the resulting sequence is equivalent to just skipping
the first m + n elements.