vstd::laws_cmp

Function lemma_option_obeys_cmp_spec

Source 
pub broadcast proof fn lemma_option_obeys_cmp_spec<T: Ord>()
Expand description
requires
obeys_cmp_spec::<T>(),
ensures
#[trigger] obeys_cmp_spec::<Option<T>>(),