vstd::seq_lib

Function lemma_seq_skip_nothing

Source 
pub broadcast proof fn lemma_seq_skip_nothing<A>(s: Seq<A>, n: int)
Expand description
ensures
n == 0 ==> (#[trigger] s.skip(n) =~= s),

s.skip(0) is equivalent to s.