diff --git a/src/extract/Extract.ml b/src/extract/Extract.ml
index 41f3000d..796cd29c 100644
--- a/src/extract/Extract.ml
+++ b/src/extract/Extract.ml
@@ -357,7 +357,7 @@ let rec extract_texpression (span : Meta.span) (ctx : extraction_ctx)
       let var_name = ctx_get_var span var_id ctx in
       F.pp_print_string fmt var_name
   | CVar var_id ->
-      let var_name = ctx_get_const_generic_var span var_id ctx in
+      let var_name = ctx_get_const_generic_var span Item var_id ctx in
       F.pp_print_string fmt var_name
   | Const cv -> extract_literal span fmt is_pattern inside cv
   | App _ ->
@@ -1314,7 +1314,7 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
   (* Add the type parameters - note that we need those bindings only for the
    * body translation (they are not top-level) *)
   let ctx, type_params, cg_params, trait_clauses =
-    ctx_add_generic_params def.item_meta.span def.item_meta.name
+    ctx_add_generic_params def.item_meta.span def.item_meta.name Item
       def.signature.llbc_generics def.signature.generics ctx
   in
   (* Print the generics *)
@@ -1323,8 +1323,8 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
   let explicit = def.signature.explicit_info in
   (let space = Some space in
    extract_generic_params def.item_meta.span ctx fmt TypeDeclId.Set.empty ~space
-     ~trait_decl def.signature.generics (Some explicit) type_params cg_params
-     trait_clauses);
+     ~trait_decl Item def.signature.generics (Some explicit) type_params
+     cg_params trait_clauses);
   (* Close the box for the generics *)
   F.pp_close_box fmt ();
   (* The input parameters - note that doing this adds bindings to the context *)
@@ -1363,22 +1363,16 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
 
     This is used for opaque function declarations, in particular.
  *)
-let extract_fun_input_parameters_types (ctx : extraction_ctx)
-    (fmt : F.formatter) (def : fun_decl) : unit =
+let extract_fun_input_parameters_types (span : span) (ctx : extraction_ctx)
+    (fmt : F.formatter) (inputs : ty list) : unit =
   let extract_param (ty : ty) : unit =
     let inside = false in
-    extract_ty def.item_meta.span ctx fmt TypeDeclId.Set.empty inside ty;
+    extract_ty span ctx fmt TypeDeclId.Set.empty inside ty;
     F.pp_print_space fmt ();
     extract_arrow fmt ();
     F.pp_print_space fmt ()
   in
-  List.iter extract_param def.signature.inputs
-
-let extract_fun_inputs_output_parameters_types (ctx : extraction_ctx)
-    (fmt : F.formatter) (def : fun_decl) : unit =
-  extract_fun_input_parameters_types ctx fmt def;
-  extract_ty def.item_meta.span ctx fmt TypeDeclId.Set.empty false
-    def.signature.output
+  List.iter extract_param inputs
 
 let assert_backend_supports_decreases_clauses (span : Meta.span) =
   match backend () with
@@ -1686,7 +1680,9 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
     (* For opaque definitions, as we don't have named parameters under the hand,
      * we don't print parameters in the form [(x : a) (y : b) ...] above,
      * but wait until here to print the types: [a -> b -> ...]. *)
-    if is_opaque then extract_fun_input_parameters_types ctx fmt def;
+    if is_opaque then
+      extract_fun_input_parameters_types def.item_meta.span ctx fmt
+        def.signature.inputs;
     (* [Tot] *)
     if has_decreases_clause then (
       assert_backend_supports_decreases_clauses def.item_meta.span;
@@ -1891,7 +1887,7 @@ let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add the type/const gen parameters - note that we need those bindings
      only for the generation of the type (they are not top-level) *)
   let ctx, _, _, _ =
-    ctx_add_generic_params def.item_meta.span def.item_meta.name
+    ctx_add_generic_params def.item_meta.span def.item_meta.name Item
       def.signature.llbc_generics def.signature.generics ctx
   in
   (* Add breaks to insert new lines between definitions *)
@@ -1907,7 +1903,8 @@ let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_open_hovbox fmt 0;
   F.pp_print_string fmt "“:";
   (* Generate the type *)
-  extract_fun_input_parameters_types ctx fmt def;
+  extract_fun_input_parameters_types def.item_meta.span ctx fmt
+    def.signature.inputs;
   extract_ty def.item_meta.span ctx fmt TypeDeclId.Set.empty false
     def.signature.output;
   (* Close the box for the type *)
@@ -1984,7 +1981,7 @@ let extract_global_decl_body_gen (span : Meta.span) (ctx : extraction_ctx)
   (* Extract the generic parameters *)
   let space = ref true in
   extract_generic_params span ctx fmt TypeDeclId.Set.empty ~space:(Some space)
-    generics (Some explicit) type_params cg_params trait_clauses;
+    Item generics (Some explicit) type_params cg_params trait_clauses;
   if not !space then F.pp_print_space fmt ();
 
   (* Open ": TYPE =" box (depth=2) *)
@@ -2121,7 +2118,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
   in
   (* Add the type parameters *)
   let ctx, type_params, cg_params, trait_clauses =
-    ctx_add_generic_params span global.item_meta.name global.llbc_generics
+    ctx_add_generic_params span global.item_meta.name Item global.llbc_generics
       global.generics ctx
   in
   match body.body with
@@ -2363,7 +2360,6 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
         in
         List.map
           (fun (name, bound_fn) ->
-            let open Charon.Types in
             compute_item_name name bound_fn.binder_value.fun_id)
           required_methods
     | Some info ->
@@ -2539,58 +2535,57 @@ let explicit_info_drop_prefix (g1 : generic_params) (g2 : explicit_info) :
  *)
 let extract_trait_decl_method_items_aux (ctx : extraction_ctx)
     (fmt : F.formatter) (decl : trait_decl) (item_name : string)
-    (id : fun_decl_id) : unit =
+    (fn : fun_decl_ref binder) : unit =
   (* Lookup the definition *)
+  let fun_decl_id = fn.binder_value.fun_id in
   let trans =
     silent_unwrap_opt_span __FILE__ __LINE__ None
-      (A.FunDeclId.Map.find_opt id ctx.trans_funs)
+      (A.FunDeclId.Map.find_opt fun_decl_id ctx.trans_funs)
   in
+  let span = trans.f.item_meta.span in
   (* Extract the items *)
-  let f = trans.f in
-  let fun_name =
-    ctx_get_trait_method decl.item_meta.span decl.def_id item_name ctx
-  in
+  let fun_name = ctx_get_trait_method span decl.def_id item_name ctx in
   let ty () =
-    (* Extract the generics *)
-    (* We need to add the generics specific to the method, by removing those
-       which actually apply to the trait decl *)
-    let generics, explicit_info =
-      let drop_trait_clauses = false in
-      ( generic_params_drop_prefix ~drop_trait_clauses decl.generics
-          f.signature.generics,
-        explicit_info_drop_prefix decl.generics f.signature.explicit_info )
-    in
-    (* Note that we do not filter the LLBC generic parameters.
-       This is ok because:
-       - we only use them to find meaningful names for the trait clauses
-       - we only generate trait clauses for the clauses we find in the
-         pure generics *)
+    let method_llbc_generics = fn.binder_llbc_generics in
+    let method_generics = fn.binder_generics in
+    let method_explicit_info = fn.binder_explicit_info in
     let ctx, type_params, cg_params, trait_clauses =
-      ctx_add_generic_params decl.item_meta.span f.item_meta.name
-        f.signature.llbc_generics generics ctx
+      ctx_add_generic_params span trans.f.item_meta.name Method
+        method_llbc_generics method_generics ctx
     in
     let backend_uses_forall =
       match backend () with
       | Coq | Lean -> true
       | FStar | HOL4 -> false
     in
-    let generics_not_empty = generics <> empty_generic_params in
+    let generics_not_empty = method_generics <> empty_generic_params in
     let use_forall = generics_not_empty && backend_uses_forall in
     let use_arrows = generics_not_empty && not backend_uses_forall in
     let use_forall_use_sep = false in
-    extract_generic_params decl.item_meta.span ctx fmt TypeDeclId.Set.empty
-      ~use_forall ~use_forall_use_sep ~use_arrows generics (Some explicit_info)
-      type_params cg_params trait_clauses;
+    extract_generic_params span ctx fmt TypeDeclId.Set.empty ~use_forall
+      ~use_forall_use_sep ~use_arrows Method method_generics
+      (Some method_explicit_info) type_params cg_params trait_clauses;
     if use_forall then F.pp_print_string fmt ",";
+
     (* Extract the inputs and output *)
     F.pp_print_space fmt ();
-    extract_fun_inputs_output_parameters_types ctx fmt f
+    (* We substitute the function item generics in temrs of the trait + method
+       generics. *)
+    let signature = trans.f.signature in
+    let subst =
+      make_subst_from_generics signature.generics fn.binder_value.fun_generics
+    in
+    let ({ inputs; output; _ } : fun_sig) = signature in
+    let inputs = List.map (ty_substitute subst) inputs in
+    let output = ty_substitute subst output in
+    extract_fun_input_parameters_types span ctx fmt inputs;
+    extract_ty span ctx fmt TypeDeclId.Set.empty false output
   in
   extract_trait_decl_item ctx fmt fun_name ty
 
 let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
-    (decl : trait_decl) (item_name : string) (id : fun_decl_id) : unit =
-  try extract_trait_decl_method_items_aux ctx fmt decl item_name id
+    (decl : trait_decl) (item_name : string) (fn : fun_decl_ref binder) : unit =
+  try extract_trait_decl_method_items_aux ctx fmt decl item_name fn
   with CFailure _ ->
     F.pp_print_space fmt ();
     extract_admit fmt
@@ -2644,10 +2639,10 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add the type and const generic params - note that we need those bindings only for the
    * body translation (they are not top-level) *)
   let ctx, type_params, cg_params, trait_clauses =
-    ctx_add_generic_params decl.item_meta.span decl.item_meta.name
+    ctx_add_generic_params decl.item_meta.span decl.item_meta.name Item
       decl.llbc_generics generics ctx
   in
-  extract_generic_params decl.item_meta.span ctx fmt TypeDeclId.Set.empty
+  extract_generic_params decl.item_meta.span ctx fmt TypeDeclId.Set.empty Item
     generics (Some decl.explicit_info) type_params cg_params trait_clauses;
 
   F.pp_print_space fmt ();
@@ -2725,9 +2720,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
 
     (* The required methods *)
     List.iter
-      (fun (name, fn) ->
-        let open Charon.Types in
-        extract_trait_decl_method_items ctx fmt decl name fn.binder_value.fun_id)
+      (fun (name, fn) -> extract_trait_decl_method_items ctx fmt decl name fn)
       decl.required_methods;
 
     (* Close the outer boxes for the definition *)
@@ -2792,15 +2785,8 @@ let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
   (* The required methods *)
   List.iter
     (fun (item_name, bound_fn) ->
-      let open Charon.Types in
-      let fun_id = bound_fn.binder_value.fun_id in
-      (* Lookup the definition to retrieve the information about the explicit/implicit parameters *)
-      let trans = A.FunDeclId.Map.find fun_id ctx.trans_funs in
-      let f = trans.f in
-      let explicit_info =
-        explicit_info_drop_prefix decl.generics f.signature.explicit_info
-      in
-      (* TODO: this is likely incorrect, we should instantiate the binders properly *)
+      let explicit_info = bound_fn.binder_explicit_info in
+      (* TODO: this looks incorrect, we should instantiate the binder properly *)
       let params =
         params
         @ List.concat
@@ -2831,139 +2817,46 @@ let extract_trait_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
  *)
 let extract_trait_impl_method_items_aux (ctx : extraction_ctx)
     (fmt : F.formatter) (impl : trait_impl) (item_name : string)
-    (id : fun_decl_id) (impl_generics : string list * string list * string list)
-    : unit =
+    (fn : fun_decl_ref binder) : unit =
+  let span = impl.item_meta.span in
   let trait_decl_id = impl.impl_trait.trait_decl_id in
+  let method_decl_id = fn.binder_value.fun_id in
   (* Lookup the definition *)
   let trans =
     silent_unwrap_opt_span __FILE__ __LINE__ None
-      (A.FunDeclId.Map.find_opt id ctx.trans_funs)
+      (A.FunDeclId.Map.find_opt method_decl_id ctx.trans_funs)
   in
   (* Extract the items *)
-  let f = trans.f in
-  let fun_name =
-    ctx_get_trait_method impl.item_meta.span trait_decl_id item_name ctx
-  in
+  let fun_name = ctx_get_trait_method span trait_decl_id item_name ctx in
   let ty () =
-    (* Filter the generics if the method is a builtin *)
-    let i_tys, i_cgs, _ = impl_generics in
-    let ( impl_types,
-          impl_cgs,
-          i_tys,
-          i_cgs,
-          f_tys,
-          f_cgs,
-          f_all_explicit_tys,
-          f_explicit_tys,
-          f_all_explicit_cgs,
-          f_explicit_cgs ) =
-      match FunDeclId.Map.find_opt f.def_id ctx.funs_filter_type_args_map with
-      | None ->
-          ( impl.generics.types,
-            impl.generics.const_generics,
-            i_tys,
-            i_cgs,
-            f.signature.generics.types,
-            f.signature.generics.const_generics,
-            f.signature.explicit_info.explicit_types,
-            f.signature.explicit_info.explicit_types,
-            f.signature.explicit_info.explicit_const_generics,
-            f.signature.explicit_info.explicit_const_generics )
-      | Some filter ->
-          let filter_list : 'a. bool list -> 'a list -> 'a list =
-           fun filter ls ->
-            let ls = List.combine filter ls in
-            List.filter_map (fun (b, ty) -> if b then Some ty else None) ls
-          in
-          let impl_types = impl.generics.types in
-          let impl_cgs = impl.generics.const_generics in
-          let impl_filter : 'a. 'a list -> bool list =
-           fun l -> Collections.List.prefix (List.length l) filter
-          in
-          let i_tys = i_tys in
-          let i_filter : 'a. 'a list -> bool list =
-           fun l -> Collections.List.prefix (List.length l) filter
-          in
-          ( filter_list (impl_filter impl_types) impl_types,
-            filter_list (impl_filter impl_cgs) impl_cgs,
-            filter_list (i_filter i_tys) i_tys,
-            filter_list (i_filter i_cgs) i_cgs,
-            filter_list filter f.signature.generics.types,
-            filter_list filter f.signature.generics.const_generics,
-            f.signature.explicit_info.explicit_types,
-            filter_list filter f.signature.explicit_info.explicit_types,
-            f.signature.explicit_info.explicit_const_generics,
-            filter_list filter f.signature.explicit_info.explicit_const_generics
-          )
-    in
-    let f_generics =
-      { f.signature.generics with types = f_tys; const_generics = f_cgs }
-    in
-    let f_explicit =
-      {
-        explicit_types = f_explicit_tys;
-        explicit_const_generics = f_explicit_cgs;
-      }
-    in
     (* Extract the generics - we need to quantify over the generics which
        are specific to the method, and call it will all the generics
        (trait impl + method generics) *)
-    let f_generics =
-      let drop_trait_clauses = true in
-      generic_params_drop_prefix ~drop_trait_clauses
-        { impl.generics with types = impl_types; const_generics = impl_cgs }
-        f_generics
-    in
-    (* Register and print the quantified generics.
-
-       Note that we do not filter the LLBC generic parameters.
-       This is ok because:
-       - we only use them to find meaningful names for the trait clauses
-       - we only generate trait clauses for the clauses we find in the
-         pure generics *)
-    let ctx, f_tys, f_cgs, f_tcs =
-      ctx_add_generic_params impl.item_meta.span f.item_meta.name
-        f.signature.llbc_generics f_generics ctx
+    let method_generics = fn.binder_generics in
+    let method_llbc_generics = fn.binder_llbc_generics in
+    let ctx, method_tys, method_cgs, method_tcs =
+      ctx_add_generic_params span trans.f.item_meta.name Method
+        method_llbc_generics method_generics ctx
     in
-    let use_forall = f_generics <> empty_generic_params in
-    extract_generic_params impl.item_meta.span ctx fmt TypeDeclId.Set.empty
-      ~use_forall f_generics (Some f_explicit) f_tys f_cgs f_tcs;
+    let use_forall = method_generics <> empty_generic_params in
+    extract_generic_params span ctx fmt TypeDeclId.Set.empty ~use_forall Method
+      method_generics None method_tys method_cgs method_tcs;
     if use_forall then F.pp_print_string fmt ",";
+
     (* Extract the function call *)
     F.pp_print_space fmt ();
-    let fun_name =
-      ctx_get_local_function impl.item_meta.span f.def_id None ctx
-    in
+    let fun_name = ctx_get_local_function span method_decl_id None ctx in
     F.pp_print_string fmt fun_name;
-    let all_generics =
-      let _, _, i_tcs = impl_generics in
-      (* Filter the implicit arguments *)
-      let filter : 'a. explicit list -> 'a list -> 'a list =
-       fun bl l ->
-        List.filter_map
-          (fun (e, x) -> if e = Explicit then Some x else None)
-          (List.combine bl l)
-      in
-      let tys = filter f_all_explicit_tys (i_tys @ f_tys) in
-      let cgs = filter f_all_explicit_cgs (i_cgs @ f_cgs) in
-
-      (* Put everything together *)
-      List.concat [ tys; cgs; i_tcs; f_tcs ]
-    in
-
-    List.iter
-      (fun p ->
-        F.pp_print_space fmt ();
-        F.pp_print_string fmt p)
-      all_generics
+    extract_generic_args span ctx fmt TypeDeclId.Set.empty
+      ~explicit:(Some trans.f.signature.explicit_info)
+      fn.binder_value.fun_generics
   in
+
   extract_trait_impl_item ctx fmt fun_name ty
 
 let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
-    (impl : trait_impl) (item_name : string) (id : fun_decl_id)
-    (impl_generics : string list * string list * string list) : unit =
-  try
-    extract_trait_impl_method_items_aux ctx fmt impl item_name id impl_generics
+    (impl : trait_impl) (item_name : string) (fn : fun_decl_ref binder) : unit =
+  try extract_trait_impl_method_items_aux ctx fmt impl item_name fn
   with CFailure _ ->
     F.pp_print_space fmt ();
     extract_admit fmt
@@ -3027,11 +2920,10 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add the type and const generic params - note that we need those bindings only for the
    * body translation (they are not top-level) *)
   let ctx, type_params, cg_params, trait_clauses =
-    ctx_add_generic_params impl.item_meta.span impl.item_meta.name
+    ctx_add_generic_params impl.item_meta.span impl.item_meta.name Item
       impl.llbc_generics impl.generics ctx
   in
-  let all_generics = (type_params, cg_params, trait_clauses) in
-  extract_generic_params impl.item_meta.span ctx fmt TypeDeclId.Set.empty
+  extract_generic_params impl.item_meta.span ctx fmt TypeDeclId.Set.empty Item
     impl.generics (Some impl.explicit_info) type_params cg_params trait_clauses;
 
   (* Print the type *)
@@ -3132,9 +3024,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
     (* The required methods *)
     List.iter
       (fun (name, bound_fn) ->
-        let open Charon.Types in
-        let id = bound_fn.binder_value.fun_id in
-        extract_trait_impl_method_items ctx fmt impl name id all_generics)
+        extract_trait_impl_method_items ctx fmt impl name bound_fn)
       impl.required_methods;
 
     (* Close the outer boxes for the definition, as well as the brackets *)
diff --git a/src/extract/ExtractBase.ml b/src/extract/ExtractBase.ml
index ee9007f5..2c3835a9 100644
--- a/src/extract/ExtractBase.ml
+++ b/src/extract/ExtractBase.ml
@@ -113,8 +113,18 @@ let decl_is_not_last_from_group (kind : decl_kind) : bool =
 
 type type_decl_kind = Enum | Struct | Tuple [@@deriving show]
 
+(** Generics can be bound in two places: each item has its generics, and
+    additionally within a trait decl or impl each method has its own generics.
+    We distinguish these two cases here. In charon, the distinction is made
+    thanks to `de_bruijn_var`.
+    Note that for the generics of a top-level `fun_decl` we always use `Item`;
+    `Method` only refers to the inner binder found in the list of methods in a
+    trait_decl/trait_impl.
+    *)
+type generic_origin = Item | Method
+
 (** We use identifiers to look for name clashes *)
-type id =
+and id =
   | GlobalId of A.GlobalDeclId.id
   | FunId of fun_id
   | TerminationMeasureId of (A.fun_id * LoopId.id option)
@@ -162,12 +172,12 @@ type id =
           must be unique (it is the case in F* ) which is why we register
           them here.
        *)
-  | TypeVarId of TypeVarId.id
-  | ConstGenericVarId of ConstGenericVarId.id
   | VarId of VarId.id
   | TraitDeclId of TraitDeclId.id
   | TraitImplId of TraitImplId.id
-  | LocalTraitClauseId of TraitClauseId.id
+  | TypeVarId of generic_origin * TypeVarId.id
+  | ConstGenericVarId of generic_origin * ConstGenericVarId.id
+  | LocalTraitClauseId of generic_origin * TraitClauseId.id
   | TraitDeclConstructorId of TraitDeclId.id
   | TraitMethodId of TraitDeclId.id * string
   | TraitItemId of TraitDeclId.id * string
@@ -674,14 +684,19 @@ let id_to_string (span : Meta.span option) (id : id) (ctx : extraction_ctx) :
       let field_name = adt_field_to_string span ctx id field_id in
       "type name: " ^ type_name ^ ", field name: " ^ field_name
   | UnknownId -> "keyword"
-  | TypeVarId id -> "type_var_id: " ^ TypeVarId.to_string id
-  | ConstGenericVarId id ->
-      "const_generic_var_id: " ^ ConstGenericVarId.to_string id
   | VarId id -> "var_id: " ^ VarId.to_string id
   | TraitDeclId id -> "trait_decl_id: " ^ TraitDeclId.to_string id
   | TraitImplId id -> "trait_impl_id: " ^ TraitImplId.to_string id
-  | LocalTraitClauseId id ->
-      "local_trait_clause_id: " ^ TraitClauseId.to_string id
+  | TypeVarId (origin, id) ->
+      "type_var_id: " ^ TypeVarId.to_string id ^ " from "
+      ^ show_generic_origin origin
+  | ConstGenericVarId (origin, id) ->
+      "const_generic_var_id: "
+      ^ ConstGenericVarId.to_string id
+      ^ " from " ^ show_generic_origin origin
+  | LocalTraitClauseId (origin, id) ->
+      "local_trait_clause_id: " ^ TraitClauseId.to_string id ^ " from "
+      ^ show_generic_origin origin
   | TraitDeclConstructorId id ->
       "trait_decl_constructor: " ^ trait_decl_id_to_string id
   | TraitParentClauseId (id, clause_id) ->
@@ -771,17 +786,32 @@ let ctx_get_var (span : Meta.span) (id : VarId.id) (ctx : extraction_ctx) :
     string =
   ctx_get (Some span) (VarId id) ctx
 
-let ctx_get_type_var (span : Meta.span) (id : TypeVarId.id)
-    (ctx : extraction_ctx) : string =
-  ctx_get (Some span) (TypeVarId id) ctx
+(** This warrants explanations. Charon supports several levels of nested
+  binders; however there are currently only two cases where we bind
+  non-lifetime variables: at the top-level of each item, and for each method
+  inside a trait_decl/trait_impl. Moreover, we use `Free` vars to identify
+  item-bound vars. This means that we can identify which binder a variable
+  comes from without rigorously tracking binder levels, which is what this
+  function does.
+  Note that the `de_bruijn_id`s are wrong anyway because we kept charon's
+  binding levels but forgot all the region binders.
+  *)
+let origin_from_de_bruijn_var (var : 'a de_bruijn_var) : generic_origin * 'a =
+  match var with
+  | Bound (_, id) -> (Method, id)
+  | Free id -> (Item, id)
 
-let ctx_get_const_generic_var (span : Meta.span) (id : ConstGenericVarId.id)
-    (ctx : extraction_ctx) : string =
-  ctx_get (Some span) (ConstGenericVarId id) ctx
+let ctx_get_type_var (span : Meta.span) (origin : generic_origin)
+    (id : TypeVarId.id) (ctx : extraction_ctx) : string =
+  ctx_get (Some span) (TypeVarId (origin, id)) ctx
 
-let ctx_get_local_trait_clause (span : Meta.span) (id : TraitClauseId.id)
-    (ctx : extraction_ctx) : string =
-  ctx_get (Some span) (LocalTraitClauseId id) ctx
+let ctx_get_const_generic_var (span : Meta.span) (origin : generic_origin)
+    (id : ConstGenericVarId.id) (ctx : extraction_ctx) : string =
+  ctx_get (Some span) (ConstGenericVarId (origin, id)) ctx
+
+let ctx_get_local_trait_clause (span : Meta.span) (origin : generic_origin)
+    (id : TraitClauseId.id) (ctx : extraction_ctx) : string =
+  ctx_get (Some span) (LocalTraitClauseId (origin, id)) ctx
 
 let ctx_get_field (span : Meta.span) (type_id : type_id) (field_id : FieldId.id)
     (ctx : extraction_ctx) : string =
@@ -1956,27 +1986,29 @@ let basename_to_unique (ctx : extraction_ctx) (name : string) =
   basename_to_unique_aux collision name_append_index name
 
 (** Generate a unique type variable name and add it to the context *)
-let ctx_add_type_var (span : Meta.span) (basename : string) (id : TypeVarId.id)
-    (ctx : extraction_ctx) : extraction_ctx * string =
+let ctx_add_type_var (span : Meta.span) (origin : generic_origin)
+    (basename : string) (id : TypeVarId.id) (ctx : extraction_ctx) :
+    extraction_ctx * string =
   let name = ctx_compute_type_var_basename ctx basename in
   let name = basename_to_unique ctx name in
-  let ctx = ctx_add span (TypeVarId id) name ctx in
+  let ctx = ctx_add span (TypeVarId (origin, id)) name ctx in
   (ctx, name)
 
 (** Generate a unique const generic variable name and add it to the context *)
-let ctx_add_const_generic_var (span : Meta.span) (basename : string)
-    (id : ConstGenericVarId.id) (ctx : extraction_ctx) : extraction_ctx * string
-    =
+let ctx_add_const_generic_var (span : Meta.span) (origin : generic_origin)
+    (basename : string) (id : ConstGenericVarId.id) (ctx : extraction_ctx) :
+    extraction_ctx * string =
   let name = ctx_compute_const_generic_var_basename ctx basename in
   let name = basename_to_unique ctx name in
-  let ctx = ctx_add span (ConstGenericVarId id) name ctx in
+  let ctx = ctx_add span (ConstGenericVarId (origin, id)) name ctx in
   (ctx, name)
 
 (** See {!ctx_add_type_var} *)
-let ctx_add_type_vars (span : Meta.span) (vars : (string * TypeVarId.id) list)
-    (ctx : extraction_ctx) : extraction_ctx * string list =
+let ctx_add_type_vars (span : Meta.span) (origin : generic_origin)
+    (vars : (string * TypeVarId.id) list) (ctx : extraction_ctx) :
+    extraction_ctx * string list =
   List.fold_left_map
-    (fun ctx (name, id) -> ctx_add_type_var span name id ctx)
+    (fun ctx (name, id) -> ctx_add_type_var span origin name id ctx)
     ctx vars
 
 (** Generate a unique variable name and add it to the context *)
@@ -1995,10 +2027,11 @@ let ctx_add_trait_self_clause (span : Meta.span) (ctx : extraction_ctx) :
   (ctx, name)
 
 (** Generate a unique trait clause name and add it to the context *)
-let ctx_add_local_trait_clause (span : Meta.span) (basename : string)
-    (id : TraitClauseId.id) (ctx : extraction_ctx) : extraction_ctx * string =
+let ctx_add_local_trait_clause (span : Meta.span) (origin : generic_origin)
+    (basename : string) (id : TraitClauseId.id) (ctx : extraction_ctx) :
+    extraction_ctx * string =
   let name = basename_to_unique ctx basename in
-  let ctx = ctx_add span (LocalTraitClauseId id) name ctx in
+  let ctx = ctx_add span (LocalTraitClauseId (origin, id)) name ctx in
   (ctx, name)
 
 (** See {!ctx_add_var} *)
@@ -2010,18 +2043,20 @@ let ctx_add_vars (span : Meta.span) (vars : var list) (ctx : extraction_ctx) :
       ctx_add_var span name v.id ctx)
     ctx vars
 
-let ctx_add_type_params (span : Meta.span) (vars : type_var list)
-    (ctx : extraction_ctx) : extraction_ctx * string list =
+let ctx_add_type_params (span : Meta.span) (origin : generic_origin)
+    (vars : type_var list) (ctx : extraction_ctx) : extraction_ctx * string list
+    =
   List.fold_left_map
-    (fun ctx (var : type_var) -> ctx_add_type_var span var.name var.index ctx)
+    (fun ctx (var : type_var) ->
+      ctx_add_type_var span origin var.name var.index ctx)
     ctx vars
 
-let ctx_add_const_generic_params (span : Meta.span)
+let ctx_add_const_generic_params (span : Meta.span) (origin : generic_origin)
     (vars : const_generic_var list) (ctx : extraction_ctx) :
     extraction_ctx * string list =
   List.fold_left_map
     (fun ctx (var : const_generic_var) ->
-      ctx_add_const_generic_var span var.name var.index ctx)
+      ctx_add_const_generic_var span origin var.name var.index ctx)
     ctx vars
 
 (** Returns the lists of names for:
@@ -2034,16 +2069,16 @@ let ctx_add_const_generic_params (span : Meta.span)
     for additional information.
   *)
 let ctx_add_local_trait_clauses (span : Meta.span)
-    (current_def_name : Types.name) (llbc_generics : Types.generic_params)
-    (clauses : trait_clause list) (ctx : extraction_ctx) :
-    extraction_ctx * string list =
+    (current_def_name : Types.name) (origin : generic_origin)
+    (llbc_generics : Types.generic_params) (clauses : trait_clause list)
+    (ctx : extraction_ctx) : extraction_ctx * string list =
   List.fold_left_map
     (fun ctx (c : trait_clause) ->
       let basename =
         ctx_compute_trait_clause_basename ctx current_def_name llbc_generics
           c.clause_id
       in
-      ctx_add_local_trait_clause span basename c.clause_id ctx)
+      ctx_add_local_trait_clause span origin basename c.clause_id ctx)
     ctx clauses
 
 (** Returns the lists of names for:
@@ -2056,14 +2091,14 @@ let ctx_add_local_trait_clauses (span : Meta.span)
     for additional information.
   *)
 let ctx_add_generic_params (span : Meta.span) (current_def_name : Types.name)
-    (llbc_generics : Types.generic_params) (generics : generic_params)
-    (ctx : extraction_ctx) :
+    (origin : generic_origin) (llbc_generics : Types.generic_params)
+    (generics : generic_params) (ctx : extraction_ctx) :
     extraction_ctx * string list * string list * string list =
   let { types; const_generics; trait_clauses } = generics in
-  let ctx, tys = ctx_add_type_params span types ctx in
-  let ctx, cgs = ctx_add_const_generic_params span const_generics ctx in
+  let ctx, tys = ctx_add_type_params span origin types ctx in
+  let ctx, cgs = ctx_add_const_generic_params span origin const_generics ctx in
   let ctx, tcs =
-    ctx_add_local_trait_clauses span current_def_name llbc_generics
+    ctx_add_local_trait_clauses span current_def_name origin llbc_generics
       trait_clauses ctx
   in
   (ctx, tys, cgs, tcs)
diff --git a/src/extract/ExtractTypes.ml b/src/extract/ExtractTypes.ml
index 7af7b5c3..3a73c55c 100644
--- a/src/extract/ExtractTypes.ml
+++ b/src/extract/ExtractTypes.ml
@@ -429,8 +429,8 @@ let extract_const_generic (span : Meta.span) (ctx : extraction_ctx)
       F.pp_print_string fmt s
   | CgValue v -> extract_literal span fmt false inside v
   | CgVar var ->
-      let id = TypesUtils.expect_free_var (Some span) var in
-      let s = ctx_get_const_generic_var span id ctx in
+      let origin, id = origin_from_de_bruijn_var var in
+      let s = ctx_get_const_generic_var span origin id ctx in
       F.pp_print_string fmt s
 
 let extract_literal_type (_ctx : extraction_ctx) (fmt : F.formatter)
@@ -582,7 +582,9 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
                 Collections.List.iter_link (F.pp_print_space fmt)
                   (extract_trait_ref span ctx fmt no_params_tys true)
                   trait_refs)))
-  | TVar vid -> F.pp_print_string fmt (ctx_get_type_var span vid ctx)
+  | TVar var ->
+      let origin, id = origin_from_de_bruijn_var var in
+      F.pp_print_string fmt (ctx_get_type_var span origin id ctx)
   | TLiteral lty -> extract_literal_type ctx fmt lty
   | TArrow (arg_ty, ret_ty) ->
       if inside then F.pp_print_string fmt "(";
@@ -772,8 +774,9 @@ and extract_trait_instance_id (span : Meta.span) (ctx : extraction_ctx)
       F.pp_print_string fmt name;
       extract_generic_args span ctx fmt no_params_tys ~explicit generics;
       if use_brackets then F.pp_print_string fmt ")"
-  | Clause id ->
-      let name = ctx_get_local_trait_clause span id ctx in
+  | Clause var ->
+      let origin, id = origin_from_de_bruijn_var var in
+      let name = ctx_get_local_trait_clause span origin id ctx in
       F.pp_print_string fmt name
   | ParentClause (inst_id, decl_id, clause_id) ->
       (* Use the trait decl id to lookup the name *)
@@ -1295,9 +1298,10 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx)
     (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) ?(use_forall = false)
     ?(use_forall_use_sep = true) ?(use_arrows = false)
     ?(as_implicits : bool = false) ?(space : bool ref option = None)
-    ?(trait_decl : trait_decl option = None) (generics : generic_params)
-    (explicit : explicit_info option) (type_params : string list)
-    (cg_params : string list) (trait_clauses : string list) : unit =
+    ?(trait_decl : trait_decl option = None) (origin : generic_origin)
+    (generics : generic_params) (explicit : explicit_info option)
+    (type_params : string list) (cg_params : string list)
+    (trait_clauses : string list) : unit =
   let all_params = List.concat [ type_params; cg_params; trait_clauses ] in
   (* HOL4 doesn't support const generics *)
   cassert __FILE__ __LINE__
@@ -1359,7 +1363,7 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx)
             insert_req_space ();
             (* ( *)
             left_bracket expl;
-            let n = ctx_get_const_generic_var span var.index ctx in
+            let n = ctx_get_const_generic_var span origin var.index ctx in
             print_implicit_symbol expl;
             F.pp_print_string fmt n;
             F.pp_print_space fmt ();
@@ -1378,7 +1382,7 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx)
           insert_req_space ();
           (* ( *)
           left_bracket expl;
-          let n = ctx_get_local_trait_clause span clause.clause_id ctx in
+          let n = ctx_get_local_trait_clause span origin clause.clause_id ctx in
           print_implicit_symbol expl;
           F.pp_print_string fmt n;
           F.pp_print_space fmt ();
@@ -1445,12 +1449,12 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx)
               map snd dtype_params;
               map
                 (fun ((_, cg) : _ * const_generic_var) ->
-                  ctx_get_const_generic_var trait_decl.item_meta.span cg.index
-                    ctx)
+                  ctx_get_const_generic_var trait_decl.item_meta.span origin
+                    cg.index ctx)
                 dcgs;
               map
                 (fun (_, c) ->
-                  ctx_get_local_trait_clause trait_decl.item_meta.span
+                  ctx_get_local_trait_clause trait_decl.item_meta.span origin
                     c.clause_id ctx)
                 dtrait_clauses;
             ]
@@ -1507,7 +1511,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add the type and const generic params - note that we need those bindings only for the
    * body translation (they are not top-level) *)
   let ctx_body, type_params, cg_params, trait_clauses =
-    ctx_add_generic_params def.item_meta.span def.item_meta.name
+    ctx_add_generic_params def.item_meta.span def.item_meta.name Item
       def.llbc_generics def.generics ctx
   in
   (* Add a break before *)
@@ -1553,7 +1557,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
     "Constant generics and type definitions with trait clauses are not \
      supported yet when generating code for HOL4";
   (* Print the generic parameters *)
-  extract_generic_params def.item_meta.span ctx_body fmt type_decl_group
+  extract_generic_params def.item_meta.span ctx_body fmt type_decl_group Item
     ~use_forall def.generics (Some def.explicit_info) type_params cg_params
     trait_clauses;
   (* Print the "=" if we extract the body*)
@@ -1795,7 +1799,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
       if is_rec then
         (* Add the type params *)
         let ctx, type_params, cg_params, trait_clauses =
-          ctx_add_generic_params decl.item_meta.span decl.item_meta.name
+          ctx_add_generic_params decl.item_meta.span decl.item_meta.name Item
             decl.llbc_generics decl.generics ctx
         in
         (* Record_var will be the ADT argument to the projector *)
@@ -1855,8 +1859,8 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
           (* Print the generics *)
           let as_implicits = true in
           extract_generic_params decl.item_meta.span ctx fmt
-            TypeDeclId.Set.empty ~as_implicits decl.generics None type_params
-            cg_params trait_clauses;
+            TypeDeclId.Set.empty Item ~as_implicits decl.generics None
+            type_params cg_params trait_clauses;
 
           (* Print the record parameter as "(x : ADT)" *)
           F.pp_print_space fmt ();
@@ -1996,8 +2000,8 @@ let extract_type_decl_record_field_projectors_simp_lemmas (ctx : extraction_ctx)
       if is_rec then
         (* Add the type params *)
         let ctx, type_params, cg_params, trait_clauses =
-          ctx_add_generic_params span decl.item_meta.name decl.llbc_generics
-            decl.generics ctx
+          ctx_add_generic_params span decl.item_meta.name Item
+            decl.llbc_generics decl.generics ctx
         in
         (* Name of the ADT *)
         let def_name = ctx_get_local_type span decl.def_id ctx in
@@ -2042,7 +2046,7 @@ let extract_type_decl_record_field_projectors_simp_lemmas (ctx : extraction_ctx)
           (* Print the generics *)
           let as_implicits = true in
           extract_generic_params span ctx fmt TypeDeclId.Set.empty ~as_implicits
-            decl.generics None type_params cg_params trait_clauses;
+            Item decl.generics None type_params cg_params trait_clauses;
 
           (* Print the input parameters (the fields) *)
           let print_field (ctx : extraction_ctx) (field_id : FieldId.id)
diff --git a/src/pure/PrintPure.ml b/src/pure/PrintPure.ml
index 54dbb46b..477703ef 100644
--- a/src/pure/PrintPure.ml
+++ b/src/pure/PrintPure.ml
@@ -11,7 +11,8 @@ open Errors
  *)
 type fmt_env = {
   crate : LlbcAst.crate;
-  generics : generic_params;
+  (* We need a list of params because we have nested binding levels for trait methods. *)
+  generics : generic_params list;
   vars : string VarId.Map.t;
 }
 
@@ -26,23 +27,46 @@ let fmt_env_push_locals (env : fmt_env) (vars : var list) : fmt_env =
 
 let var_id_to_pretty_string (id : var_id) : string = "^" ^ VarId.to_string id
 
-let type_var_id_to_string (env : fmt_env) (id : type_var_id) : string =
+let lookup_var_in_env (env : fmt_env)
+    (find_in : generic_params -> 'id -> 'b option) (var : 'id de_bruijn_var) :
+    'b option =
+  if List.length env.generics == 0 then None
+  else
+    let dbid, varid =
+      match var with
+      | Bound (dbid, varid) -> (dbid, varid)
+      | Free varid ->
+          let len = List.length env.generics in
+          let dbid = len - 1 in
+          (dbid, varid)
+    in
+    match List.nth_opt env.generics dbid with
+    | None -> None
+    | Some generics -> begin
+        match find_in generics varid with
+        | None -> None
+        | Some r -> Some r
+      end
+
+let type_db_var_to_string (env : fmt_env) (var : type_var_id de_bruijn_var) :
+    string =
   (* Note that the types are not necessarily ordered following their indices *)
-  match
-    List.find_opt (fun (x : type_var) -> x.index = id) env.generics.types
-  with
-  | None -> Print.Types.type_var_id_to_pretty_string id
+  let find (generics : generic_params) varid =
+    List.find_opt (fun (v : type_var) -> v.index = varid) generics.types
+  in
+  match lookup_var_in_env env find var with
+  | None -> Print.Types.type_db_var_to_pretty_string var
   | Some x -> Print.Types.type_var_to_string x
 
-let const_generic_var_id_to_string (env : fmt_env) (id : const_generic_var_id) :
-    string =
-  (* Note that the regions are not necessarily ordered following their indices *)
-  match
+let const_generic_db_var_to_string (env : fmt_env)
+    (var : const_generic_var_id de_bruijn_var) : string =
+  let find (generics : generic_params) varid =
     List.find_opt
-      (fun (x : const_generic_var) -> x.index = id)
-      env.generics.const_generics
-  with
-  | None -> Print.Types.const_generic_var_id_to_pretty_string id
+      (fun (v : const_generic_var) -> v.index = varid)
+      generics.const_generics
+  in
+  match lookup_var_in_env env find var with
+  | None -> Print.Types.const_generic_db_var_to_pretty_string var
   | Some x -> Print.Types.const_generic_var_to_string x
 
 let var_id_to_string (env : fmt_env) (id : VarId.id) : string =
@@ -56,7 +80,11 @@ let fmt_env_to_llbc_fmt_env (env : fmt_env) : Print.fmt_env =
   Charon.PrintLlbcAst.Crate.crate_to_fmt_env env.crate
 
 let decls_ctx_to_fmt_env (ctx : Contexts.decls_ctx) : fmt_env =
-  { crate = ctx.crate; generics = empty_generic_params; vars = VarId.Map.empty }
+  {
+    crate = ctx.crate;
+    generics = [ empty_generic_params ];
+    vars = VarId.Map.empty;
+  }
 
 let name_to_string (env : fmt_env) =
   Print.Types.name_to_string (fmt_env_to_llbc_fmt_env env)
@@ -114,12 +142,10 @@ let type_id_to_string (env : fmt_env) (id : type_id) : string =
   | TTuple -> ""
   | TBuiltin aty -> builtin_ty_to_string aty
 
-(* TODO: duplicates  Charon.PrintTypes.const_generic_to_string *)
 let const_generic_to_string (env : fmt_env) (cg : const_generic) : string =
   match cg with
   | CgGlobal id -> global_decl_id_to_string env id
-  | CgVar var ->
-      const_generic_var_id_to_string env (Substitute.expect_free_var None var)
+  | CgVar var -> const_generic_db_var_to_string env var
   | CgValue lit -> literal_to_string lit
 
 let rec ty_to_string (env : fmt_env) (inside : bool) (ty : ty) : string =
@@ -136,7 +162,7 @@ let rec ty_to_string (env : fmt_env) (inside : bool) (ty : ty) : string =
           in
           let ty_s = type_id_to_string env id ^ generics_s in
           if generics <> [] && inside then "(" ^ ty_s ^ ")" else ty_s)
-  | TVar tv -> type_var_id_to_string env tv
+  | TVar tv -> type_db_var_to_string env tv
   | TLiteral lty -> literal_type_to_string lty
   | TArrow (arg_ty, ret_ty) ->
       let ty =
@@ -179,7 +205,7 @@ and trait_instance_id_to_string (env : fmt_env) (id : trait_instance_id) :
       let generics = generic_args_to_string env generics in
       let impl_id = trait_impl_id_to_string env impl_id in
       impl_id ^ generics
-  | Clause id -> trait_clause_id_to_string env id
+  | Clause var -> Print.Types.trait_db_var_to_pretty_string var
   | ParentClause (inst_id, _decl_id, clause_id) ->
       let inst_id = trait_instance_id_to_string env inst_id in
       let clause_id = trait_clause_id_to_string env clause_id in
@@ -216,7 +242,7 @@ let variant_to_string env (v : variant) : string =
   ^ ")"
 
 let type_decl_to_string (env : fmt_env) (def : type_decl) : string =
-  let env = { env with generics = def.generics } in
+  let env = { env with generics = [ def.generics ] } in
   let name = def.name in
   let params =
     if def.generics = empty_generic_params then ""
@@ -463,7 +489,7 @@ let typed_pattern_to_string ?(span : Meta.span option = None) (env : fmt_env)
   snd (typed_pattern_to_string_aux span env v)
 
 let fun_sig_to_string (env : fmt_env) (sg : fun_sig) : string =
-  let env = { env with generics = sg.generics } in
+  let env = { env with generics = [ sg.generics ] } in
   let generics = generic_params_to_strings env sg.generics in
   let inputs = List.map (ty_to_string env false) sg.inputs in
   let output = ty_to_string env false sg.output in
@@ -541,7 +567,7 @@ let rec texpression_to_string ?(span : Meta.span option = None) (env : fmt_env)
     string =
   match e.e with
   | Var var_id -> var_id_to_string env var_id
-  | CVar cg_id -> const_generic_var_id_to_string env cg_id
+  | CVar cg_id -> const_generic_db_var_to_string env (Free cg_id)
   | Const cv -> literal_to_string cv
   | App _ ->
       (* Recursively destruct the app, to have a pair (app, arguments list) *)
@@ -773,7 +799,7 @@ and espan_to_string ?(span : Meta.span option = None) (env : fmt_env)
   "@span[" ^ espan ^ "]"
 
 let fun_decl_to_string (env : fmt_env) (def : fun_decl) : string =
-  let env = { env with generics = def.signature.generics } in
+  let env = { env with generics = [ def.signature.generics ] } in
   let name = def.name ^ fun_suffix def.loop_id in
   let signature = fun_sig_to_string env def.signature in
   match def.body with
diff --git a/src/pure/Pure.ml b/src/pure/Pure.ml
index 5d6dafb0..1e41ab0b 100644
--- a/src/pure/Pure.ml
+++ b/src/pure/Pure.ml
@@ -47,7 +47,6 @@ type trait_clause_id = T.trait_clause_id [@@deriving show, ord]
 type trait_item_name = T.trait_item_name [@@deriving show, ord]
 type global_decl_id = T.global_decl_id [@@deriving show, ord]
 type fun_decl_id = A.fun_decl_id [@@deriving show, ord]
-type fun_decl_ref = T.fun_decl_ref [@@deriving show, ord]
 type loop_id = LoopId.id [@@deriving show, ord]
 type region_group_id = T.region_group_id [@@deriving show, ord]
 type mutability = Mut | Const [@@deriving show, ord]
@@ -56,7 +55,7 @@ type file_name = Meta.file_name [@@deriving show, ord]
 type raw_span = Meta.raw_span [@@deriving show, ord]
 type span = Meta.span [@@deriving show, ord]
 type ref_kind = Types.ref_kind [@@deriving show, ord]
-type 'a binder = 'a Types.binder [@@deriving show, ord]
+type 'a de_bruijn_var = 'a Types.de_bruijn_var [@@deriving show, ord]
 
 (** The builtin types for the pure AST.
 
@@ -246,7 +245,8 @@ type ty =
           be able to only give back part of the ADT. We need a way to encode
           such "partial" ADTs.
        *)
-  | TVar of type_var_id
+  | TVar of type_var_id de_bruijn_var
+    (* Note: the `de_bruijn_id`s are incorrect, see comment on `translate_region_binder` *)
   | TLiteral of literal_type
   | TArrow of ty * ty
   | TTraitType of trait_ref * string
@@ -258,6 +258,11 @@ and trait_ref = {
   trait_decl_ref : trait_decl_ref;
 }
 
+and fun_decl_ref = {
+  fun_id : fun_decl_id;
+  fun_generics : generic_args; (* The name: annoying field collisions... *)
+}
+
 and trait_decl_ref = {
   trait_decl_id : trait_decl_id;
   decl_generics : generic_args; (* The name: annoying field collisions... *)
@@ -277,7 +282,8 @@ and generic_args = {
 and trait_instance_id =
   | Self
   | TraitImpl of trait_impl_id * generic_args
-  | Clause of trait_clause_id
+  | Clause of trait_clause_id de_bruijn_var
+    (* Note: the `de_bruijn_id`s are incorrect, see comment on `translate_region_binder` *)
   | ParentClause of trait_instance_id * trait_decl_id * trait_clause_id
   | UnknownTrait of string
 [@@deriving
@@ -1271,6 +1277,20 @@ type backend_attributes = {
 }
 [@@deriving show]
 
+(** A value of type `T` bound by generic parameters. Used in any context where
+    we're adding generic parameters that aren't on the top-level item, e.g.
+    trait methods.
+ *)
+type 'a binder = {
+  binder_value : 'a;
+  binder_generics : generic_params;
+  binder_preds : predicates;
+  binder_llbc_generics : Types.generic_params;
+  binder_explicit_info : explicit_info;
+      (** Information about which inputs parameters are explicit/implicit *)
+}
+[@@deriving show, ord]
+
 type fun_decl = {
   def_id : FunDeclId.id;
   item_meta : T.item_meta;
diff --git a/src/pure/PureUtils.ml b/src/pure/PureUtils.ml
index 962a23e3..af11fede 100644
--- a/src/pure/PureUtils.ml
+++ b/src/pure/PureUtils.ml
@@ -158,12 +158,16 @@ let ty_substitute (subst : subst) (ty : ty) : ty =
   let obj =
     object
       inherit [_] map_ty
-      method! visit_TVar _ var_id = subst.ty_subst var_id
+
+      method! visit_TVar _ var =
+        subst.ty_subst (Substitute.expect_free_var None var)
 
       method! visit_CgVar _ var =
         subst.cg_subst (Substitute.expect_free_var None var)
 
-      method! visit_Clause _ id = subst.tr_subst id
+      method! visit_Clause _ var =
+        subst.tr_subst (Substitute.expect_free_var None var)
+
       method! visit_Self _ = subst.tr_self
     end
   in
diff --git a/src/symbolic/SymbolicToPure.ml b/src/symbolic/SymbolicToPure.ml
index a4f29e5b..10dda1c3 100644
--- a/src/symbolic/SymbolicToPure.ml
+++ b/src/symbolic/SymbolicToPure.ml
@@ -352,7 +352,7 @@ let bs_ctx_to_fmt_env (ctx : bs_ctx) : Print.fmt_env =
 let bs_ctx_to_pure_fmt_env (ctx : bs_ctx) : PrintPure.fmt_env =
   {
     crate = ctx.decls_ctx.crate;
-    generics = ctx.sg.generics;
+    generics = [ ctx.sg.generics ];
     vars = VarId.Map.empty;
   }
 
@@ -441,7 +441,10 @@ let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) :
 let bs_ctx_lookup_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) : type_decl =
   TypeDeclId.Map.find id ctx.type_ctx.type_decls
 
-(* We simply ignore the bound regions *)
+(* We simply ignore the bound regions. Note that this messes up the de bruijn
+   ids in variables: variables inside `rb.binder_value` are nested deeper so
+   we should shift them before moving them out of their binder. We ignore this
+   because we don't yet handle complex binding situations in Aeneas. *)
 let translate_region_binder (translate_value : 'a -> 'b)
     (rb : 'a T.region_binder) : 'b =
   translate_value rb.binder_value
@@ -476,6 +479,11 @@ and translate_trait_decl_ref (span : Meta.span option)
   in
   { trait_decl_id = tr.trait_decl_id; decl_generics }
 
+and translate_fun_decl_ref (span : Meta.span option) (translate_ty : T.ty -> ty)
+    (fr : T.fun_decl_ref) : fun_decl_ref =
+  let fun_generics = translate_generic_args span translate_ty fr.fun_generics in
+  { fun_id = fr.fun_id; fun_generics }
+
 and translate_global_decl_ref (span : Meta.span option)
     (translate_ty : T.ty -> ty) (gr : T.global_decl_ref) : global_decl_ref =
   let global_generics =
@@ -496,7 +504,9 @@ and translate_trait_instance_id (span : Meta.span option)
   | BuiltinOrAuto _ ->
       (* We should have eliminated those in the prepasses *)
       craise_opt_span __FILE__ __LINE__ span "Unreachable"
-  | Clause var -> Clause (TypesUtils.expect_free_var span var)
+  | Clause var ->
+      Clause var
+      (* Note: the `de_bruijn_id`s are incorrect, see comment on `translate_region_binder` *)
   | ParentClause (inst_id, decl_id, clause_id) ->
       let inst_id = translate_trait_instance_id inst_id in
       ParentClause (inst_id, decl_id, clause_id)
@@ -531,7 +541,9 @@ let rec translate_sty (span : Meta.span option) (ty : T.ty) : ty =
           | T.TArray -> TAdt (TBuiltin TArray, generics)
           | T.TSlice -> TAdt (TBuiltin TSlice, generics)
           | T.TStr -> TAdt (TBuiltin TStr, generics)))
-  | TVar var -> TVar (TypesUtils.expect_free_var span var)
+  | TVar var ->
+      TVar var
+      (* Note: the `de_bruijn_id`s are incorrect, see comment on `translate_region_binder` *)
   | TLiteral ty -> TLiteral ty
   | TNever -> craise_opt_span __FILE__ __LINE__ span "Unreachable"
   | TRef (_, rty, _) -> translate span rty
@@ -766,7 +778,7 @@ let rec translate_fwd_ty (span : Meta.span option) (type_infos : type_infos)
               craise_opt_span __FILE__ __LINE__ span
                 "Unreachable: box/vec/option receives exactly one type \
                  parameter"))
-  | TVar var -> TVar (TypesUtils.expect_free_var span var)
+  | TVar var -> TVar var
   | TNever -> craise_opt_span __FILE__ __LINE__ span "Unreachable"
   | TLiteral lty -> TLiteral lty
   | TRef (_, rty, _) -> translate rty
@@ -874,7 +886,7 @@ let rec translate_back_ty (span : Meta.span option) (type_infos : type_infos)
                 (* Note that if there is exactly one type, [mk_simpl_tuple_ty]
                  * is the identity *)
                 Some (mk_simpl_tuple_ty tys_t)))
-  | TVar var -> wrap (TVar (TypesUtils.expect_free_var span var))
+  | TVar var -> wrap (TVar var)
   | TNever -> craise_opt_span __FILE__ __LINE__ span "Unreachable"
   | TLiteral lty -> wrap (TLiteral lty)
   | TRef (r, rty, rkind) -> (
@@ -4287,7 +4299,9 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
        call to the loop forward function) *)
     let generics =
       let { types; const_generics; trait_clauses } = ctx.sg.generics in
-      let types = List.map (fun (ty : T.type_var) -> TVar ty.T.index) types in
+      let types =
+        List.map (fun (ty : T.type_var) -> TVar (Free ty.T.index)) types
+      in
       let const_generics =
         List.map
           (fun (cg : T.const_generic_var) -> T.CgVar (Free cg.T.index))
@@ -4299,7 +4313,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
             let trait_decl_ref =
               { trait_decl_id = c.trait_id; decl_generics = c.generics }
             in
-            { trait_id = Clause c.clause_id; trait_decl_ref })
+            { trait_id = Clause (Free c.clause_id); trait_decl_ref })
           trait_clauses
       in
       { types; const_generics; trait_refs }
@@ -4687,6 +4701,22 @@ let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list =
         None)
     (TypeDeclId.Map.values ctx.type_ctx.type_decls)
 
+let translate_trait_method (span : span option) (translate_ty : T.ty -> ty)
+    (bound_fn : T.fun_decl_ref T.binder) : fun_decl_ref binder =
+  let binder_llbc_generics = bound_fn.T.binder_params in
+  let binder_generics, binder_preds =
+    translate_generic_params span binder_llbc_generics
+  in
+  let binder_explicit_info = compute_explicit_info binder_generics [] in
+  {
+    binder_value =
+      translate_fun_decl_ref span translate_ty bound_fn.T.binder_value;
+    binder_generics;
+    binder_preds;
+    binder_explicit_info;
+    binder_llbc_generics;
+  }
+
 let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     : trait_decl =
   let {
@@ -4701,26 +4731,31 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
   } : A.trait_decl =
     trait_decl
   in
+  let span = Some item_meta.span in
   let type_infos = ctx.type_ctx.type_infos in
+  let translate_ty = translate_fwd_ty span type_infos in
   let name =
     Print.Types.name_to_string
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
       item_meta.name
   in
-  let generics, preds =
-    translate_generic_params (Some trait_decl.item_meta.span) llbc_generics
-  in
+  let generics, preds = translate_generic_params span llbc_generics in
   let explicit_info = compute_explicit_info generics [] in
   let parent_clauses =
+    List.map (translate_trait_clause span) llbc_parent_clauses
+  in
+  let consts = List.map (fun (name, ty) -> (name, translate_ty ty)) consts in
+  let required_methods =
     List.map
-      (translate_trait_clause (Some trait_decl.item_meta.span))
-      llbc_parent_clauses
+      (fun (name, bound_fn) ->
+        (name, translate_trait_method span translate_ty bound_fn))
+      required_methods
   in
-  let consts =
+  let provided_methods =
     List.map
-      (fun (name, ty) ->
-        (name, translate_fwd_ty (Some trait_decl.item_meta.span) type_infos ty))
-      consts
+      (fun (name, bound_fn) ->
+        (name, translate_trait_method span translate_ty bound_fn))
+      provided_methods
   in
   {
     def_id;
@@ -4753,36 +4788,40 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
   } =
     trait_impl
   in
-  let span = item_meta.span in
+  let span = Some item_meta.span in
   let type_infos = ctx.type_ctx.type_infos in
+  let translate_ty = translate_fwd_ty span type_infos in
   let impl_trait =
-    (translate_trait_decl_ref (Some span)
-       (translate_fwd_ty (Some span) type_infos))
-      llbc_impl_trait
+    (translate_trait_decl_ref span translate_ty) llbc_impl_trait
   in
   let name =
     Print.Types.name_to_string
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
       item_meta.name
   in
-  let generics, preds = translate_generic_params (Some span) llbc_generics in
+  let generics, preds = translate_generic_params span llbc_generics in
   let explicit_info = compute_explicit_info generics [] in
   let parent_trait_refs =
-    List.map (translate_strait_ref (Some span)) parent_trait_refs
+    List.map (translate_strait_ref span) parent_trait_refs
   in
   let consts =
     List.map
       (fun (name, gref) ->
-        ( name,
-          translate_global_decl_ref (Some span)
-            (translate_fwd_ty (Some span) type_infos)
-            gref ))
+        (name, translate_global_decl_ref span translate_ty gref))
       consts
   in
-  let types =
+  let types = List.map (fun (name, ty) -> (name, translate_ty ty)) types in
+  let required_methods =
+    List.map
+      (fun (name, bound_fn) ->
+        (name, translate_trait_method span translate_ty bound_fn))
+      required_methods
+  in
+  let provided_methods =
     List.map
-      (fun (name, ty) -> (name, translate_fwd_ty (Some span) type_infos ty))
-      types
+      (fun (name, bound_fn) ->
+        (name, translate_trait_method span translate_ty bound_fn))
+      provided_methods
   in
   {
     def_id;