Function lemma_identity_vec_view 

pub broadcast proof fn lemma_identity_vec_view<T: DeepView<V = T>>(values: &Vec<T>)

requires

forall |item: T| #[trigger] item.deep_view() == item,

ensures

#[trigger] values.deep_view() == values@,

Identity-view elements give a vector the same shallow and deep views.