Function hash_map_entry_ensures 

pub open spec fn hash_map_entry_ensures<Key: Eq + Hash, Value, S: BuildHasher, A: Allocator>(
    old_m: &HashMap<Key, Value, S, A>,
    final_m: &HashMap<Key, Value, S, A>,
    key: Key,
    entry: Entry<'_, Key, Value, A>,
) -> bool

{
    ({
        &&& obeys_key_model::<Key>()
        &&& builds_valid_hashers::<S>()
        &&& hash_map_inv(old_m)

    })
        ==> {
            &&& hash_map_inv(final_m)
            &&& match entry {
                Entry::Occupied(occupied_entry) => (
                    &&& old_m@.contains_key(occupied_entry.spec_key())
                    &&& key.eq_spec(&occupied_entry.spec_key())
                    &&& occupied_entry.value() == old_m@[occupied_entry.spec_key()]

                ),
                Entry::Vacant(vacant_entry) => (
                    &&& vacant_entry.spec_key() == key
                    &&& forall |stored_key: Key| (
                        #[trigger] old_m@.contains_key(stored_key)
                            ==> !key.eq_spec(&stored_key)
                    )

                ),
            }
            &&& final_m@
                == match entry.final_value() {
                    Some(value) => old_m@.insert(entry.spec_key(), value),
                    None => old_m@.remove(entry.spec_key()),
                }

        }
}