pub broadcast proof fn lemma_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
pub broadcast proof fn lemma_map_empty<K, V>()#[trigger] Map::<K, V>::empty().dom() == Set::<K>::empty(),The domain of the empty map is the empty set