Function vstd::seq_lib::to_multiset_remove

source · 
pub broadcast proof fn to_multiset_remove<A>(s: Seq<A>, i: int)
Expand description
requires
0 <= i < s.len(),
ensures
s.remove(i).to_multiset() =~= s.to_multiset().remove(s[i]),