diff --git a/creusot-contracts/src/ghost.rs b/creusot-contracts/src/ghost.rs
index bc522e0ace..f9fae61c9d 100644
--- a/creusot-contracts/src/ghost.rs
+++ b/creusot-contracts/src/ghost.rs
@@ -11,6 +11,7 @@ impl<T: ?Sized> Deref for Ghost<T> {
     #[trusted]
     #[ghost]
     #[open(self)]
+    #[rustc_diagnostic_item = "ghost_deref"]
     #[creusot::builtins = "prelude.Ghost.inner"]
     fn deref(&self) -> &Self::Target {
         pearlite! { absurd }
@@ -47,6 +48,7 @@ impl<T: ?Sized> Ghost<T> {
     #[trusted]
     #[ghost]
     #[open(self)]
+    #[rustc_diagnostic_item = "ghost_inner"]
     #[creusot::builtins = "prelude.Ghost.inner"]
     pub fn inner(self) -> T
     where
diff --git a/creusot-contracts/src/logic/ops.rs b/creusot-contracts/src/logic/ops.rs
index 1d6afbfac1..f4fba661e3 100644
--- a/creusot-contracts/src/logic/ops.rs
+++ b/creusot-contracts/src/logic/ops.rs
@@ -6,6 +6,7 @@ pub trait IndexLogic<I> {
     type Item;
 
     #[ghost]
+    #[rustc_diagnostic_item = "index_logic_method"]
     fn index_logic(self, idx: I) -> Self::Item;
 }
 
diff --git a/creusot/src/translation/pearlite.rs b/creusot/src/translation/pearlite.rs
index e6275cc4ef..15474d0704 100644
--- a/creusot/src/translation/pearlite.rs
+++ b/creusot/src/translation/pearlite.rs
@@ -5,12 +5,16 @@
 // Transforms THIR into a Term which may be serialized in Creusot metadata files for usage by dependent crates
 // The `lower` module then transforms a `Term` into a WhyML expression.
 
-use std::collections::HashSet;
+use std::{
+    collections::HashSet,
+    fmt::{Display, Formatter},
+    unreachable,
+};
 
 use crate::{
     error::{CrErr, CreusotResult, Error},
     translation::TranslationCtx,
-    util,
+    util::{self, is_ghost_ty},
 };
 use itertools::Itertools;
 use log::*;
@@ -27,8 +31,8 @@ use rustc_middle::{
         AdtExpr, ArmId, Block, ClosureExpr, ExprId, ExprKind, Pat, PatKind, StmtId, StmtKind, Thir,
     },
     ty::{
-        int_ty, subst::SubstsRef, uint_ty, Ty, TyCtxt, TyKind, TypeFoldable, TypeVisitable,
-        UpvarSubsts,
+        int_ty, subst::SubstsRef, uint_ty, GenericArg, Ty, TyCtxt, TyKind, TypeFoldable,
+        TypeVisitable, UpvarSubsts,
     },
 };
 use rustc_serialize::{Decodable, Decoder, Encodable, Encoder};
@@ -485,7 +489,11 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> {
                     }
                 }
             }
-            ExprKind::Borrow { borrow_kind: BorrowKind::Shared, arg } => self.expr_term(arg),
+            ExprKind::Borrow { borrow_kind: BorrowKind::Shared, arg } => {
+                let mut e = self.expr_term(arg)?;
+                e.ty = ty;
+                Ok(e)
+            }
             ExprKind::Borrow { arg, .. } => {
                 let t = self.logical_reborrow(arg)?;
                 Ok(Term { ty, span, kind: t })
@@ -798,6 +806,7 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> {
         if let ExprKind::Deref { arg } = self.thir[rebor_id].kind {
             return Ok(self.expr_term(arg)?.kind);
         };
+        // eprintln!("{}", PrintExpr(self.thir, rebor_id));
         // Handle every other case.
         let (cur, fin) = self.logical_reborrow_inner(rebor_id)?;
 
@@ -822,22 +831,77 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> {
                 ))
             }
             ExprKind::Deref { arg } => {
+                // Detect * ghost_deref & and treat that as a single 'projection'
+                if self.is_ghost_deref(*arg) {
+                    let ExprKind::Call { args, .. } = &self.thir[*arg].kind else { unreachable!() };
+                    let ExprKind::Borrow { borrow_kind: BorrowKind::Shared, arg } = self.thir[args[0]].kind else { unreachable!() };
+
+                    let (cur, fin) = self.logical_reborrow_inner(arg)?;
+                    let deref_method =
+                        self.ctx.get_diagnostic_item(Symbol::intern("ghost_inner")).unwrap();
+                    // Extract the `T` from `Ghost<T>`
+                    let TyKind::Adt(_, subst) = self.thir[arg].ty.peel_refs().kind() else {unreachable!()};
+                    return Ok((
+                        Term::call(self.ctx.tcx, deref_method, subst, vec![cur]),
+                        Term::call(self.ctx.tcx, deref_method, subst, vec![fin]),
+                    ));
+                };
+
                 let inner = self.expr_term(*arg)?;
-                if let TermKind::Var(_) = inner.kind {}
-                let ty = inner.ty.builtin_deref(false).expect("expected reference type").ty;
 
-                Ok((
-                    Term { ty, span, kind: TermKind::Cur { term: Box::new(inner.clone()) } },
-                    Term { ty, span, kind: TermKind::Fin { term: Box::new(inner) } },
-                ))
+                Ok((inner.clone().cur().span(span), inner.fin().span(span)))
+            }
+            ExprKind::Call { ty: fn_ty, args, .. } if fn_ty.is_fn() => {
+                let index_logic_method =
+                    self.ctx.get_diagnostic_item(Symbol::intern("index_logic_method")).unwrap();
+
+                let TyKind::FnDef(id,_) = fn_ty.kind() else { panic!("expected function type") };
+
+                let (cur, fin) = self.logical_reborrow_inner(args[0])?;
+
+                if id == &index_logic_method {
+                    let index = self.expr_term(args[1])?;
+
+                    let subst =
+                        self.ctx.mk_substs(&[GenericArg::from(cur.ty), GenericArg::from(index.ty)]);
+
+                    Ok((
+                        Term::call(
+                            self.ctx.tcx,
+                            index_logic_method,
+                            subst,
+                            vec![cur, index.clone()],
+                        ),
+                        Term::call(
+                            self.ctx.tcx,
+                            index_logic_method,
+                            subst,
+                            vec![fin, index.clone()],
+                        ),
+                    ))
+                } else {
+                    return Err(Error::new(span, format!("unsupported projection {id:?}")));
+                }
             }
-            _ => Err(Error::new(
+            e => Err(Error::new(
                 span,
-                "unsupported logical reborrow, only simple field projections are supproted, sorry",
+                format!("unsupported logical reborrow {e:?}, only simple field projections are supported"),
             )),
         }
     }
 
+    pub(crate) fn is_ghost_deref(&self, expr_id: ExprId) -> bool {
+        let ExprKind::Call { ty, .. } = &self.thir[expr_id].kind else {return false};
+
+        let TyKind::FnDef(id, sub) = ty.kind() else { panic!("expected function type") };
+
+        if Some(*id) != self.ctx.get_diagnostic_item(Symbol::intern("deref_method")) {
+            return false;
+        }
+
+        sub[0].as_type().map(|ty| is_ghost_ty(self.ctx.tcx, ty)).unwrap_or(false)
+    }
+
     fn mk_projection(&self, lhs: Term<'tcx>, name: FieldIdx) -> Result<TermKind<'tcx>, Error> {
         let pat = field_pattern(lhs.ty, name).expect("mk_projection: no term for field");
 
@@ -1121,6 +1185,27 @@ impl<'tcx> Term<'tcx> {
         Term { ty: tcx.types.bool, kind: TermKind::Lit(Literal::Bool(false)), span: DUMMY_SP }
     }
 
+    pub(crate) fn call(
+        tcx: TyCtxt<'tcx>,
+        def_id: DefId,
+        subst: SubstsRef<'tcx>,
+        args: Vec<Term<'tcx>>,
+    ) -> Self {
+        let ty = tcx.type_of(def_id).subst(tcx, subst);
+        let result = ty.fn_sig(tcx).skip_binder().output();
+        let fun = Term {
+            ty: tcx.type_of(def_id).subst(tcx, subst),
+            kind: TermKind::Item(def_id, subst),
+            span: DUMMY_SP,
+        };
+
+        Term {
+            ty: result,
+            span: DUMMY_SP,
+            kind: TermKind::Call { id: def_id, subst, fun: Box::new(fun.clone()), args },
+        }
+    }
+
     pub(crate) fn var(sym: Symbol, ty: Ty<'tcx>) -> Self {
         Term { ty, kind: TermKind::Var(sym), span: DUMMY_SP }
     }
@@ -1439,3 +1524,84 @@ impl<'tcx> Term<'tcx> {
         }
     }
 }
+
+struct PrintExpr<'a, 'tcx>(&'a Thir<'tcx>, ExprId);
+
+impl Display for PrintExpr<'_, '_> {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+        print_thir_expr(f, self.0, self.1)
+    }
+}
+
+fn print_thir_expr<'tcx>(
+    fmt: &mut Formatter,
+    thir: &Thir<'tcx>,
+    expr_id: ExprId,
+) -> std::fmt::Result {
+    match &thir[expr_id].kind {
+        ExprKind::Call { fun, args, .. } => {
+            print_thir_expr(fmt, thir, *fun)?;
+            write!(fmt, "(")?;
+            for a in args.iter() {
+                print_thir_expr(fmt, thir, *a)?;
+                write!(fmt, ",")?;
+            }
+            write!(fmt, ")")?;
+        }
+        ExprKind::Deref { arg } => {
+            write!(fmt, "* ")?;
+            print_thir_expr(fmt, thir, *arg)?;
+        }
+        ExprKind::Borrow { borrow_kind, arg } => {
+            match borrow_kind {
+                BorrowKind::Shared => write!(fmt, "& ")?,
+                BorrowKind::Shallow => write!(fmt, "&shallow ")?,
+                BorrowKind::Mut { .. } => write!(fmt, "&mut ")?,
+            };
+
+            print_thir_expr(fmt, thir, *arg)?;
+        }
+        ExprKind::Field { lhs, variant_index, name } => {
+            print_thir_expr(fmt, thir, *lhs)?;
+            let ty = thir[expr_id].ty;
+            let (var_name, field_name) = match ty.kind() {
+                TyKind::Adt(def, _) => {
+                    let var = &def.variants()[*variant_index];
+                    (var.name.to_string(), var.fields[*name].name.to_string())
+                }
+                TyKind::Tuple(_) => ("_".into(), format!("{name:?}")),
+                _ => unreachable!(),
+            };
+
+            write!(fmt, " as {var_name} . {field_name}")?;
+        }
+        ExprKind::Index { lhs, index } => {
+            print_thir_expr(fmt, thir, *lhs)?;
+            write!(fmt, "[")?;
+            print_thir_expr(fmt, thir, *index)?;
+            write!(fmt, "]")?;
+        }
+        ExprKind::ZstLiteral { .. } => match thir[expr_id].ty.kind() {
+            TyKind::FnDef(id, _) => write!(fmt, "{id:?}")?,
+            _ => write!(fmt, "zst")?,
+        },
+        ExprKind::Literal { lit, neg } => {
+            if *neg {
+                write!(fmt, "-")?;
+            }
+
+            write!(fmt, "{}", lit.node)?;
+        }
+        ExprKind::Use { source } => print_thir_expr(fmt, thir, *source)?,
+        ExprKind::VarRef { id } => {
+            write!(fmt, "{:?}", id.0)?;
+        }
+        ExprKind::Scope { value, .. } => {
+            print_thir_expr(fmt, thir, *value)?;
+        }
+        _ => {
+            write!(fmt, "{:?}", thir[expr_id])?;
+        }
+    }
+    Ok(())
+}
diff --git a/creusot/src/translation/specification.rs b/creusot/src/translation/specification.rs
index 6a0e31c897..81359f40b2 100644
--- a/creusot/src/translation/specification.rs
+++ b/creusot/src/translation/specification.rs
@@ -304,6 +304,7 @@ pub(crate) fn is_overloaded_item(tcx: TyCtxt, def_id: DefId) -> bool {
         || def_path.ends_with("::ops::Neg::neg")
         || def_path.ends_with("::boxed::Box::<T>::new")
         || def_path.ends_with("::ops::Deref::deref")
+        || def_path.ends_with("::ops::DerefMut::deref_mut")
         || def_path.ends_with("Ghost::<T>::from_fn")
 }
 
diff --git a/creusot/tests/should_succeed/100doors.mlcfg b/creusot/tests/should_succeed/100doors.mlcfg
index 75c56e956e..58becfd3b1 100644
--- a/creusot/tests/should_succeed/100doors.mlcfg
+++ b/creusot/tests/should_succeed/100doors.mlcfg
@@ -272,7 +272,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/bug/874.mlcfg b/creusot/tests/should_succeed/bug/874.mlcfg
index fb42317fe7..651d528bc0 100644
--- a/creusot/tests/should_succeed/bug/874.mlcfg
+++ b/creusot/tests/should_succeed/bug/874.mlcfg
@@ -164,7 +164,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/bug/two_phase.mlcfg b/creusot/tests/should_succeed/bug/two_phase.mlcfg
index 03ab3ab23e..152dcb1e12 100644
--- a/creusot/tests/should_succeed/bug/two_phase.mlcfg
+++ b/creusot/tests/should_succeed/bug/two_phase.mlcfg
@@ -218,7 +218,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/cell/02.mlcfg b/creusot/tests/should_succeed/cell/02.mlcfg
index c9319eff17..d964f898b2 100644
--- a/creusot/tests/should_succeed/cell/02.mlcfg
+++ b/creusot/tests/should_succeed/cell/02.mlcfg
@@ -417,7 +417,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/filter_positive.mlcfg b/creusot/tests/should_succeed/filter_positive.mlcfg
index 095aaab518..d4064ba598 100644
--- a/creusot/tests/should_succeed/filter_positive.mlcfg
+++ b/creusot/tests/should_succeed/filter_positive.mlcfg
@@ -319,7 +319,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/hashmap.mlcfg b/creusot/tests/should_succeed/hashmap.mlcfg
index f86ab5c13f..a9dec272cc 100644
--- a/creusot/tests/should_succeed/hashmap.mlcfg
+++ b/creusot/tests/should_succeed/hashmap.mlcfg
@@ -527,7 +527,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
@@ -2368,7 +2368,7 @@ module CreusotContracts_Ghost_Impl1_ShallowModel
     type t = t,
     type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
   function shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy =
-    [#"../../../../creusot-contracts/src/ghost.rs" 26 20 26 48] ShallowModel0.shallow_model (Ghost.inner self)
+    [#"../../../../creusot-contracts/src/ghost.rs" 27 20 27 48] ShallowModel0.shallow_model (Ghost.inner self)
   val shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy
     ensures { result = shallow_model self }
     
diff --git a/creusot/tests/should_succeed/heapsort_generic.mlcfg b/creusot/tests/should_succeed/heapsort_generic.mlcfg
index 8e2de7131b..29b67d0337 100644
--- a/creusot/tests/should_succeed/heapsort_generic.mlcfg
+++ b/creusot/tests/should_succeed/heapsort_generic.mlcfg
@@ -1004,7 +1004,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
@@ -1221,7 +1221,7 @@ module CreusotContracts_Ghost_Impl1_ShallowModel
     type t = t,
     type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
   function shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy =
-    [#"../../../../creusot-contracts/src/ghost.rs" 26 20 26 48] ShallowModel0.shallow_model (Ghost.inner self)
+    [#"../../../../creusot-contracts/src/ghost.rs" 27 20 27 48] ShallowModel0.shallow_model (Ghost.inner self)
   val shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy
     ensures { result = shallow_model self }
     
diff --git a/creusot/tests/should_succeed/hillel.mlcfg b/creusot/tests/should_succeed/hillel.mlcfg
index 424bd4dadc..6951c4d9ca 100644
--- a/creusot/tests/should_succeed/hillel.mlcfg
+++ b/creusot/tests/should_succeed/hillel.mlcfg
@@ -218,7 +218,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
@@ -303,7 +303,7 @@ module CreusotContracts_Ghost_Impl1_ShallowModel
     type t = t,
     type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
   function shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy =
-    [#"../../../../creusot-contracts/src/ghost.rs" 26 20 26 48] ShallowModel0.shallow_model (Ghost.inner self)
+    [#"../../../../creusot-contracts/src/ghost.rs" 27 20 27 48] ShallowModel0.shallow_model (Ghost.inner self)
   val shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy
     ensures { result = shallow_model self }
     
@@ -1337,7 +1337,7 @@ module CreusotContracts_Logic_Ops_Impl2_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : slice t) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 41 8 41 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 42 8 42 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : slice t) (ix : int) : t
     ensures { result = index_logic self ix }
     
@@ -1487,7 +1487,7 @@ module CreusotContracts_Logic_Ops_Impl6_IndexLogic
   use seq.Seq
   use prelude.Int
   function index_logic [@inline:trivial] (self : Ghost.ghost_ty (Seq.seq t)) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 85 8 85 33] Seq.get (Ghost.inner self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 86 8 86 33] Seq.get (Ghost.inner self) ix
   val index_logic [@inline:trivial] (self : Ghost.ghost_ty (Seq.seq t)) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/index_range.mlcfg b/creusot/tests/should_succeed/index_range.mlcfg
index b06feb085f..d1945ba539 100644
--- a/creusot/tests/should_succeed/index_range.mlcfg
+++ b/creusot/tests/should_succeed/index_range.mlcfg
@@ -159,7 +159,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/invariant_moves.mlcfg b/creusot/tests/should_succeed/invariant_moves.mlcfg
index 2dbf76b626..2c504e9eca 100644
--- a/creusot/tests/should_succeed/invariant_moves.mlcfg
+++ b/creusot/tests/should_succeed/invariant_moves.mlcfg
@@ -186,7 +186,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg b/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg
index e94ee1597c..64ec75f860 100644
--- a/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg
+++ b/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg
@@ -282,7 +282,7 @@ module CreusotContracts_Logic_Ops_Impl2_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : slice t) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 41 8 41 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 42 8 42 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : slice t) (ix : int) : t
     ensures { result = index_logic self ix }
     
@@ -1648,7 +1648,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
@@ -1676,7 +1676,7 @@ module CreusotContracts_Logic_Ops_Impl6_IndexLogic
   use seq.Seq
   use prelude.Int
   function index_logic [@inline:trivial] (self : Ghost.ghost_ty (Seq.seq t)) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 85 8 85 33] Seq.get (Ghost.inner self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 86 8 86 33] Seq.get (Ghost.inner self) ix
   val index_logic [@inline:trivial] (self : Ghost.ghost_ty (Seq.seq t)) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg b/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg
index b40f364b2b..70ad72afd5 100644
--- a/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg
+++ b/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg
@@ -244,7 +244,7 @@ module CreusotContracts_Logic_Ops_Impl2_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : slice t) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 41 8 41 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 42 8 42 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : slice t) (ix : int) : t
     ensures { result = index_logic self ix }
     
@@ -1490,7 +1490,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
@@ -1746,7 +1746,7 @@ module CreusotContracts_Logic_Ops_Impl6_IndexLogic
   use seq.Seq
   use prelude.Int
   function index_logic [@inline:trivial] (self : Ghost.ghost_ty (Seq.seq t)) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 85 8 85 33] Seq.get (Ghost.inner self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 86 8 86 33] Seq.get (Ghost.inner self) ix
   val index_logic [@inline:trivial] (self : Ghost.ghost_ty (Seq.seq t)) (ix : int) : t
     ensures { result = index_logic self ix }
     
@@ -6144,7 +6144,7 @@ module CreusotContracts_Ghost_Impl1_ShallowModel
     type t = t,
     type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
   function shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy =
-    [#"../../../../../creusot-contracts/src/ghost.rs" 26 20 26 48] ShallowModel0.shallow_model (Ghost.inner self)
+    [#"../../../../../creusot-contracts/src/ghost.rs" 27 20 27 48] ShallowModel0.shallow_model (Ghost.inner self)
   val shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy
     ensures { result = shallow_model self }
     
diff --git a/creusot/tests/should_succeed/iterators/04_skip.mlcfg b/creusot/tests/should_succeed/iterators/04_skip.mlcfg
index 1fd5392277..4a8b92516e 100644
--- a/creusot/tests/should_succeed/iterators/04_skip.mlcfg
+++ b/creusot/tests/should_succeed/iterators/04_skip.mlcfg
@@ -619,7 +619,7 @@ module CreusotContracts_Logic_Ops_Impl6_IndexLogic
   use seq.Seq
   use prelude.Int
   function index_logic [@inline:trivial] (self : Ghost.ghost_ty (Seq.seq t)) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 85 8 85 33] Seq.get (Ghost.inner self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 86 8 86 33] Seq.get (Ghost.inner self) ix
   val index_logic [@inline:trivial] (self : Ghost.ghost_ty (Seq.seq t)) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/iterators/08_collect_extend.mlcfg b/creusot/tests/should_succeed/iterators/08_collect_extend.mlcfg
index 1a4b747819..23131d644c 100644
--- a/creusot/tests/should_succeed/iterators/08_collect_extend.mlcfg
+++ b/creusot/tests/should_succeed/iterators/08_collect_extend.mlcfg
@@ -313,7 +313,7 @@ module CreusotContracts_Ghost_Impl1_ShallowModel
     type t = t,
     type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
   function shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy =
-    [#"../../../../../creusot-contracts/src/ghost.rs" 26 20 26 48] ShallowModel0.shallow_model (Ghost.inner self)
+    [#"../../../../../creusot-contracts/src/ghost.rs" 27 20 27 48] ShallowModel0.shallow_model (Ghost.inner self)
   val shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy
     ensures { result = shallow_model self }
     
@@ -1011,7 +1011,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/knapsack.mlcfg b/creusot/tests/should_succeed/knapsack.mlcfg
index a6c204c396..a84f28daeb 100644
--- a/creusot/tests/should_succeed/knapsack.mlcfg
+++ b/creusot/tests/should_succeed/knapsack.mlcfg
@@ -371,7 +371,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/knapsack_full.mlcfg b/creusot/tests/should_succeed/knapsack_full.mlcfg
index 89494e0695..e480a00f06 100644
--- a/creusot/tests/should_succeed/knapsack_full.mlcfg
+++ b/creusot/tests/should_succeed/knapsack_full.mlcfg
@@ -626,7 +626,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/list_index_mut.mlcfg b/creusot/tests/should_succeed/list_index_mut.mlcfg
index c0f48c715a..fa4105ae33 100644
--- a/creusot/tests/should_succeed/list_index_mut.mlcfg
+++ b/creusot/tests/should_succeed/list_index_mut.mlcfg
@@ -171,7 +171,7 @@ module CreusotContracts_Ghost_Impl1_ShallowModel
     type t = t,
     type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
   function shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy =
-    [#"../../../../creusot-contracts/src/ghost.rs" 26 20 26 48] ShallowModel0.shallow_model (Ghost.inner self)
+    [#"../../../../creusot-contracts/src/ghost.rs" 27 20 27 48] ShallowModel0.shallow_model (Ghost.inner self)
   val shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy
     ensures { result = shallow_model self }
     
diff --git a/creusot/tests/should_succeed/list_reversal_lasso.mlcfg b/creusot/tests/should_succeed/list_reversal_lasso.mlcfg
index 7da4d52c65..abfcde4a94 100644
--- a/creusot/tests/should_succeed/list_reversal_lasso.mlcfg
+++ b/creusot/tests/should_succeed/list_reversal_lasso.mlcfg
@@ -192,7 +192,7 @@ module CreusotContracts_Logic_Ops_Impl1_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : usize) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 30 8 30 32] Seq.get (ShallowModel0.shallow_model self) (UIntSize.to_int ix)
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 31 8 31 32] Seq.get (ShallowModel0.shallow_model self) (UIntSize.to_int ix)
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : usize) : t
     ensures { result = index_logic self ix }
     
@@ -1437,7 +1437,7 @@ module CreusotContracts_Logic_Ops_Impl6_IndexLogic
   use seq.Seq
   use prelude.Int
   function index_logic [@inline:trivial] (self : Ghost.ghost_ty (Seq.seq t)) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 85 8 85 33] Seq.get (Ghost.inner self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 86 8 86 33] Seq.get (Ghost.inner self) ix
   val index_logic [@inline:trivial] (self : Ghost.ghost_ty (Seq.seq t)) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/mapping_test.mlcfg b/creusot/tests/should_succeed/mapping_test.mlcfg
index 06b88a4c00..070fe77ec2 100644
--- a/creusot/tests/should_succeed/mapping_test.mlcfg
+++ b/creusot/tests/should_succeed/mapping_test.mlcfg
@@ -195,7 +195,7 @@ module CreusotContracts_Ghost_Impl1_ShallowModel
     type t = t,
     type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
   function shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy =
-    [#"../../../../creusot-contracts/src/ghost.rs" 26 20 26 48] ShallowModel0.shallow_model (Ghost.inner self)
+    [#"../../../../creusot-contracts/src/ghost.rs" 27 20 27 48] ShallowModel0.shallow_model (Ghost.inner self)
   val shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy
     ensures { result = shallow_model self }
     
diff --git a/creusot/tests/should_succeed/selection_sort_generic.mlcfg b/creusot/tests/should_succeed/selection_sort_generic.mlcfg
index 5a4069ce17..58c9455e32 100644
--- a/creusot/tests/should_succeed/selection_sort_generic.mlcfg
+++ b/creusot/tests/should_succeed/selection_sort_generic.mlcfg
@@ -287,7 +287,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
@@ -638,7 +638,7 @@ module CreusotContracts_Ghost_Impl1_ShallowModel
     type t = t,
     type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
   function shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy =
-    [#"../../../../creusot-contracts/src/ghost.rs" 26 20 26 48] ShallowModel0.shallow_model (Ghost.inner self)
+    [#"../../../../creusot-contracts/src/ghost.rs" 27 20 27 48] ShallowModel0.shallow_model (Ghost.inner self)
   val shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy
     ensures { result = shallow_model self }
     
diff --git a/creusot/tests/should_succeed/slices/01.mlcfg b/creusot/tests/should_succeed/slices/01.mlcfg
index 9cc8170672..f38cb4b72a 100644
--- a/creusot/tests/should_succeed/slices/01.mlcfg
+++ b/creusot/tests/should_succeed/slices/01.mlcfg
@@ -284,7 +284,7 @@ module CreusotContracts_Logic_Ops_Impl2_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : slice t) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 41 8 41 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 42 8 42 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : slice t) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/slices/02_std.mlcfg b/creusot/tests/should_succeed/slices/02_std.mlcfg
index 45f93c6790..519d6f7041 100644
--- a/creusot/tests/should_succeed/slices/02_std.mlcfg
+++ b/creusot/tests/should_succeed/slices/02_std.mlcfg
@@ -179,7 +179,7 @@ module CreusotContracts_Logic_Ops_Impl2_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : slice t) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 41 8 41 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 42 8 42 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : slice t) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/sparse_array.mlcfg b/creusot/tests/should_succeed/sparse_array.mlcfg
index 8d072c1b63..146f61418b 100644
--- a/creusot/tests/should_succeed/sparse_array.mlcfg
+++ b/creusot/tests/should_succeed/sparse_array.mlcfg
@@ -202,7 +202,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/syntax/05_pearlite.mlcfg b/creusot/tests/should_succeed/syntax/05_pearlite.mlcfg
index d8f25e3b3f..1c5fba79dd 100644
--- a/creusot/tests/should_succeed/syntax/05_pearlite.mlcfg
+++ b/creusot/tests/should_succeed/syntax/05_pearlite.mlcfg
@@ -489,3 +489,372 @@ module C05Pearlite_Proj2
     ensures { result = proj2 x }
     
 end
+module CreusotContracts_Logic_Ops_Impl2_IndexLogic_Stub
+  type t
+  use prelude.Slice
+  use prelude.Int
+  function index_logic [@inline:trivial] (self : slice t) (ix : int) : t
+end
+module CreusotContracts_Logic_Ops_Impl2_IndexLogic_Interface
+  type t
+  use prelude.Slice
+  use prelude.Int
+  function index_logic [@inline:trivial] (self : slice t) (ix : int) : t
+  val index_logic [@inline:trivial] (self : slice t) (ix : int) : t
+    ensures { result = index_logic self ix }
+    
+end
+module CreusotContracts_Logic_Ops_Impl2_IndexLogic
+  type t
+  use prelude.Slice
+  use prelude.Int
+  use seq.Seq
+  use seq.Seq
+  clone CreusotContracts_Invariant_Inv_Stub as Inv1 with
+    type t = Seq.seq t
+  clone Core_Num_Impl11_Max_Stub as Max0
+  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
+    type t = slice t
+  clone CreusotContracts_Std1_Slice_Impl0_ShallowModel_Stub as ShallowModel0 with
+    type t = t,
+    predicate Inv0.inv = Inv0.inv,
+    val Max0.mAX' = Max0.mAX',
+    predicate Inv1.inv = Inv1.inv,
+    axiom .
+  function index_logic [@inline:trivial] (self : slice t) (ix : int) : t =
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 42 8 42 31] Seq.get (ShallowModel0.shallow_model self) ix
+  val index_logic [@inline:trivial] (self : slice t) (ix : int) : t
+    ensures { result = index_logic self ix }
+    
+end
+module C05Pearlite_ReborrowIndexProjection_Stub
+  type t
+  use prelude.Borrow
+  use prelude.Slice
+  function reborrow_index_projection [#"../05_pearlite.rs" 86 0 86 80] (a : borrowed (borrowed (slice t))) : borrowed t
+end
+module C05Pearlite_ReborrowIndexProjection_Interface
+  type t
+  use prelude.Borrow
+  use prelude.Slice
+  function reborrow_index_projection [#"../05_pearlite.rs" 86 0 86 80] (a : borrowed (borrowed (slice t))) : borrowed t
+  val reborrow_index_projection [#"../05_pearlite.rs" 86 0 86 80] (a : borrowed (borrowed (slice t))) : borrowed t
+    ensures { result = reborrow_index_projection a }
+    
+end
+module C05Pearlite_ReborrowIndexProjection
+  type t
+  use prelude.Borrow
+  use prelude.Slice
+  clone CreusotContracts_Logic_Ops_Impl2_IndexLogic_Stub as IndexLogic0 with
+    type t = t
+  function reborrow_index_projection [#"../05_pearlite.rs" 86 0 86 80] (a : borrowed (borrowed (slice t))) : borrowed t
+   =
+    [#"../05_pearlite.rs" 85 0 85 8] {current = IndexLogic0.index_logic ( *  * a) 0; final = IndexLogic0.index_logic ( ^  * a) 0}
+  val reborrow_index_projection [#"../05_pearlite.rs" 86 0 86 80] (a : borrowed (borrowed (slice t))) : borrowed t
+    ensures { result = reborrow_index_projection a }
+    
+end
+module C05Pearlite_ReborrowIndexProjection2_Stub
+  type t
+  use prelude.Borrow
+  use prelude.Slice
+  function reborrow_index_projection2 [#"../05_pearlite.rs" 92 0 92 69] (a : slice t) : t
+end
+module C05Pearlite_ReborrowIndexProjection2_Interface
+  type t
+  use prelude.Borrow
+  use prelude.Slice
+  function reborrow_index_projection2 [#"../05_pearlite.rs" 92 0 92 69] (a : slice t) : t
+  val reborrow_index_projection2 [#"../05_pearlite.rs" 92 0 92 69] (a : slice t) : t
+    ensures { result = reborrow_index_projection2 a }
+    
+end
+module C05Pearlite_ReborrowIndexProjection2
+  type t
+  use prelude.Borrow
+  use prelude.Slice
+  clone CreusotContracts_Logic_Ops_Impl2_IndexLogic_Stub as IndexLogic0 with
+    type t = t
+  function reborrow_index_projection2 [#"../05_pearlite.rs" 92 0 92 69] (a : slice t) : t =
+    [#"../05_pearlite.rs" 91 0 91 8] IndexLogic0.index_logic a 0
+  val reborrow_index_projection2 [#"../05_pearlite.rs" 92 0 92 69] (a : slice t) : t
+    ensures { result = reborrow_index_projection2 a }
+    
+end
+module Core_Ptr_NonNull_NonNull_Type
+  use prelude.Opaque
+  type t_nonnull 't =
+    | C_NonNull opaque_ptr
+    
+end
+module Core_Marker_PhantomData_Type
+  type t_phantomdata 't =
+    | C_PhantomData
+    
+end
+module Core_Ptr_Unique_Unique_Type
+  use Core_Marker_PhantomData_Type as Core_Marker_PhantomData_Type
+  use Core_Ptr_NonNull_NonNull_Type as Core_Ptr_NonNull_NonNull_Type
+  type t_unique 't =
+    | C_Unique (Core_Ptr_NonNull_NonNull_Type.t_nonnull 't) (Core_Marker_PhantomData_Type.t_phantomdata 't)
+    
+end
+module Alloc_RawVec_RawVec_Type
+  use prelude.Int
+  use prelude.UIntSize
+  use Core_Ptr_Unique_Unique_Type as Core_Ptr_Unique_Unique_Type
+  type t_rawvec 't 'a =
+    | C_RawVec (Core_Ptr_Unique_Unique_Type.t_unique 't) usize 'a
+    
+end
+module Alloc_Vec_Vec_Type
+  use prelude.Int
+  use prelude.UIntSize
+  use Alloc_RawVec_RawVec_Type as Alloc_RawVec_RawVec_Type
+  type t_vec 't 'a =
+    | C_Vec (Alloc_RawVec_RawVec_Type.t_rawvec 't 'a) usize
+    
+end
+module Alloc_Alloc_Global_Type
+  type t_global  =
+    | C_Global
+    
+end
+module CreusotContracts_Std1_Vec_Impl0_ShallowModel_Stub
+  type t
+  type a
+  use seq.Seq
+  use prelude.UIntSize
+  use prelude.Int
+  use seq.Seq
+  use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
+  clone CreusotContracts_Invariant_Inv_Stub as Inv1 with
+    type t = Seq.seq t
+  clone Core_Num_Impl11_Max_Stub as Max0
+  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
+    type t = Alloc_Vec_Vec_Type.t_vec t a
+  function shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t
+end
+module CreusotContracts_Std1_Vec_Impl0_ShallowModel_Interface
+  type t
+  type a
+  use seq.Seq
+  use prelude.UIntSize
+  use prelude.Int
+  use seq.Seq
+  use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
+  clone CreusotContracts_Invariant_Inv_Stub as Inv1 with
+    type t = Seq.seq t
+  clone Core_Num_Impl11_Max_Stub as Max0
+  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
+    type t = Alloc_Vec_Vec_Type.t_vec t a
+  function shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t
+  val shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t
+    requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self}
+    ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length result <= UIntSize.to_int Max0.mAX' }
+    ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv result }
+    ensures { result = shallow_model self }
+    
+  axiom shallow_model_spec : forall self : Alloc_Vec_Vec_Type.t_vec t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv (shallow_model self)) && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model self) <= UIntSize.to_int Max0.mAX')
+end
+module CreusotContracts_Std1_Vec_Impl0_ShallowModel
+  type t
+  type a
+  use seq.Seq
+  use prelude.UIntSize
+  use prelude.Int
+  use seq.Seq
+  use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
+  clone CreusotContracts_Invariant_Inv_Stub as Inv1 with
+    type t = Seq.seq t
+  clone Core_Num_Impl11_Max_Stub as Max0
+  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
+    type t = Alloc_Vec_Vec_Type.t_vec t a
+  function shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t
+  val shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t
+    requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self}
+    ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length result <= UIntSize.to_int Max0.mAX' }
+    ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv result }
+    ensures { result = shallow_model self }
+    
+  axiom shallow_model_spec : forall self : Alloc_Vec_Vec_Type.t_vec t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv (shallow_model self)) && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model self) <= UIntSize.to_int Max0.mAX')
+end
+module CreusotContracts_Logic_Ops_Impl0_IndexLogic_Stub
+  type t
+  type a
+  use prelude.Int
+  use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
+  function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
+end
+module CreusotContracts_Logic_Ops_Impl0_IndexLogic_Interface
+  type t
+  type a
+  use prelude.Int
+  use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
+  function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
+  val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
+    ensures { result = index_logic self ix }
+    
+end
+module CreusotContracts_Logic_Ops_Impl0_IndexLogic
+  type t
+  type a
+  use prelude.Int
+  use seq.Seq
+  use seq.Seq
+  clone CreusotContracts_Invariant_Inv_Stub as Inv1 with
+    type t = Seq.seq t
+  clone Core_Num_Impl11_Max_Stub as Max0
+  use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
+  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
+    type t = Alloc_Vec_Vec_Type.t_vec t a
+  clone CreusotContracts_Std1_Vec_Impl0_ShallowModel_Stub as ShallowModel0 with
+    type t = t,
+    type a = a,
+    predicate Inv0.inv = Inv0.inv,
+    val Max0.mAX' = Max0.mAX',
+    predicate Inv1.inv = Inv1.inv,
+    axiom .
+  function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
+  val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
+    ensures { result = index_logic self ix }
+    
+end
+module C05Pearlite_Test3_Stub
+  type t
+  use prelude.Ghost
+  use prelude.Borrow
+  use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
+  use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
+  function test3 [#"../05_pearlite.rs" 98 0 98 58] (a : Ghost.ghost_ty (borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)))) : borrowed t
+    
+end
+module C05Pearlite_Test3_Interface
+  type t
+  use prelude.Ghost
+  use prelude.Borrow
+  use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
+  use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
+  function test3 [#"../05_pearlite.rs" 98 0 98 58] (a : Ghost.ghost_ty (borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)))) : borrowed t
+    
+  val test3 [#"../05_pearlite.rs" 98 0 98 58] (a : Ghost.ghost_ty (borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)))) : borrowed t
+    ensures { result = test3 a }
+    
+end
+module C05Pearlite_Test3
+  type t
+  use prelude.Ghost
+  use prelude.Borrow
+  use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
+  use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
+  clone CreusotContracts_Logic_Ops_Impl0_IndexLogic_Stub as IndexLogic0 with
+    type t = t,
+    type a = Alloc_Alloc_Global_Type.t_global
+  function test3 [#"../05_pearlite.rs" 98 0 98 58] (a : Ghost.ghost_ty (borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)))) : borrowed t
+    
+   =
+    [#"../05_pearlite.rs" 97 0 97 8] {current = IndexLogic0.index_logic ( * Ghost.inner a) 0; final = IndexLogic0.index_logic ( ^ Ghost.inner a) 0}
+  val test3 [#"../05_pearlite.rs" 98 0 98 58] (a : Ghost.ghost_ty (borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)))) : borrowed t
+    ensures { result = test3 a }
+    
+end
+module C05Pearlite_Test4_Stub
+  type t
+  use prelude.Borrow
+  use prelude.Ghost
+  use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
+  use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
+  function test4 [#"../05_pearlite.rs" 104 0 104 58] (a : borrowed (Ghost.ghost_ty (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)))) : borrowed t
+    
+end
+module C05Pearlite_Test4_Interface
+  type t
+  use prelude.Borrow
+  use prelude.Ghost
+  use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
+  use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
+  function test4 [#"../05_pearlite.rs" 104 0 104 58] (a : borrowed (Ghost.ghost_ty (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)))) : borrowed t
+    
+  val test4 [#"../05_pearlite.rs" 104 0 104 58] (a : borrowed (Ghost.ghost_ty (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)))) : borrowed t
+    ensures { result = test4 a }
+    
+end
+module C05Pearlite_Test4
+  type t
+  use prelude.Borrow
+  use prelude.Ghost
+  use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
+  use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
+  clone CreusotContracts_Logic_Ops_Impl0_IndexLogic_Stub as IndexLogic0 with
+    type t = t,
+    type a = Alloc_Alloc_Global_Type.t_global
+  function test4 [#"../05_pearlite.rs" 104 0 104 58] (a : borrowed (Ghost.ghost_ty (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)))) : borrowed t
+    
+   =
+    [#"../05_pearlite.rs" 103 0 103 8] {current = IndexLogic0.index_logic (Ghost.inner ( * a)) 0; final = IndexLogic0.index_logic (Ghost.inner ( ^ a)) 0}
+  val test4 [#"../05_pearlite.rs" 104 0 104 58] (a : borrowed (Ghost.ghost_ty (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)))) : borrowed t
+    ensures { result = test4 a }
+    
+end
+module C05Pearlite_Test5_Stub
+  type t
+  use prelude.Borrow
+  use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
+  use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
+  function test5 [#"../05_pearlite.rs" 110 0 110 61] (a : borrowed (borrowed (borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global))))) : borrowed t
+    
+end
+module C05Pearlite_Test5_Interface
+  type t
+  use prelude.Borrow
+  use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
+  use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
+  function test5 [#"../05_pearlite.rs" 110 0 110 61] (a : borrowed (borrowed (borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global))))) : borrowed t
+    
+  val test5 [#"../05_pearlite.rs" 110 0 110 61] (a : borrowed (borrowed (borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global))))) : borrowed t
+    ensures { result = test5 a }
+    
+end
+module C05Pearlite_Test5
+  type t
+  use prelude.Borrow
+  use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
+  use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
+  clone CreusotContracts_Logic_Ops_Impl0_IndexLogic_Stub as IndexLogic0 with
+    type t = t,
+    type a = Alloc_Alloc_Global_Type.t_global
+  function test5 [#"../05_pearlite.rs" 110 0 110 61] (a : borrowed (borrowed (borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global))))) : borrowed t
+    
+   =
+    [#"../05_pearlite.rs" 109 0 109 8] {current = IndexLogic0.index_logic ( *  *  * a) 0; final = IndexLogic0.index_logic ( ^  *  * a) 0}
+  val test5 [#"../05_pearlite.rs" 110 0 110 61] (a : borrowed (borrowed (borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global))))) : borrowed t
+    ensures { result = test5 a }
+    
+end
+module C05Pearlite_Test6_Stub
+  use prelude.Borrow
+  use prelude.Int
+  use prelude.UInt32
+  function test6 [#"../05_pearlite.rs" 116 0 116 53] (a : borrowed (borrowed uint32)) : borrowed uint32
+end
+module C05Pearlite_Test6_Interface
+  use prelude.Borrow
+  use prelude.Int
+  use prelude.UInt32
+  function test6 [#"../05_pearlite.rs" 116 0 116 53] (a : borrowed (borrowed uint32)) : borrowed uint32
+  val test6 [#"../05_pearlite.rs" 116 0 116 53] (a : borrowed (borrowed uint32)) : borrowed uint32
+    ensures { result = test6 a }
+    
+end
+module C05Pearlite_Test6
+  use prelude.Borrow
+  use prelude.Int
+  use prelude.UInt32
+  function test6 [#"../05_pearlite.rs" 116 0 116 53] (a : borrowed (borrowed uint32)) : borrowed uint32 =
+    [#"../05_pearlite.rs" 115 0 115 8] {current =  *  * a; final =  ^  * a}
+  val test6 [#"../05_pearlite.rs" 116 0 116 53] (a : borrowed (borrowed uint32)) : borrowed uint32
+    ensures { result = test6 a }
+    
+end
diff --git a/creusot/tests/should_succeed/syntax/05_pearlite.rs b/creusot/tests/should_succeed/syntax/05_pearlite.rs
index 205be2e265..4fb2ab7010 100644
--- a/creusot/tests/should_succeed/syntax/05_pearlite.rs
+++ b/creusot/tests/should_succeed/syntax/05_pearlite.rs
@@ -79,6 +79,44 @@ pub fn proj2(x: &mut &mut (S, S)) -> bool {
     x.0.x()
 }
 
+// Unnesting through an index projection
+
+#[open(self)]
+#[ghost]
+pub fn reborrow_index_projection<'a, 'b, T>(a: &'a mut &'b mut [T]) -> &'a mut T {
+    &mut a[0]
+}
+
+#[open(self)]
+#[ghost]
+pub fn reborrow_index_projection2<'a, 'b, T>(a: &'a &'b [T]) -> &'a T {
+    &a[0]
+}
+
+#[open(self)]
+#[ghost]
+pub fn test3<'a, T>(a: Ghost<&'a mut Vec<T>>) -> &'a mut T {
+    &mut a[0]
+}
+
+#[open(self)]
+#[ghost]
+pub fn test4<'a, T>(a: &'a mut Ghost<Vec<T>>) -> &'a mut T {
+    &mut a[0]
+}
+
+#[open(self)]
+#[ghost]
+pub fn test5<'a, T>(a: &'a mut &mut &mut Vec<T>) -> &'a mut T {
+    &mut a[0]
+}
+
+#[open(self)]
+#[ghost]
+pub fn test6<'a>(a: &'a mut &&mut u32) -> &'a mut u32 {
+    &mut ***a
+}
+
 // Left out until I understand the semantics of `Deref` patterns.
 // #[ghost]
 // pub fn proj_opt(x : &mut Option<S>)  -> bool {
diff --git a/creusot/tests/should_succeed/syntax/11_array_types.mlcfg b/creusot/tests/should_succeed/syntax/11_array_types.mlcfg
index ffe3b23c31..e87fab52c9 100644
--- a/creusot/tests/should_succeed/syntax/11_array_types.mlcfg
+++ b/creusot/tests/should_succeed/syntax/11_array_types.mlcfg
@@ -43,7 +43,7 @@ module CreusotContracts_Logic_Ops_Impl4_IndexLogic
   use prelude.Int
   use seq.Seq
   function index_logic [@inline:trivial] (self : array t) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 63 8 63 31] Seq.get (Slice.id self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 64 8 64 31] Seq.get (Slice.id self) ix
   val index_logic [@inline:trivial] (self : array t) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/syntax/12_ghost_code.mlcfg b/creusot/tests/should_succeed/syntax/12_ghost_code.mlcfg
index 658231c943..7c1a1f2c70 100644
--- a/creusot/tests/should_succeed/syntax/12_ghost_code.mlcfg
+++ b/creusot/tests/should_succeed/syntax/12_ghost_code.mlcfg
@@ -193,7 +193,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
@@ -849,7 +849,7 @@ module CreusotContracts_Ghost_Impl1_ShallowModel
     type t = t,
     type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
   function shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy =
-    [#"../../../../../creusot-contracts/src/ghost.rs" 26 20 26 48] ShallowModel0.shallow_model (Ghost.inner self)
+    [#"../../../../../creusot-contracts/src/ghost.rs" 27 20 27 48] ShallowModel0.shallow_model (Ghost.inner self)
   val shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy
     ensures { result = shallow_model self }
     
diff --git a/creusot/tests/should_succeed/syntax/13_vec_macro.mlcfg b/creusot/tests/should_succeed/syntax/13_vec_macro.mlcfg
index be2bd57633..2248373e5e 100644
--- a/creusot/tests/should_succeed/syntax/13_vec_macro.mlcfg
+++ b/creusot/tests/should_succeed/syntax/13_vec_macro.mlcfg
@@ -164,7 +164,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/syntax/derive_macros.mlcfg b/creusot/tests/should_succeed/syntax/derive_macros.mlcfg
index d831fd0b99..3901ef0597 100644
--- a/creusot/tests/should_succeed/syntax/derive_macros.mlcfg
+++ b/creusot/tests/should_succeed/syntax/derive_macros.mlcfg
@@ -1149,7 +1149,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/take_first_mut.mlcfg b/creusot/tests/should_succeed/take_first_mut.mlcfg
index 5e5d8c48c5..927eb42bc0 100644
--- a/creusot/tests/should_succeed/take_first_mut.mlcfg
+++ b/creusot/tests/should_succeed/take_first_mut.mlcfg
@@ -131,7 +131,7 @@ module CreusotContracts_Logic_Ops_Impl2_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : slice t) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 41 8 41 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 42 8 42 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : slice t) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/type_invariants/vec_inv.mlcfg b/creusot/tests/should_succeed/type_invariants/vec_inv.mlcfg
index ad8bf25519..bb49563b7c 100644
--- a/creusot/tests/should_succeed/type_invariants/vec_inv.mlcfg
+++ b/creusot/tests/should_succeed/type_invariants/vec_inv.mlcfg
@@ -204,7 +204,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/vector/01.mlcfg b/creusot/tests/should_succeed/vector/01.mlcfg
index 7c08f8a169..517706bbdd 100644
--- a/creusot/tests/should_succeed/vector/01.mlcfg
+++ b/creusot/tests/should_succeed/vector/01.mlcfg
@@ -159,7 +159,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
@@ -360,7 +360,7 @@ module CreusotContracts_Ghost_Impl1_ShallowModel
     type t = t,
     type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
   function shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy =
-    [#"../../../../../creusot-contracts/src/ghost.rs" 26 20 26 48] ShallowModel0.shallow_model (Ghost.inner self)
+    [#"../../../../../creusot-contracts/src/ghost.rs" 27 20 27 48] ShallowModel0.shallow_model (Ghost.inner self)
   val shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy
     ensures { result = shallow_model self }
     
diff --git a/creusot/tests/should_succeed/vector/02_gnome.mlcfg b/creusot/tests/should_succeed/vector/02_gnome.mlcfg
index f96bb8a2f6..dd900cebcd 100644
--- a/creusot/tests/should_succeed/vector/02_gnome.mlcfg
+++ b/creusot/tests/should_succeed/vector/02_gnome.mlcfg
@@ -260,7 +260,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
@@ -595,7 +595,7 @@ module CreusotContracts_Ghost_Impl1_ShallowModel
     type t = t,
     type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
   function shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy =
-    [#"../../../../../creusot-contracts/src/ghost.rs" 26 20 26 48] ShallowModel0.shallow_model (Ghost.inner self)
+    [#"../../../../../creusot-contracts/src/ghost.rs" 27 20 27 48] ShallowModel0.shallow_model (Ghost.inner self)
   val shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy
     ensures { result = shallow_model self }
     
diff --git a/creusot/tests/should_succeed/vector/03_knuth_shuffle.mlcfg b/creusot/tests/should_succeed/vector/03_knuth_shuffle.mlcfg
index 0f5377dc76..b89733e1b7 100644
--- a/creusot/tests/should_succeed/vector/03_knuth_shuffle.mlcfg
+++ b/creusot/tests/should_succeed/vector/03_knuth_shuffle.mlcfg
@@ -367,7 +367,7 @@ module CreusotContracts_Ghost_Impl1_ShallowModel
     type t = t,
     type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
   function shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy =
-    [#"../../../../../creusot-contracts/src/ghost.rs" 26 20 26 48] ShallowModel0.shallow_model (Ghost.inner self)
+    [#"../../../../../creusot-contracts/src/ghost.rs" 27 20 27 48] ShallowModel0.shallow_model (Ghost.inner self)
   val shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy
     ensures { result = shallow_model self }
     
diff --git a/creusot/tests/should_succeed/vector/04_binary_search.mlcfg b/creusot/tests/should_succeed/vector/04_binary_search.mlcfg
index 8c49d49580..b6bb115dad 100644
--- a/creusot/tests/should_succeed/vector/04_binary_search.mlcfg
+++ b/creusot/tests/should_succeed/vector/04_binary_search.mlcfg
@@ -275,7 +275,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/vector/05_binary_search_generic.mlcfg b/creusot/tests/should_succeed/vector/05_binary_search_generic.mlcfg
index d14c198bf7..84786996ec 100644
--- a/creusot/tests/should_succeed/vector/05_binary_search_generic.mlcfg
+++ b/creusot/tests/should_succeed/vector/05_binary_search_generic.mlcfg
@@ -625,7 +625,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg b/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg
index 20d5f99e53..b9a1479a99 100644
--- a/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg
+++ b/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg
@@ -290,7 +290,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
@@ -3770,7 +3770,7 @@ module CreusotContracts_Logic_Ops_Impl2_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : slice t) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 41 8 41 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 42 8 42 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : slice t) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/vector/08_haystack.mlcfg b/creusot/tests/should_succeed/vector/08_haystack.mlcfg
index ba7701ab65..30319b22eb 100644
--- a/creusot/tests/should_succeed/vector/08_haystack.mlcfg
+++ b/creusot/tests/should_succeed/vector/08_haystack.mlcfg
@@ -223,7 +223,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/creusot/tests/should_succeed/vector/09_capacity.mlcfg b/creusot/tests/should_succeed/vector/09_capacity.mlcfg
index 746c929b58..706ec0fad8 100644
--- a/creusot/tests/should_succeed/vector/09_capacity.mlcfg
+++ b/creusot/tests/should_succeed/vector/09_capacity.mlcfg
@@ -218,7 +218,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
     
diff --git a/rustfmt.toml b/rustfmt.toml
index 8c27e7aabe..dd95ae4c03 100644
--- a/rustfmt.toml
+++ b/rustfmt.toml
@@ -6,7 +6,7 @@ reorder_imports = true
 reorder_modules = true
 remove_nested_parens = true
 fn_params_layout = "Tall"
-edition = "2018"
+edition = "2021"
 merge_derives = true
 use_try_shorthand = false
 use_field_init_shorthand = false