vstd::map_lib

Function lemma_union_remove_right

Source 
pub broadcast proof fn lemma_union_remove_right<K, V>(m1: Map<K, V>, m2: Map<K, V>, k: K)
Expand description
requires
!m1.contains_key(k),
m2.contains_key(k),
ensures
#[trigger] m1.union_prefer_right(m2).remove(k) == m1.union_prefer_right(m2.remove(k)),