Function vstd::seq_lib::lemma_seq_append_take_skip
source · pub broadcast proof fn lemma_seq_append_take_skip<A>(a: Seq<A>, b: Seq<A>, n: int)Expand description
ensures
n == a.len() ==> (((a + b).take(n) =~= a) && ((a + b).skip(n) =~= b)),If n is the length of sequence a, then taking the first n elements of the concatenation
a + b is equivalent to the sequence a and skipping the first n elements of the concatenation
a + b is equivalent to the sequence b.