Function lemma_vec_obeys_view_eq

pub broadcast proof fn lemma_vec_obeys_view_eq<T: PartialEq + View>()

Expand description

requires

super::super::laws_eq::obeys_concrete_eq::<T>(),

ensures

#[trigger] super::super::laws_eq::obeys_view_eq::<Vec<T>>(),

Function lemma_vec_obeys_view_eqCopy item path