Function hash_map_inv 

pub open spec fn hash_map_inv<Key: Eq + Hash, Value, S, A: Allocator>(
    m: &HashMap<Key, Value, S, A>,
) -> bool

{
    forall |k1: Key, k2: Key| (
        {
            &&& #[trigger] m@.contains_key(k1)
            &&& #[trigger] m@.contains_key(k2)
            &&& k1 != k2

        } ==> !k1.eq_spec(&k2)
    )
}