vstd::map

Function axiom_map_empty

Source 
pub broadcast proof fn axiom_map_empty<K, V>()
Expand description
ensures
#[trigger] Map::<K, V>::empty().dom() == Set::<K>::empty(),

The domain of the empty map is the empty set