pub broadcast proof fn axiom_key_obeys_cmp_spec_meaning<K: Ord>()Expand description
ensures
#[trigger] key_obeys_cmp_spec::<K>() <==> obeys_cmp_spec::<K>(),For types that are ordered, key_obeys_cmp_spec is equivalent to obeys_cmp_spec.