Function axiom_borrowed_key_hashing_matches_box 

pub broadcast proof fn axiom_borrowed_key_hashing_matches_box<Q: Hash + Eq + ?Sized, A: Allocator>()

ensures

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