Function lemma_seq_append_take_skip 

pub broadcast proof fn lemma_seq_append_take_skip<A>(a: Seq<A>, b: Seq<A>, n: int)

ensures

n == a.len() ==> (((a + b)[..n] =~= a) && ((a + b)[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.