Function vstd::map_lib::lemma_map_new_domain

source · 
pub proof fn lemma_map_new_domain<K, V>(fk: FnSpec<(K,), bool>, fv: FnSpec<(K,), V>)
Expand description
ensures
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).