pub broadcast proof fn lemma_map_new_index<K, V>(s: Set<K>, fv: FnSpec<(K,), V>, k: K)Expand description
requires
s.contains(k),Map::new(s, fv)[k] == fv(k),Since Map::new is closed, this broadcast lemma is needed to establish
that it produces a map that maps elements using the given function.