lemma_forall_map_remove

vstd_extra::map_extra

Function lemma_forall_map_remove 

Source 
pub broadcast proof fn lemma_forall_map_remove<K, V>(
    m: Map<K, V>,
    f: FnSpec<(K, V), bool>,
    k: K,
)
Expand description
ensures
forall_map(m, f)
    <==> #[trigger] forall_map(m.remove(k), f) && (m.contains_key(k) ==> f(k, m[k])),

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