vstd::multiset

Function 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.