pub broadcast proof fn axiom_vec_decreases_to_view<T>(v: Vec<T>)
#[trigger] (decreases_to!(v => v @)),