pub broadcast proof fn axiom_slice_has_resolved<T>(slice: &[T], i: int)Expand description
ensures
0 <= i < spec_slice_len(slice)
==> (#[trigger] has_resolved_unsized::<[T]>(slice)
==> has_resolved(#[trigger] slice@[i])),