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,