diff --git a/source/rust_verify/src/rust_to_vir_func.rs b/source/rust_verify/src/rust_to_vir_func.rs
index ec41f1325..c23f5dc67 100644
--- a/source/rust_verify/src/rust_to_vir_func.rs
+++ b/source/rust_verify/src/rust_to_vir_func.rs
@@ -1389,7 +1389,13 @@ pub(crate) fn remove_ignored_trait_bounds_from_predicates<'tcx>(
     use rustc_middle::ty::{ConstKind, ScalarInt, ValTree};
     preds.retain(|p: &Clause<'tcx>| match p.kind().skip_binder() {
         rustc_middle::ty::ClauseKind::<'tcx>::Trait(tp) => {
-            if in_trait && trait_ids.contains(&tp.trait_ref.def_id) && tp.trait_ref.args.len() >= 1
+            // Skip private trait bounds
+            let path = tcx.def_path_str(tp.trait_ref.def_id);
+            if path == "core::slice::index::private_slice_index::Sealed" {
+                false
+            } else if in_trait
+                && trait_ids.contains(&tp.trait_ref.def_id)
+                && tp.trait_ref.args.len() >= 1
             {
                 if let GenericArgKind::Type(ty) = tp.trait_ref.args[0].unpack() {
                     match ty.kind() {
diff --git a/source/vstd/slice.rs b/source/vstd/slice.rs
index 15384444b..2955c710e 100644
--- a/source/vstd/slice.rs
+++ b/source/vstd/slice.rs
@@ -103,8 +103,36 @@ pub exec fn slice_subrange<T, 'a>(slice: &'a [T], i: usize, j: usize) -> (out: &
     &slice[i..j]
 }
 
+#[verifier::external_trait_specification]
+pub trait ExSliceIndex<T> where T: ?Sized {
+    type ExternalTraitSpecificationFor: core::slice::SliceIndex<T>;
+
+    type Output: ?Sized;
+}
+
+pub assume_specification<T, I>[ <[T]>::get::<I> ](slice: &[T], i: I) -> (b: Option<
+    &<I as core::slice::SliceIndex<[T]>>::Output,
+>) where I: core::slice::SliceIndex<[T]>
+    returns
+        spec_slice_get(slice, i),
+;
+
+pub open spec fn spec_slice_get<T: ?Sized, I: core::slice::SliceIndex<T>>(
+    val: &T,
+    idx: I,
+) -> Option<&<I as core::slice::SliceIndex<T>>::Output>;
+
+pub broadcast proof fn axiom_slice_get_usize<T>(v: &[T], i: usize)
+    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(),
+{
+    admit();
+}
+
 pub broadcast group group_slice_axioms {
     axiom_spec_len,
+    axiom_slice_get_usize,
 }
 
 } // verus!