Function vstd::seq_lib::lemma_seq_empty_contains_nothing

source · 
pub proof fn lemma_seq_empty_contains_nothing<A>(x: A)
Expand description
ensures
!Seq::<A>::empty().contains(x),

The empty sequence contains nothing