Function lemma_map_remove_keys_finite Copy item path

pub broadcast proof fn lemma_map_remove_keys_finite<K, V>(m: Map<K, V>, keys: Set<K>)

m.dom().finite(),

keys.finite(),

(#[trigger] m.remove_keys(keys)).dom().finite(),