vstd::seq_lib

Function lemma_seq_empty_contains_nothing

Source 
pub broadcast proof fn lemma_seq_empty_contains_nothing<A>(x: A)
Expand description
ensures
!(#[trigger] Seq::<A>::empty().contains(x)),

The empty sequence contains nothing