pub broadcast proof fn lemma_imap_remove_different<K, V>(m: IMap<K, V>, key1: K, key2: K)Expand description
requires
key1 != key2,#[trigger] m.remove(key2)[key1] == m[key1],Removing a key-value pair from a map does not change the value mapped to by any other keys in the map.