Function lemma_option_obeys_concrete_eq

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

Expand description

requires

obeys_concrete_eq::<T>(),

ensures

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

Function lemma_option_obeys_concrete_eqCopy item path