Function axiom_borrowed_key_hashing_matches_ref 

pub broadcast proof fn axiom_borrowed_key_hashing_matches_ref<Q: Hash + Eq + ?Sized>()

ensures

#[trigger] borrowed_key_hashing_matches::<&Q, Q>(),