Function hash_map_remove_ensures 

pub open spec fn hash_map_remove_ensures<Key: Borrow<Q> + Hash + Eq, Value, S: BuildHasher, A: Allocator, Q: Hash + Eq + ?Sized>(
    old_m: &HashMap<Key, Value, S, A>,
    final_m: &HashMap<Key, Value, S, A>,
    k: &Q,
    result: Option<Value>,
) -> bool

{
    ({
        &&& obeys_key_model::<Key>()
        &&& obeys_key_model::<Q>()
        &&& builds_valid_hashers::<S>()
        &&& <Key as BorrowSpec<Q>>::obeys_borrow_spec()
        &&& hash_map_inv(old_m)

    })
        ==> {
            &&& hash_map_inv(final_m)
            &&& match result {
                Some(v) => {
                    exists |key: Key| {
                        &&& #[trigger] old_m@.contains_key(key)
                        &&& k.eq_spec(<Key as BorrowSpec<Q>>::borrow_spec(&key))
                        &&& old_m@[key] == v
                        &&& final_m@ == old_m@.remove(key)

                    }
                }
                None => (
                    &&& forall |key: Key| (
                        #[trigger] old_m@.contains_key(key)
                            ==> !k.eq_spec(<Key as BorrowSpec<Q>>::borrow_spec(&key))
                    )
                    &&& final_m@ == old_m@

                ),
            }

        }
}