pub broadcast proof fn to_multiset_len<A>(s: Seq<A>)
s.len() == #[trigger] s.to_multiset().len(),
to_multiset() preserves length