pub broadcast proof fn axiom_vec_has_resolved<T>(vec: Vec<T>, i: int)Expand description
ensures
0 <= i < vec.len()
==> (#[trigger] has_resolved::<Vec<T>>(vec) ==> has_resolved(#[trigger] vec@[i])),