Function lemma_union_insert_right Copy item path

pub broadcast proof fn lemma_union_insert_right<K, V>(
    m1: IMap<K, V>,
    m2: IMap<K, V>,
    k: K,
    v: V,
)

#[trigger] m1.union_prefer_right(m2.insert(k, v))
    == m1.union_prefer_right(m2).insert(k, v),