Function vstd::map_lib::lemma_union_insert_right

source · 
pub broadcast proof fn lemma_union_insert_right<K, V>(m1: Map<K, V>, m2: Map<K, V>, k: K, v: V)
Expand description
ensures
#[trigger] m1.union_prefer_right(m2.insert(k, v))
    == m1.union_prefer_right(m2).insert(k, v),