lemma_ref_obeys_deep_eq

vstd::laws_eq

Function lemma_ref_obeys_deep_eq 

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