pub broadcast proof fn lemma_map_new_domain<K, V>(s: Set<K>, fv: FnSpec<(K,), V>)Expand description
ensures
#[trigger] Map::<K, V>::new(s, fv).dom() == s,The domain of a map constructed with Map::new(fk, fv) is equivalent to the set constructed with Set::new(fk).