Function lemma_forall_map_values_remove

pub broadcast proof fn lemma_forall_map_values_remove<K, V>(
    m: Map<K, V>,
    f: FnSpec<(V,), bool>,
    k: K,
)

Expand description

ensures

forall_map_values(m, f)
    <==> #[trigger] forall_map_values(m.remove(k), f) && (m.contains_key(k) ==> f(m[k])),

forall_map_values(m,f) holds if forall_map_values(m.remove(k), f) holds and f(m[k]) holds (if m contains k).

lemma_forall_map_values_remove