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