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.
pub broadcast proof fn axiom_len_empty<V>()(#[trigger] Multiset::<V>::empty().len()) == 0,The length of the empty multiset is 0.