Function lemma_option_obeys_eq_spec

pub broadcast proof fn lemma_option_obeys_eq_spec<T: PartialEq>()

Expand description

requires

obeys_eq_spec::<T>(),

ensures

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

Function lemma_option_obeys_eq_specCopy item path