Function vstd::seq_lib::lemma_seq_skip_update_commut1
source · pub proof fn lemma_seq_skip_update_commut1<A>(s: Seq<A>, i: int, v: A, n: int)Expand description
ensures
0 <= n <= i < s.len()
==> #[trigger] s.update(i, v).skip(n) =~= s.skip(n).update(i - n, v),If i is a valid index after the first n indices of sequence s, updating sequence s at
index i with value v and then skipping the first n elements is equivalent to skipping the first n
elements of s and then updating index i-n to value v.