Function vstd::map::axiom_map_index_decreases_finite

source · 
pub broadcast proof fn axiom_map_index_decreases_finite<K, V>(m: Map<K, V>, key: K)
Expand description
requires
m.dom().finite(),
m.dom().contains(key),
ensures
#[trigger] (decreases_to!(m => m[key])),