Function vstd::seq_lib::lemma_multiset_commutative

source · 
pub proof fn lemma_multiset_commutative<A>(a: Seq<A>, b: Seq<A>)
Expand description
ensures
(a + b).to_multiset() =~= a.to_multiset().add(b.to_multiset()),

The multiset of a concatenated sequence a + b is equivalent to the multiset of just sequence a added to the multiset of just sequence b.