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