Function vstd::seq_lib::lemma_seq_take_nothing

source · 
pub broadcast proof fn lemma_seq_take_nothing<A>(s: Seq<A>, n: int)
Expand description
ensures
n == 0 ==> (#[trigger] s.take(n) =~= Seq::<A>::empty()),

s.take(0) is equivalent to the empty sequence.