Function lemma_option_obeys_eq_spec Copy item path

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

obeys_eq::<T>(),

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