pub broadcast proof fn lemma_forall_map_values_insert<K, V>(
m: Map<K, V>,
f: FnSpec<(V,), bool>,
k: K,
v: V,
)Expand description
ensures
#[trigger] forall_map_values(m.insert(k, v), f)
==> f(v)
&& if m.contains_key(k) {
forall_map_values(m.remove(k), f)
} else {
forall_map_values(m, f)
},forall_map_values(m.insert(k, v), f) holds if f(v) holds and
forall_map_values(m.remove(k),f) (if m contains k) or forall_map_values(m, f) (if m does not contain k).