Function axiom_multiset_ext_equal_deep

Help

pub broadcast proof fn axiom_multiset_ext_equal_deep<V>(m1: Multiset<V>, m2: Multiset<V>)

Expand description

ensures

#[trigger] (m1 =~~= m2) <==> (m1 =~= m2),

Function axiom_multiset_ext_equal_deepCopy item path