Function lemma_seq_skip_nothing 

pub broadcast proof fn lemma_seq_skip_nothing<A>(s: Seq<A>, n: int)

ensures

n == 0 ==> (#[trigger] s[n..] =~= s),

s[0..] is equivalent to s.