lemma_project_first_key_sound

vstd_extra::map_extra

Function lemma_project_first_key_sound 

Source 
pub proof fn lemma_project_first_key_sound<K1, K2, V>(m: Map<(K1, K2), V>, k1: K1)
Expand description
ensures
forall |k2: K2| {
    &&& #[trigger] project_first_key(m, k1).contains_key(k2)
        <==> m.contains_key((k1, k2))
    &&& project_first_key(m, k1).contains_key(k2)
        ==> project_first_key(m, k1)[k2] == m[(k1, k2)]

},

A lemma showing that `project_first_key`` is sound. There is no need to actually use this lemma in practice at most of the time because Verus can automatically prove it.