Function borrowed_key_hashing_matches 

pub uninterp spec fn borrowed_key_hashing_matches<Key: Borrow<Q> + Hash + Eq + ?Sized, Q: Hash + Eq + ?Sized>() -> bool

Whether borrowing a key preserves its Hash and Eq behavior.

Owned keys and their borrowed forms must hash identically for any hasher and compare equal in the same circumstances. This predicate is opaque because Hash does not yet have a specification model.