Function lemma_ref_obeys_cmp_spec Copy item path

pub broadcast proof fn lemma_ref_obeys_cmp_spec<T: Ord>()

obeys_cmp::<T>(),

#[trigger] obeys_cmp::<&T>(),