Function lemma_borrowed_key_mutated_deref 

pub broadcast proof fn lemma_borrowed_key_mutated_deref<Key, Value>(
    old_map: Map<Key, Value>,
    new_map: Map<Key, Value>,
    key: &Key,
    old_value: Value,
    new_value: Value,
)

ensures

#[trigger] borrowed_key_mutated(old_map, new_map, key, old_value, new_value)
    <==> {
        &&& old_map.contains_key(*key)
        &&& old_map[*key] == old_value
        &&& new_map == old_map.insert(*key, new_value)

    },

Simplifies borrowed_key_mutated when the borrowed key has the map’s key type.