pub broadcast proof fn axiom_slice_get_usize<T>(v: &[T], i: usize)Expand description
ensures
i < v.len() ==> #[trigger] spec_slice_get(v, i) == Some(&v[i as int]),i >= v.len() ==> spec_slice_get(v, i).is_none(),