Function vstd::multiset::axiom_multiset_always_finite

source · 
pub broadcast proof fn axiom_multiset_always_finite<V>(m: Multiset<V>)
Expand description
ensures
#[trigger] m.dom().finite(),

The domain of a multiset (the set of all values that map to a multiplicity greater than 0) is always finite.