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.