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.