pub proof fn lemma_forall_map_entry<K, V>(m: Map<K, V>, f: FnSpec<(K, V), bool>, k: K)Expand description
requires
forall_map(m, f),m.contains_key(k),f(k, m[k]),For any key in the map, f(k, map[k]) holds if forall_map(map, f) holds.