Function vstd::multiset::axiom_len_singleton
source · pub broadcast proof fn axiom_len_singleton<V>(v: V)Expand description
ensures
(#[trigger] Multiset::<V>::singleton(v).len()) == 1,The length of a singleton multiset is 1.