Function lemma_union_remove_left

pub broadcast proof fn lemma_union_remove_left<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.remove(k).union_prefer_right(m2),

Function lemma_union_remove_leftCopy item path