pub broadcast proof fn lemma_map_new_domain<K, V>(s: Set<K>, fv: FnSpec<(K,), V>)Expand description
ensures
Map::new(s, fv).dom() == s,Since Map::new is uninterpret, this broadcast lemma is needed to establish
that it produces a map with the given set as its domain.