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.