Function hash_set_contains_ensures 

pub open spec fn hash_set_contains_ensures<Key: Borrow<Q> + Hash + Eq, S: BuildHasher, A: Allocator, Q: Hash + Eq + ?Sized>(
    m: &HashSet<Key, S, A>,
    k: &Q,
    result: bool,
) -> bool

{
    ({
        &&& obeys_key_model::<Key>()
        &&& obeys_key_model::<Q>()
        &&& builds_valid_hashers::<S>()
        &&& <Key as BorrowSpec<Q>>::obeys_borrow_spec()
        &&& hash_set_inv(m)

    })
        ==> {
            result
                == exists |key: Key| {
                    &&& #[trigger] m@.contains(key)
                    &&& k.eq_spec(<Key as BorrowSpec<Q>>::borrow_spec(&key))

                }
        }
}