Function vstd::multiset::axiom_choose_count

source · 
pub broadcast proof fn axiom_choose_count<V>(m: Multiset<V>)
Expand description
requires
#[trigger] m.len() != 0,
ensures
#[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.