diff --git a/frontend/exporter/src/constant_utils.rs b/frontend/exporter/src/constant_utils.rs
index 4426ba40c..a02f4c86f 100644
--- a/frontend/exporter/src/constant_utils.rs
+++ b/frontend/exporter/src/constant_utils.rs
@@ -305,14 +305,14 @@ pub(crate) fn is_anon_const<'tcx>(
 fn trait_const_to_constant_expr_kind<'tcx, S: BaseState<'tcx> + HasOwnerId>(
     s: &S,
     _const_def_id: rustc_hir::def_id::DefId,
-    substs: rustc_middle::ty::SubstsRef<'tcx>,
+    generics: rustc_middle::ty::GenericArgsRef<'tcx>,
     assoc: &rustc_middle::ty::AssocItem,
 ) -> ConstantExprKind {
     assert!(assoc.trait_item_def_id.is_some());
     let name = assoc.name.to_string();
 
     // Retrieve the trait information
-    let impl_expr = get_trait_info(s, substs, assoc);
+    let impl_expr = get_trait_info(s, generics, assoc);
 
     ConstantExprKind::TraitConst { impl_expr, name }
 }
@@ -356,19 +356,18 @@ pub trait ConstantExt<'tcx>: Sized + std::fmt::Debug {
             let cv = if let Some(assoc) = s.base().tcx.opt_associated_item(ucv.def) {
                 if assoc.trait_item_def_id.is_some() {
                     // This must be a trait declaration constant
-                    trait_const_to_constant_expr_kind(s, ucv.def, ucv.substs, &assoc)
+                    trait_const_to_constant_expr_kind(s, ucv.def, ucv.args, &assoc)
                 } else {
                     // Constant appearing in an inherent impl block.
 
                     // Solve the trait obligations
                     let parent_def_id = tcx.parent(ucv.def);
                     let param_env = s.param_env();
-                    let trait_refs =
-                        solve_item_traits(s, param_env, parent_def_id, ucv.substs, None);
+                    let trait_refs = solve_item_traits(s, param_env, parent_def_id, ucv.args, None);
 
                     // Convert
                     let id = ucv.def.sinto(s);
-                    let generics = ucv.substs.sinto(s);
+                    let generics = ucv.args.sinto(s);
                     ConstantExprKind::GlobalName {
                         id,
                         generics,
@@ -377,7 +376,7 @@ pub trait ConstantExt<'tcx>: Sized + std::fmt::Debug {
                 }
             } else {
                 // Top-level constant.
-                assert!(ucv.substs.is_empty(), "top-level constant has generics?");
+                assert!(ucv.args.is_empty(), "top-level constant has generics?");
                 let id = ucv.def.sinto(s);
                 ConstantExprKind::GlobalName {
                     id,
@@ -559,9 +558,9 @@ pub fn const_value_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
             let cv = match &hty {
                 Ty::Tuple(tys) if tys.is_empty() => ConstantExprKind::Tuple { fields: Vec::new() },
                 Ty::Arrow(_) => match ty.kind() {
-                    rustc_middle::ty::TyKind::FnDef(def_id, substs) => {
+                    rustc_middle::ty::TyKind::FnDef(def_id, args) => {
                         let (def_id, generics, generics_impls, method_impl) =
-                            get_function_from_def_id_and_substs(s, *def_id, substs);
+                            get_function_from_def_id_and_generics(s, *def_id, args);
 
                         ConstantExprKind::FnPtr {
                             def_id,
diff --git a/frontend/exporter/src/rustc_utils.rs b/frontend/exporter/src/rustc_utils.rs
index 676d44407..f83248752 100644
--- a/frontend/exporter/src/rustc_utils.rs
+++ b/frontend/exporter/src/rustc_utils.rs
@@ -6,9 +6,9 @@ impl<'tcx, T: ty::TypeFoldable<ty::TyCtxt<'tcx>>> ty::Binder<'tcx, T> {
     fn subst(
         self,
         tcx: ty::TyCtxt<'tcx>,
-        substs: &[ty::subst::GenericArg<'tcx>],
+        generics: &[ty::GenericArg<'tcx>],
     ) -> ty::Binder<'tcx, T> {
-        self.rebind(ty::EarlyBinder::bind(self.clone().skip_binder()).subst(tcx, substs))
+        self.rebind(ty::EarlyBinder::bind(self.clone().skip_binder()).instantiate(tcx, generics))
     }
 }
 
@@ -95,11 +95,11 @@ impl<'tcx> ty::TyCtxt<'tcx> {
 pub fn poly_trait_ref<'tcx, S: UnderOwnerState<'tcx>>(
     s: &S,
     assoc: &ty::AssocItem,
-    substs: ty::SubstsRef<'tcx>,
+    generics: ty::GenericArgsRef<'tcx>,
 ) -> Option<ty::PolyTraitRef<'tcx>> {
     let tcx = s.base().tcx;
     let r#trait = tcx.trait_of_item(assoc.def_id)?;
-    Some(ty::Binder::dummy(ty::TraitRef::new(tcx, r#trait, substs)))
+    Some(ty::Binder::dummy(ty::TraitRef::new(tcx, r#trait, generics)))
 }
 
 #[tracing::instrument(skip(s))]
diff --git a/frontend/exporter/src/state.rs b/frontend/exporter/src/state.rs
index 26e1fc4f6..71b4ae887 100644
--- a/frontend/exporter/src/state.rs
+++ b/frontend/exporter/src/state.rs
@@ -248,7 +248,7 @@ impl ImplInfos {
 
         Self {
             generics: tcx.generics_of(did).sinto(s),
-            typ: tcx.type_of(did).subst_identity().sinto(s),
+            typ: tcx.type_of(did).instantiate_identity().sinto(s),
             trait_ref: tcx.impl_trait_ref(did).sinto(s),
             clauses: tcx.predicates_defined_on(did).predicates.sinto(s),
         }
diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs
index 1f6471e2c..cae1cec9c 100644
--- a/frontend/exporter/src/traits.rs
+++ b/frontend/exporter/src/traits.rs
@@ -80,10 +80,10 @@ pub(crate) mod search_clause {
     fn predicates_to_poly_trait_predicates<'tcx>(
         tcx: TyCtxt<'tcx>,
         predicates: impl Iterator<Item = Predicate<'tcx>>,
-        substs: subst::SubstsRef<'tcx>,
+        generics: GenericArgsRef<'tcx>,
     ) -> impl Iterator<Item = PolyTraitPredicate<'tcx>> {
         predicates
-            .map(move |pred| pred.kind().subst(tcx, substs))
+            .map(move |pred| pred.kind().subst(tcx, generics))
             .filter_map(|pred| pred.as_poly_trait_predicate())
     }
 
@@ -160,20 +160,16 @@ pub(crate) mod search_clause {
                 .predicates_defined_on_or_above(self.def_id())
                 .into_iter()
                 .map(|apred| apred.predicate);
-            predicates_to_poly_trait_predicates(
-                tcx,
-                predicates,
-                self.skip_binder().trait_ref.substs,
-            )
-            .enumerate()
-            .collect()
+            predicates_to_poly_trait_predicates(tcx, predicates, self.skip_binder().trait_ref.args)
+                .enumerate()
+                .collect()
         }
         fn associated_items_trait_predicates(
             self,
             s: &S,
         ) -> Vec<(
             AssocItem,
-            subst::EarlyBinder<Vec<(usize, PolyTraitPredicate<'tcx>)>>,
+            EarlyBinder<Vec<(usize, PolyTraitPredicate<'tcx>)>>,
         )> {
             let tcx = s.base().tcx;
             tcx.associated_items(self.def_id())
@@ -185,7 +181,7 @@ pub(crate) mod search_clause {
                         predicates_to_poly_trait_predicates(
                             tcx,
                             clauses.into_iter().map(|clause| clause.as_predicate()),
-                            self.skip_binder().trait_ref.substs,
+                            self.skip_binder().trait_ref.args,
                         )
                         .enumerate()
                         .collect()
@@ -321,11 +317,11 @@ impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::PolyTraitRef<'tcx> {
         match select_trait_candidate(s, param_env, *self) {
             ImplSource::UserDefined(ImplSourceUserDefinedData {
                 impl_def_id,
-                substs,
+                args: generics,
                 nested,
             }) => ImplExprAtom::Concrete {
                 id: impl_def_id.sinto(s),
-                generics: substs.sinto(s),
+                generics: generics.sinto(s),
             }
             .with_args(impl_exprs(s, &nested), trait_ref),
             ImplSource::Param(nested, _constness) => {
@@ -398,7 +394,7 @@ pub fn super_clause_to_clause_and_impl_expr<'tcx, S: UnderOwnerState<'tcx>>(
     let tcx = s.base().tcx;
     let impl_trait_ref = tcx
         .impl_trait_ref(impl_did)
-        .map(|binder| rustc_middle::ty::Binder::dummy(binder.subst_identity()))?;
+        .map(|binder| rustc_middle::ty::Binder::dummy(binder.instantiate_identity()))?;
     let original_predicate_id = {
         // We don't want the id of the substituted clause id, but the
         // original clause id (with, i.e., `Self`)
diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs
index 80fd771db..f85fe9783 100644
--- a/frontend/exporter/src/types/copied.rs
+++ b/frontend/exporter/src/types/copied.rs
@@ -463,19 +463,19 @@ pub enum CanonicalVarInfo {
     PlaceholderConst(PlaceholderConst, Ty),
 }
 
-/// Reflects [`rustc_middle::ty::subst::UserSelfTy`]
+/// Reflects [`rustc_middle::ty::UserSelfTy`]
 #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)]
-#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::ty::subst::UserSelfTy<'tcx>, state: S as gstate)]
+#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::ty::UserSelfTy<'tcx>, state: S as gstate)]
 pub struct UserSelfTy {
     pub impl_def_id: DefId,
     pub self_ty: Ty,
 }
 
-/// Reflects [`rustc_middle::ty::subst::UserSubsts`]
+/// Reflects [`rustc_middle::ty::UserArgs`]
 #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)]
-#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::ty::subst::UserSubsts<'tcx>, state: S as gstate)]
-pub struct UserSubsts {
-    pub substs: Vec<GenericArg>,
+#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::ty::UserArgs<'tcx>, state: S as gstate)]
+pub struct UserArgs {
+    pub args: Vec<GenericArg>,
     pub user_self_ty: Option<UserSelfTy>,
 }
 
@@ -506,7 +506,7 @@ pub enum UserType {
     // See: https://github.com/hacspec/hax/pull/209
 
     // Ty(Ty),
-    // TypeOf(DefId, UserSubsts),
+    // TypeOf(DefId, UserArgs),
     #[todo]
     Todo(String),
 }
@@ -560,8 +560,8 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, FieldDef> for rustc_middle::ty::Fi
     fn sinto(&self, s: &S) -> FieldDef {
         let tcx = s.base().tcx;
         let ty = {
-            let substs = rustc_middle::ty::subst::InternalSubsts::identity_for_item(tcx, self.did);
-            self.ty(tcx, substs).sinto(s)
+            let generics = rustc_middle::ty::GenericArgs::identity_for_item(tcx, self.did);
+            self.ty(tcx, generics).sinto(s)
         };
         let name = {
             let name = self.name.sinto(s);
@@ -650,11 +650,11 @@ pub struct Region {
     pub kind: RegionKind,
 }
 
-/// Reflects both [`rustc_middle::ty::subst::GenericArg`] and [`rustc_middle::ty::subst::GenericArgKind`]
+/// Reflects both [`rustc_middle::ty::GenericArg`] and [`rustc_middle::ty::GenericArgKind`]
 #[derive(
     AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
-#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::ty::subst::GenericArgKind<'tcx>, state: S as s)]
+#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::ty::GenericArgKind<'tcx>, state: S as s)]
 pub enum GenericArg {
     Lifetime(Region),
     Type(Ty),
@@ -668,14 +668,14 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, GenericArg> for rustc_middle::ty::
 }
 
 impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Vec<GenericArg>>
-    for rustc_middle::ty::subst::SubstsRef<'tcx>
+    for rustc_middle::ty::GenericArgsRef<'tcx>
 {
     fn sinto(&self, s: &S) -> Vec<GenericArg> {
         self.iter().map(|v| v.unpack().sinto(s)).collect()
     }
 }
 
-/// Reflects both [`rustc_middle::ty::subst::GenericArg`] and [`rustc_middle::ty::subst::GenericArgKind`]
+/// Reflects both [`rustc_middle::ty::GenericArg`] and [`rustc_middle::ty::GenericArgKind`]
 #[derive(AdtInto)]
 #[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::LitIntType, state: S as gstate)]
 #[derive(
@@ -1242,10 +1242,10 @@ impl<'tcx, S: ExprState<'tcx>> SInto<S, Expr> for rustc_middle::thir::Expr<'tcx>
                     return cexpr.into();
                 }
                 rustc_middle::thir::ExprKind::ZstLiteral { .. } => match ty.kind() {
-                    rustc_middle::ty::TyKind::FnDef(def, _substs) => {
-                        /* TODO: translate substs
+                    rustc_middle::ty::TyKind::FnDef(def, _generics) => {
+                        /* TODO: translate generics
                         let tcx = s.base().tcx;
-                        let sig = &tcx.fn_sig(*def).subst(tcx, substs);
+                        let sig = &tcx.fn_sig(*def).instantiate(tcx, generics);
                         let ret: rustc_middle::ty::Ty = tcx.erase_late_bound_regions(sig.output());
                         let inputs = sig.inputs();
                         let indexes = inputs.skip_binder().iter().enumerate().map(|(i, _)| i);
@@ -1308,7 +1308,7 @@ impl<'tcx, S: ExprState<'tcx>> SInto<S, Expr> for rustc_middle::thir::Expr<'tcx>
                         );
                     };
                     match lhs_ty {
-                        rustc_middle::ty::TyKind::Adt(adt_def, _substs) => {
+                        rustc_middle::ty::TyKind::Adt(adt_def, _generics) => {
                             let variant = adt_def.variant(variant_index);
                             ExprKind::Field {
                                 field: variant.fields[name].did.sinto(s),
@@ -1354,10 +1354,10 @@ impl<'tcx, S: ExprState<'tcx>> SInto<S, Pat> for rustc_middle::thir::Pat<'tcx> {
         let rustc_middle::thir::Pat { span, kind, ty } = self;
         let contents = match kind {
             rustc_middle::thir::PatKind::Leaf { subpatterns } => match ty.kind() {
-                rustc_middle::ty::TyKind::Adt(adt_def, substs) => {
+                rustc_middle::ty::TyKind::Adt(adt_def, args) => {
                     (rustc_middle::thir::PatKind::Variant {
                         adt_def: adt_def.clone(),
-                        substs,
+                        args,
                         variant_index: rustc_target::abi::VariantIdx::from_usize(0),
                         subpatterns: subpatterns.clone(),
                     })
@@ -1559,7 +1559,7 @@ pub struct TyGenerics {
 )]
 pub struct Alias {
     pub kind: AliasKind,
-    pub substs: Vec<GenericArg>,
+    pub args: Vec<GenericArg>,
     pub def_id: DefId,
 }
 
@@ -1601,32 +1601,32 @@ impl Alias {
                 // this seems fine. If we detect such a situation, we
                 // emit a warning with a lot of debugging information.
                 let poly_trait_ref = if trait_ref.has_escaping_bound_vars() {
-                    let trait_ref_and_substs = alias_ty.trait_ref_and_own_substs(tcx);
-                    let rebased_substs = alias_ty.rebase_substs_onto_impl(alias_ty.substs, tcx);
-                    let norm_rebased_substs = tcx.try_subst_and_normalize_erasing_regions(
-                        rebased_substs,
+                    let trait_ref_and_generics = alias_ty.trait_ref_and_own_args(tcx);
+                    let rebased_generics = alias_ty.rebase_args_onto_impl(alias_ty.args, tcx);
+                    let norm_rebased_generics = tcx.try_subst_and_normalize_erasing_regions(
+                        rebased_generics,
                         s.param_env(),
                         EarlyBinder::bind(trait_ref),
                     );
-                    let norm_substs = tcx.try_subst_and_normalize_erasing_regions(
-                        alias_ty.substs,
+                    let norm_generics = tcx.try_subst_and_normalize_erasing_regions(
+                        alias_ty.args,
                         s.param_env(),
                         EarlyBinder::bind(trait_ref),
                     );
-                    let early_binder_substs =
+                    let early_binder_generics =
                         std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| {
-                            EarlyBinder::bind(trait_ref).subst(tcx, alias_ty.substs)
+                            EarlyBinder::bind(trait_ref).instantiate(tcx, alias_ty.args)
                         }));
-                    let early_binder_rebased_substs =
+                    let early_binder_rebased_generics =
                         std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| {
-                            EarlyBinder::bind(trait_ref).subst(tcx, alias_ty.substs)
+                            EarlyBinder::bind(trait_ref).instantiate(tcx, alias_ty.args)
                         }));
                     warning!(
                         s,
                         "Hax frontend found a projected type with escaping bound vars. Please report https://github.com/hacspec/hax/issues/495";
-                        {alias_ty, alias_kind, trait_ref, trait_ref_and_substs, rebased_substs,
-                         norm_rebased_substs, norm_substs,
-                         early_binder_substs, early_binder_rebased_substs}
+                        {alias_ty, alias_kind, trait_ref, trait_ref_and_generics, rebased_generics,
+                         norm_rebased_generics, norm_generics,
+                         early_binder_generics, early_binder_rebased_generics}
                     );
                     // we cannot use `Binder::dummy`: it asserts that
                     // there is no any escaping bound vars
@@ -1645,7 +1645,7 @@ impl Alias {
         };
         Alias {
             kind,
-            substs: alias_ty.substs.sinto(s),
+            args: alias_ty.args.sinto(s),
             def_id: alias_ty.def_id.sinto(s),
         }
     }
@@ -1666,12 +1666,12 @@ pub enum Ty {
 
     #[custom_arm(
         rustc_middle::ty::TyKind::FnPtr(sig) => arrow_of_sig(sig, state),
-        rustc_middle::ty::TyKind::FnDef(def, substs) => {
+        rustc_middle::ty::TyKind::FnDef(def, generics) => {
             let tcx = state.base().tcx;
-            arrow_of_sig(&tcx.fn_sig(*def).subst(tcx, substs), state)
+            arrow_of_sig(&tcx.fn_sig(*def).instantiate(tcx, generics), state)
         },
-        FROM_TYPE::Closure (_defid, substs) => {
-            let sig = substs.as_closure().sig();
+        FROM_TYPE::Closure (_defid, generics) => {
+            let sig = generics.as_closure().sig();
             let sig = state.base().tcx.signature_unclosure(sig, rustc_hir::Unsafety::Normal);
             arrow_of_sig(&sig, state)
         },
@@ -1680,10 +1680,10 @@ pub enum Ty {
     Arrow(Box<PolyFnSig>),
 
     #[custom_arm(
-        rustc_middle::ty::TyKind::Adt(adt_def, substs) => {
+        rustc_middle::ty::TyKind::Adt(adt_def, generics) => {
             let def_id = adt_def.did().sinto(state);
-            let generic_args: Vec<GenericArg> = substs.sinto(state);
-            let trait_refs = solve_item_traits(state, state.param_env(), adt_def.did(), substs, None);
+            let generic_args: Vec<GenericArg> = generics.sinto(state);
+            let trait_refs = solve_item_traits(state, state.param_env(), adt_def.did(), generics, None);
             Ty::Adt { def_id, generic_args, trait_refs }
         },
     )]
@@ -1897,7 +1897,7 @@ pub enum PatKind {
         is_primary: bool,
     },
     #[custom_arm(
-        FROM_TYPE::Variant {adt_def, variant_index, substs, subpatterns} => {
+        FROM_TYPE::Variant {adt_def, variant_index, args, subpatterns} => {
             let variants = adt_def.variants();
             let variant: &rustc_middle::ty::VariantDef = &variants[*variant_index];
             TO_TYPE::Variant {
@@ -1909,13 +1909,13 @@ pub enum PatKind {
                         pattern: f.pattern.sinto(gstate),
                     })
                     .collect(),
-                substs: substs.sinto(gstate),
+                args: args.sinto(gstate),
             }
         }
     )]
     Variant {
         info: VariantInformations,
-        substs: Vec<GenericArg>,
+        args: Vec<GenericArg>,
         subpatterns: Vec<FieldPat>,
     },
     #[disable_mapping]
@@ -2214,7 +2214,7 @@ pub enum ExprKind {
             /* TODO: see whether [user_ty] below is relevant or not */
             rustc_middle::thir::ExprKind::ZstLiteral {user_ty: _ } => {
                 match ty.kind() {
-                    rustc_middle::ty::TyKind::FnDef(def_id, substs) => {
+                    rustc_middle::ty::TyKind::FnDef(def_id, generics) => {
                         let (hir_id, attributes) = e.hir_id_and_attributes(gstate);
                         let hir_id = hir_id.map(|hir_id| hir_id.index());
                         let contents = Box::new(ExprKind::GlobalName {
@@ -2222,10 +2222,10 @@ pub enum ExprKind {
                         });
                         let tcx = gstate.base().tcx;
                         r#impl = tcx.opt_associated_item(*def_id).as_ref().and_then(|assoc| {
-                            poly_trait_ref(gstate, assoc, substs)
+                            poly_trait_ref(gstate, assoc, generics)
                         }).map(|poly_trait_ref| poly_trait_ref.impl_expr(gstate, gstate.param_env()));
-                        generic_args = substs.sinto(gstate);
-                        bounds_impls = solve_item_traits(gstate, gstate.param_env(), *def_id, substs, None);
+                        generic_args = generics.sinto(gstate);
+                        bounds_impls = solve_item_traits(gstate, gstate.param_env(), *def_id, generics, None);
                         Expr {
                             contents,
                             span: e.span.sinto(gstate),
@@ -2416,7 +2416,7 @@ pub enum ExprKind {
     },
     ConstBlock {
         did: DefId,
-        substs: Vec<GenericArg>,
+        args: Vec<GenericArg>,
     },
     Repeat {
         value: Expr,
@@ -2470,13 +2470,13 @@ pub enum ExprKind {
     },
     NamedConst {
         def_id: GlobalIdent,
-        substs: Vec<GenericArg>,
+        args: Vec<GenericArg>,
         user_ty: Option<CanonicalUserType>,
         #[not_in_source]
         #[value({
             let tcx = gstate.base().tcx;
             tcx.opt_associated_item(*def_id).as_ref().and_then(|assoc| {
-                poly_trait_ref(gstate, assoc, substs)
+                poly_trait_ref(gstate, assoc, args)
             }).map(|poly_trait_ref| poly_trait_ref.impl_expr(gstate, gstate.param_env()))
         })]
         r#impl: Option<ImplExpr>,
@@ -2829,10 +2829,10 @@ impl<
         S,
         D: Clone,
         T: SInto<S, D> + rustc_middle::ty::TypeFoldable<rustc_middle::ty::TyCtxt<'tcx>>,
-    > SInto<S, D> for rustc_middle::ty::subst::EarlyBinder<T>
+    > SInto<S, D> for rustc_middle::ty::EarlyBinder<T>
 {
     fn sinto(&self, s: &S) -> D {
-        self.clone().subst_identity().sinto(s)
+        self.clone().instantiate_identity().sinto(s)
     }
 }
 
@@ -3216,8 +3216,8 @@ pub struct Lifetime {
 )]
 pub struct TraitRef {
     pub def_id: DefId,
-    #[from(substs)]
-    /// reflects the `substs` field
+    #[from(args)]
+    /// reflects the `args` field
     pub generic_args: Vec<GenericArg>,
 }
 
@@ -3526,7 +3526,7 @@ fn region_bounds_at_current_owner<'tcx, S: UnderOwnerState<'tcx>>(s: &S) -> Gene
 
     let clauses: Vec<ty::Clause<'tcx>> = if use_item_bounds {
         tcx.item_bounds(s.owner_id())
-            .subst_identity()
+            .instantiate_identity()
             .iter()
             .collect()
     } else {
diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs
index 48f3671e6..9cd5a99dc 100644
--- a/frontend/exporter/src/types/mir.rs
+++ b/frontend/exporter/src/types/mir.rs
@@ -164,7 +164,7 @@ pub struct SourceScopeData {
 #[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::ty::Instance<'tcx>, state: S as s)]
 pub struct Instance {
     pub def: InstanceDef,
-    pub substs: Vec<GenericArg>,
+    pub args: Vec<GenericArg>,
 }
 
 #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)]
@@ -207,10 +207,10 @@ pub struct Terminator {
     pub kind: TerminatorKind,
 }
 
-pub(crate) fn get_function_from_def_id_and_substs<'tcx, S: BaseState<'tcx> + HasOwnerId>(
+pub(crate) fn get_function_from_def_id_and_generics<'tcx, S: BaseState<'tcx> + HasOwnerId>(
     s: &S,
     def_id: rustc_hir::def_id::DefId,
-    substs: rustc_middle::ty::subst::SubstsRef<'tcx>,
+    generics: rustc_middle::ty::GenericArgsRef<'tcx>,
 ) -> (DefId, Vec<GenericArg>, Vec<ImplExpr>, Option<ImplExpr>) {
     let tcx = s.base().tcx;
     let param_env = s.param_env();
@@ -221,7 +221,7 @@ pub(crate) fn get_function_from_def_id_and_substs<'tcx, S: BaseState<'tcx> + Has
     // fn foo<T : Bar>(...)
     //            ^^^
     // ```
-    let mut trait_refs = solve_item_traits(s, param_env, def_id, substs, None);
+    let mut trait_refs = solve_item_traits(s, param_env, def_id, generics, None);
 
     // Check if this is a trait method call: retrieve the trait source if
     // it is the case (i.e., where does the method come from? Does it refer
@@ -248,7 +248,7 @@ pub(crate) fn get_function_from_def_id_and_substs<'tcx, S: BaseState<'tcx> + Has
     //            ^^^
     //     method level trait obligation
     // ```
-    let (substs, source) = if let Some(assoc) = tcx.opt_associated_item(def_id) {
+    let (generics, source) = if let Some(assoc) = tcx.opt_associated_item(def_id) {
         // There is an associated item.
         use tracing::*;
         trace!("def_id: {:?}", def_id);
@@ -276,7 +276,7 @@ pub(crate) fn get_function_from_def_id_and_substs<'tcx, S: BaseState<'tcx> + Has
         //     ...
         // }
         // ```
-        // The substs for the call to `baz` will be the concatenation: `<T, u32, U>`, which we
+        // The generics for the call to `baz` will be the concatenation: `<T, u32, U>`, which we
         // split into `<T, u32>` and `<U>`.
         //
         // If we have:
@@ -288,33 +288,33 @@ pub(crate) fn get_function_from_def_id_and_substs<'tcx, S: BaseState<'tcx> + Has
         //     tree.insert(false);
         // }
         // ```
-        // The substs for `insert` are `<u32>` for the impl and `<bool>` for the method.
+        // The generics for `insert` are `<u32>` for the impl and `<bool>` for the method.
         let params_info = get_params_info(s, container_def_id);
         let num_container_generics = params_info.num_generic_params;
         match assoc.container {
             rustc_middle::ty::AssocItemContainer::TraitContainer => {
                 // Retrieve the trait information
-                let impl_expr = get_trait_info(s, substs, &assoc);
+                let impl_expr = get_trait_info(s, generics, &assoc);
                 // Return only the method generics; the trait generics are included in `impl_expr`.
-                let method_substs = &substs[num_container_generics..];
-                (method_substs.sinto(s), Option::Some(impl_expr))
+                let method_generics = &generics[num_container_generics..];
+                (method_generics.sinto(s), Option::Some(impl_expr))
             }
             rustc_middle::ty::AssocItemContainer::ImplContainer => {
                 // Solve the trait constraints of the impl block.
                 let container_generics = tcx.generics_of(container_def_id);
-                let container_substs = substs.truncate_to(tcx, container_generics);
+                let container_generics = generics.truncate_to(tcx, container_generics);
                 let container_trait_refs =
-                    solve_item_traits(s, param_env, container_def_id, container_substs, None);
+                    solve_item_traits(s, param_env, container_def_id, container_generics, None);
                 trait_refs.extend(container_trait_refs);
-                (substs.sinto(s), Option::None)
+                (generics.sinto(s), Option::None)
             }
         }
     } else {
         // Regular function call
-        (substs.sinto(s), Option::None)
+        (generics.sinto(s), Option::None)
     };
 
-    (def_id.sinto(s), substs, trait_refs, source)
+    (def_id.sinto(s), generics, trait_refs, source)
 }
 
 /// Return the [DefId] of the function referenced by an operand, with the
@@ -335,14 +335,14 @@ fn get_function_from_operand<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>>(
         Operand::Constant(c) => {
             // Regular function case
             let c = c.deref();
-            let (def_id, substs) = match &c.literal {
+            let (def_id, generics) = match &c.literal {
                 ConstantKind::Ty(c) => {
                     // The type of the constant should be a FnDef, allowing
                     // us to retrieve the function's identifier and instantiation.
                     let c_ty = c.ty();
                     assert!(c_ty.is_fn());
                     match c_ty.kind() {
-                        TyKind::FnDef(def_id, substs) => (*def_id, *substs),
+                        TyKind::FnDef(def_id, generics) => (*def_id, *generics),
                         _ => {
                             unreachable!();
                         }
@@ -352,7 +352,7 @@ fn get_function_from_operand<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>>(
                     // Same as for the `Ty` case above
                     assert!(c_ty.is_fn());
                     match c_ty.kind() {
-                        TyKind::FnDef(def_id, substs) => (*def_id, *substs),
+                        TyKind::FnDef(def_id, generics) => (*def_id, *generics),
                         _ => {
                             unreachable!();
                         }
@@ -363,9 +363,9 @@ fn get_function_from_operand<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>>(
                 }
             };
 
-            let (fun_id, substs, trait_refs, trait_info) =
-                get_function_from_def_id_and_substs(s, def_id, substs);
-            (FunOperand::Id(fun_id), substs, trait_refs, trait_info)
+            let (fun_id, generics, trait_refs, trait_info) =
+                get_function_from_def_id_and_generics(s, def_id, generics);
+            (FunOperand::Id(fun_id), generics, trait_refs, trait_info)
         }
         Operand::Move(place) => {
             // Closure case.
@@ -404,11 +404,11 @@ fn translate_terminator_kind_call<'tcx, S: BaseState<'tcx> + HasMir<'tcx> + HasO
         fn_span,
     } = terminator
     {
-        let (fun, substs, trait_refs, trait_info) = get_function_from_operand(s, func);
+        let (fun, generics, trait_refs, trait_info) = get_function_from_operand(s, func);
 
         TerminatorKind::Call {
             fun,
-            substs,
+            generics,
             args: args.sinto(s),
             destination: destination.sinto(s),
             target: target.sinto(s),
@@ -549,7 +549,7 @@ pub enum TerminatorKind {
         /// We truncate the substitution so as to only include the arguments
         /// relevant to the method (and not the trait) if it is a trait method
         /// call. See [ParamsInfo] for the full details.
-        substs: Vec<GenericArg>,
+        generics: Vec<GenericArg>,
         args: Vec<Operand>,
         destination: Place,
         target: Option<BasicBlock>,
@@ -720,7 +720,7 @@ impl<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>> SInto<S, Place>
                         Deref => {
                             current_ty = match current_ty.kind() {
                                 TyKind::Ref(_, ty, _) => ty.clone(),
-                                TyKind::Adt(def, substs) if def.is_box() => substs.type_at(0),
+                                TyKind::Adt(def, generics) if def.is_box() => generics.type_at(0),
                                 _ => supposely_unreachable_fatal!(
                                     s, "PlaceDerefNotRefNorBox";
                                     {current_ty, current_kind, elem}
@@ -729,12 +729,12 @@ impl<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>> SInto<S, Place>
                             ProjectionElem::Deref
                         }
                         Field(index, ty) => {
-                            if let TyKind::Closure(_, substs) = cur_ty.kind() {
+                            if let TyKind::Closure(_, generics) = cur_ty.kind() {
                                 // We get there when we access one of the fields
                                 // of the the state captured by a closure.
                                 use crate::rustc_index::Idx;
-                                let substs = substs.as_closure();
-                                let upvar_tys: Vec<_> = substs.upvar_tys().collect();
+                                let generics = generics.as_closure();
+                                let upvar_tys: Vec<_> = generics.upvar_tys().collect();
                                 current_ty = upvar_tys[index.sinto(s).index()].clone();
                                 ProjectionElem::Field(ProjectionElemFieldKind::ClosureState(
                                     index.sinto(s),
@@ -850,15 +850,15 @@ pub(crate) fn poly_fn_sig_to_mir_poly_fn_sig<'tcx, S: BaseState<'tcx> + HasOwner
 pub enum AggregateKind {
     Array(Ty),
     Tuple,
-    #[custom_arm(rustc_middle::mir::AggregateKind::Adt(def_id, vid, substs, annot, fid) => {
+    #[custom_arm(rustc_middle::mir::AggregateKind::Adt(def_id, vid, generics, annot, fid) => {
         let adt_kind = s.base().tcx.adt_def(def_id).adt_kind().sinto(s);
         let param_env = s.param_env();
-        let trait_refs = solve_item_traits(s, param_env, *def_id, substs, None);
+        let trait_refs = solve_item_traits(s, param_env, *def_id, generics, None);
         AggregateKind::Adt(
             def_id.sinto(s),
             vid.sinto(s),
             adt_kind,
-            substs.sinto(s),
+            generics.sinto(s),
             trait_refs,
             annot.sinto(s),
             fid.sinto(s))
@@ -872,27 +872,27 @@ pub enum AggregateKind {
         Option<UserTypeAnnotationIndex>,
         Option<FieldIdx>,
     ),
-    #[custom_arm(rustc_middle::mir::AggregateKind::Closure(rust_id, substs) => {
+    #[custom_arm(rustc_middle::mir::AggregateKind::Closure(rust_id, generics) => {
         let def_id : DefId = rust_id.sinto(s);
-        // The substs is meant to be converted to a function signature. Note
+        // The generics is meant to be converted to a function signature. Note
         // that Rustc does its job: the PolyFnSig binds the captured local
         // type, regions, etc. variables, which means we can treat the local
         // closure like any top-level function.
-        let closure = substs.as_closure();
+        let closure = generics.as_closure();
         let sig = closure.sig();
         let sig = poly_fn_sig_to_mir_poly_fn_sig(&sig, s);
 
         // Solve the trait obligations. Note that we solve the parent
         let tcx = s.base().tcx;
         let param_env = s.param_env();
-        let parent_substs = closure.parent_substs();
-        let substs = tcx.mk_substs(parent_substs);
+        let parent_generics = closure.parent_args();
+        let generics = tcx.mk_args(parent_generics);
         // Retrieve the predicates from the parent (i.e., the function which calls
         // the closure).
         let predicates = tcx.predicates_defined_on(tcx.generics_of(rust_id).parent.unwrap());
 
-        let trait_refs = solve_item_traits(s, param_env, *rust_id, substs, Some(predicates));
-        AggregateKind::Closure(def_id, parent_substs.sinto(s), trait_refs, sig)
+        let trait_refs = solve_item_traits(s, param_env, *rust_id, generics, Some(predicates));
+        AggregateKind::Closure(def_id, parent_generics.sinto(s), trait_refs, sig)
     })]
     Closure(DefId, Vec<GenericArg>, Vec<ImplExpr>, MirPolyFnSig),
     Generator(DefId, Vec<GenericArg>, Movability),
diff --git a/frontend/exporter/src/types/mir_traits.rs b/frontend/exporter/src/types/mir_traits.rs
index 182e4607f..c0d3c39dd 100644
--- a/frontend/exporter/src/types/mir_traits.rs
+++ b/frontend/exporter/src/types/mir_traits.rs
@@ -4,7 +4,7 @@ use crate::prelude::*;
 /// TODO: rename
 pub fn get_trait_info<'tcx, S: UnderOwnerState<'tcx>>(
     s: &S,
-    substs: rustc_middle::ty::SubstsRef<'tcx>,
+    generics: rustc_middle::ty::GenericArgsRef<'tcx>,
     assoc: &rustc_middle::ty::AssocItem,
 ) -> ImplExpr {
     let tcx = s.base().tcx;
@@ -15,7 +15,7 @@ pub fn get_trait_info<'tcx, S: UnderOwnerState<'tcx>>(
 
     // Create the reference to the trait
     use rustc_middle::ty::TraitRef;
-    let tr_ref = TraitRef::new(tcx, tr_def_id, substs);
+    let tr_ref = TraitRef::new(tcx, tr_def_id, generics);
     let tr_ref = rustc_middle::ty::Binder::dummy(tr_ref);
 
     // Solve
@@ -48,7 +48,7 @@ pub fn solve_item_traits<'tcx, S: UnderOwnerState<'tcx>>(
     s: &S,
     param_env: rustc_middle::ty::ParamEnv<'tcx>,
     def_id: rustc_hir::def_id::DefId,
-    substs: rustc_middle::ty::subst::SubstsRef<'tcx>,
+    generics: rustc_middle::ty::GenericArgsRef<'tcx>,
     predicates: Option<rustc_middle::ty::GenericPredicates<'tcx>>,
 ) -> Vec<ImplExpr> {
     let tcx = s.base().tcx;
@@ -77,7 +77,7 @@ pub fn solve_item_traits<'tcx, S: UnderOwnerState<'tcx>>(
             // variables.
             // Remark: there is also EarlyBinder::subst(...)
             let value = rustc_middle::ty::EarlyBinder::bind(pred_kind.skip_binder());
-            tcx.subst_and_normalize_erasing_regions(substs, param_env, value)
+            tcx.subst_and_normalize_erasing_regions(generics, param_env, value)
         };
 
         // Explore only the trait predicates
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 4966f3eda..794fd61a1 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2023-07-10"
+channel = "nightly-2023-07-15"
 components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ]