Function vstd::seq_lib::lemma_seq_skip_build_commut
source · pub proof fn lemma_seq_skip_build_commut<A>(s: Seq<A>, v: A, n: int)Expand description
ensures
0 <= n <= s.len() ==> s.push(v).skip(n) =~= s.skip(n).push(v),Pushing element v onto the end of sequence s and then skipping the first n elements is
equivalent to skipping the first n elements of s and then pushing v onto the end.