Function vstd::map::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