vstd::seq_lib

Function 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