lemma_project_first_key_finite

vstd_extra::map_extra

Function lemma_project_first_key_finite 

Source 
pub proof fn lemma_project_first_key_finite<K1, K2, V>(m: Map<(K1, K2), V>, k1: K1)
Expand description
requires
m.dom().finite(),
ensures
project_first_key(m, k1).dom().finite(),

If the original map is finite, then the projected map is also finite.