Function vstd::seq_lib::lemma_seq_empty_equality

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

A sequence with length 0 is equivalent to the empty sequence