Function vstd::multiset::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,