Function vstd::map_lib::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(),