Function vstd::seq_lib::to_multiset_len

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

to_multiset() preserves length