fix trigger in to_multiset_len and commutative_foldr proof (#1454)

* fix trigger in to_multiset_len trigger and commutative_foldr proof

source/vstd/seq_lib.rs

@@ -1434,8 +1434,7 @@ pub broadcast proof fn to_multiset_remove<A>(s: Seq<A>, i: int)
 /// to_multiset() preserves length
 pub broadcast proof fn to_multiset_len<A>(s: Seq<A>)
     ensures
-        #[trigger s.to_multiset().len()]
-        s.len() == s.to_multiset().len(),
+        s.len() == #[trigger] s.to_multiset().len(),
     decreases s.len(),
 {
     broadcast use super::multiset::group_multiset_axioms;
@@ -1822,6 +1821,8 @@ pub proof fn lemma_fold_right_permutation<A, B>(l1: Seq<A>, l2: Seq<A>, f: spec_
         ));
 
         lemma_fold_right_permutation(l1.drop_last(), l2.remove(i), f, v);
+    } else {
+        assert(l2.to_multiset().len() == 0);
     }
 }