lemma_forall_map_values_entry

vstd_extra::map_extra

Function lemma_forall_map_values_entry 

Source 
pub proof fn lemma_forall_map_values_entry<K, V>(
    m: Map<K, V>,
    f: FnSpec<(V,), bool>,
    k: K,
)
Expand description
requires
forall_map_values(m, f),
m.contains_key(k),
ensures
f(m[k]),

For any key in the map, f(map[k]) holds if forall_map_values(map, f) holds.