Function lemma_option_obeys_cmp_spec Copy item path

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

obeys_cmp::<T>(),

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