Function axiom_borrowed_key_hashing_matches_self 

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

ensures

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