Function vstd::seq_lib::to_multiset_contains

source · 
pub broadcast proof fn to_multiset_contains<A>(s: Seq<A>, a: A)
Expand description
ensures
s.contains(a) <==> s.to_multiset().count(a) > 0,

to_multiset() contains only the elements of the sequence