Function vstd::seq_lib::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