pub broadcast proof fn lemma_imap_empty<K, V>()Expand description
ensures
#[trigger] IMap::<K, V>::empty().dom() == ISet::<K>::empty(),The domain of the empty map is the empty set
pub broadcast proof fn lemma_imap_empty<K, V>()#[trigger] IMap::<K, V>::empty().dom() == ISet::<K>::empty(),The domain of the empty map is the empty set