Function to_multiset_update

Source
pub broadcast proof fn to_multiset_update<A>(s: Seq<A>, i: int, a: A)
Expand description
requires
0 <= i < s.len(),
ensures
#[trigger] s.update(i, a).to_multiset() == s.to_multiset().insert(a).remove(s[i]),