pub proof fn lemma_map_insert_len<K, V>(m: Map<K, V>, k: K, v: V)Expand description
requires
m.dom().finite(),#[trigger] m.insert(k, v).len() == m.len() + (if m.contains_key(k) { 0int } else { 1 }),The length of inserting a key-value pair (k,v) into a map m depends on whether
the key k already exists in the map. If it does, the length remains the same;
if it doesn’t, the length increases by 1.