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