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