Function vstd::seq_lib::lemma_seq_append_take_skip
source · pub 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.