pub broadcast proof fn axiom_deref_key_ordering_matches<Key: Ord>()Expand description
ensures
#[trigger] borrowed_key_ordering_matches::<Key, Key>(),A key type has the same ordering as itself.