pub broadcast proof fn lemma_imap_remove_domain<K, V>(m: IMap<K, V>, key: K)Expand description
ensures
#[trigger] m.remove(key).dom() == m.dom().remove(key),The domain of a map after removing a key-value pair is equivalent to removing the key from the original map’s domain set.