Function vstd::multiset::axiom_len_empty
source · pub broadcast proof fn axiom_len_empty<V>()Expand description
ensures
(#[trigger] Multiset::<V>::empty().len()) == 0,The length of the empty multiset is 0.