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.