Function vstd::map_lib::lemma_map_new_values

source · 
pub proof fn lemma_map_new_values<K, V>(fk: FnSpec<(K,), bool>, fv: FnSpec<(K,), V>)
Expand description
ensures
Map::<K, V>::new(fk, fv).values()
    == Set::<V>::new(|v: V| (exists |k: K| #[trigger] fk(k) && #[trigger] fv(k) == v)),

The set of values of a map constructed with Map::new(fk, fv) is equivalent to the set constructed with Set::new(|v: V| (exists |k: K| fk(k) && fv(k) == v). In other words, the set of all values fv(k) where fk(k) is true.