vstd::map_lib

Function lemma_values_finite

Source 
pub proof fn lemma_values_finite<K, V>(m: Map<K, V>)
Expand description
requires
m.dom().finite(),
ensures
m.values().finite(),