pub broadcast proof fn axiom_deref_key_cmp<Key: Ord>(stored_key: Key, key: &Key)Expand description
ensures
#[trigger] borrowed_key_cmp::<Key, Key>(stored_key, key) == stored_key.cmp_spec(key),Comparing a stored key against a borrowed key of the same type agrees with Ord’s model.