pub broadcast proof fn lemma_option_obeys_deep_eq<T: PartialEq + DeepView>()
Expand description
requires
obeys_deep_eq::<T>(),
ensures#[trigger] obeys_deep_eq::<Option<T>>(),