Function hash_set_inv 

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

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

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