Function vstd::seq_lib::lemma_seq_union_to_multiset_commutative

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

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