Function vstd::seq_lib::lemma_seq_empty_equality

source · 
pub proof fn lemma_seq_empty_equality<A>(s: Seq<A>)
Expand description
ensures
s.len() == 0 ==> s =~= Seq::<A>::empty(),

A sequence with length 0 is equivalent to the empty sequence