vstd::multiset

Function axiom_multiset_ext_equal_deep

Source
pub broadcast proof fn axiom_multiset_ext_equal_deep<V>(m1: Multiset<V>, m2: Multiset<V>)
Expand description
ensures
#[trigger] (m1 =~~= m2) <==> (m1 =~= m2),