pub broadcast proof fn axiom_choose_count<V>(m: Multiset<V>)Expand description
requires
#[trigger] m.len() != 0,#[trigger] m.count(m.choose()) > 0,In a nonempty multiset m, the choose function will return a value that maps to a multiplicity
greater than 0 in m.