Function vstd::map_lib::lemma_union_dom

source · 
pub broadcast proof fn lemma_union_dom<K, V>(m1: Map<K, V>, m2: Map<K, V>)
Expand description
ensures
#[trigger] m1.union_prefer_right(m2).dom() == m1.dom().union(m2.dom()),