diff --git a/Makefile b/Makefile
index 1647a519..4691c98f 100644
--- a/Makefile
+++ b/Makefile
@@ -57,7 +57,7 @@ clean-and-test:
 .PRECIOUS: %.llbc
 %.llbc: %.rs .charon_version
 	# --mir elaborated --add-drop-bounds 
-	$(CHARON) rustc --preset=eurydice --dest-file "$@" $(CHARON_EXTRA) -- $<
+	$(CHARON) rustc --monomorphize --preset=eurydice --dest-file "$@" $(CHARON_EXTRA) -- $<
 
 out/test-%/main.c: test/main.c
 	mkdir -p out/test-$*
@@ -73,7 +73,7 @@ test/issue_105.llbc: CHARON_EXTRA = \
   --include=core::cmp::* \
   --include=core::convert::*
 
-test/array2d.llbc: CHARON_EXTRA = --include=core::array::equality::*
+# test/array2d.llbc: CHARON_EXTRA = --include=core::array::equality::*
 
 test/core_num.llbc: CHARON_EXTRA = \
   --include=core::num::*::BITS \
@@ -83,6 +83,9 @@ test/println.llbc: CHARON_EXTRA = \
   --include=core::fmt::Arguments --include=core::fmt::rt::*::new_const \
   --include=core::fmt::rt::Argument
 
+# test-where_clauses_closures: CHARON_EXTRA = \
+# 	--include=core::convert::*
+
 test/option.llbc: CHARON_EXTRA = \
   --include=core::option::*
 
diff --git a/bin/main.ml b/bin/main.ml
index fb48d4a0..f7381687 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -235,8 +235,9 @@ Supported options:|}
   (* Must happen now, before Monomorphization.datatypes, because otherwise
      MonomorphizationState.state gets filled with lids that later on get eliminated on the basis
      that they were empty structs to begin with, which would send Checker off the rails *)
-  let files = Krml.DataTypes.remove_empty_structs files in
+  let files = Eurydice.Cleanup2.remove_empty_structs files in
   let files = Krml.Monomorphization.datatypes files in
+  let files = Eurydice.Cleanup2.drop_unused_type files in
   (* Cannot use remove_unit_buffers as it is technically incorrect *)
   let files = Krml.DataTypes.remove_unit_fields#visit_files () files in
   Eurydice.Logging.log "Phase2.13" "%a" pfiles files;
@@ -264,7 +265,7 @@ Supported options:|}
   let errors, files = Krml.Checker.check_everything ~warn:true files in
   if errors then
     fail __FILE__ __LINE__;
-  let files = Krml.Inlining.drop_unused files in
+  (*let files = Krml.Inlining.drop_unused files in*)
   let files = Eurydice.Cleanup2.remove_array_temporaries#visit_files () files in
   Eurydice.Logging.log "Phase2.25" "%a" pfiles files;
   let files = Eurydice.Cleanup2.remove_array_repeats#visit_files false files in
@@ -289,7 +290,7 @@ Supported options:|}
   let files = Eurydice.Cleanup2.remove_array_from_fn files in
   Eurydice.Logging.log "Phase2.6" "%a" pfiles files;
   (* remove_array_from_fn, above, creates further opportunities for removing unused functions. *)
-  let files = Krml.Inlining.drop_unused files in
+  (* let files = Krml.Inlining.drop_unused files in *)
   let files = Eurydice.Cleanup2.remove_implicit_array_copies#visit_files () files in
   (* Creates opportunities for removing unused variables *)
   let files = Eurydice.Cleanup2.remove_assign_return#visit_files () files in
@@ -312,6 +313,8 @@ Supported options:|}
   let files = Eurydice.Cleanup2.float_comments files in
   Eurydice.Logging.log "Phase2.95" "%a" pfiles files;
   let files = Eurydice.Cleanup2.bonus_cleanups#visit_files [] files in
+  let files = Krml.Inlining.drop_unused files in
+  let files = Eurydice.Cleanup2.drop_unused_monoed_func files in
   (* Macros stemming from globals -- FIXME why is this not Krml.AstToCStar.mk_macros_set? *)
   let files, macros = Eurydice.Cleanup2.build_macros files in
 
diff --git a/cremepat/cremepat.ml b/cremepat/cremepat.ml
index 8294587c..3a802828 100644
--- a/cremepat/cremepat.ml
+++ b/cremepat/cremepat.ml
@@ -157,13 +157,16 @@ let compile_parse_tree (env : env) loc
         (* EApp (ETApp (e, ts), es) *)
         ppat_cons_many ~loc "EApp"
           [
-            ppat_cons_many ~loc "ETApp"
-              [
-                compile env head;
-                compile_expr_list_pattern env cgs;
-                compile_expr_list_pattern env methods;
-                compile_typ_list_pattern env ts;
-              ];
+            (if cgs = [] && methods = [] && ts = [] then
+               compile env head
+             else
+               ppat_cons_many ~loc "ETApp"
+                 [
+                   compile env head;
+                   compile_expr_list_pattern env cgs;
+                   compile_expr_list_pattern env methods;
+                   compile_typ_list_pattern env ts;
+                 ]);
             ppat_list ~loc (List.map (compile env) args);
           ]
     | Addr e -> ppat_cons_one ~loc "EAddrOf" (compile env e)
diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h
index b9126ba2..9397e564 100644
--- a/include/eurydice_glue.h
+++ b/include/eurydice_glue.h
@@ -132,6 +132,9 @@ typedef struct {
                  end) /* x is already at an array type, no need for cast */
 #define Eurydice_array_to_subslice(_arraylen, x, r, t, _0, _1)                 \
   EURYDICE_SLICE((t *)x, r.start, r.end)
+// The mono version is exactly the same, just with a different name
+#define Eurydice_array_to_subslice_mono(_arraylen, x, r, t, _0, _1)            \
+  EURYDICE_SLICE((t *)x, r.start, r.end)
 
 // Same as above, variant for when start and end are statically known
 #define Eurydice_array_to_subslice3(x, start, end, t_ptr)                      \
@@ -146,6 +149,11 @@ typedef struct {
   EURYDICE_SLICE((t *)x, 0, r)
 #define Eurydice_array_to_subslice_from(size, x, r, t, _range_t, _0)           \
   EURYDICE_SLICE((t *)x, r, size)
+// The mono versions are exactly the same, just different names
+#define Eurydice_array_to_subslice_to_mono(_size, x, r, t, _range_t, _0)       \
+  EURYDICE_SLICE((t *)x, 0, r)
+#define Eurydice_array_to_subslice_from_mono(size, x, r, t, _range_t, _0)      \
+  EURYDICE_SLICE((t *)x, r, size)
 
 // Copy a slice with memcopy
 #define Eurydice_slice_copy(dst, src, t)                                       \
@@ -329,6 +337,17 @@ core_convert_num__core__convert__From_u16__for_usize__from(uint16_t x) {
   return x;
 }
 
+// for monoed where-clauses_simple
+static inline uint64_t
+core_convert_num__core__convert__From___u64__u16___from(uint16_t x) {
+  return x;
+}
+
+static inline size_t
+core_convert_num__core__convert__From___usize__u16___from(uint16_t x) {
+  return x;
+}
+
 static inline uint32_t core_num__u8__count_ones(uint8_t x0) {
 #ifdef _MSC_VER
   return __popcnt(x0);
@@ -549,6 +568,7 @@ typedef const char *Prims_string;
 // This is temporary. Ultimately we want to be able to extract all of this.
 
 typedef void *core_fmt_Formatter;
+typedef void *core_fmt_Formatter_____;
 #define core_fmt_rt__core__fmt__rt__Argument__a___new_display(x1, x2, x3, x4)  \
   NULL
 
diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml
index 6dcd66ff..6a02a65e 100644
--- a/lib/AstOfLlbc.ml
+++ b/lib/AstOfLlbc.ml
@@ -193,6 +193,7 @@ module RustNames = struct
       map_vars_to_vars = false;
       match_with_trait_decl_refs = true;
       (* use_trait_decl_refs = true; *)
+      (* match_mono = true; *)
     }
 
   let vec = parse_pattern "alloc::vec::Vec<@>"
@@ -205,14 +206,23 @@ module RustNames = struct
     parse_pattern "SliceIndexShared<'_, @T>", Builtin.slice_index;
     parse_pattern "SliceIndexMut<'_, @T>", Builtin.slice_index;
 
+    (* slices: generics *)
     parse_pattern "core::slice::index::{core::ops::index::Index<[@T], @I, @Clause2_Output>}::index<'_, @, core::ops::range::Range<usize>, [@]>", Builtin.slice_subslice;
     parse_pattern "core::slice::index::{core::ops::index::IndexMut<[@T], @I, @Clause2_Output>}::index_mut<'_, @, core::ops::range::Range<usize>, [@]>", Builtin.slice_subslice;
     parse_pattern "core::slice::index::{core::ops::index::Index<[@T], @I, @Clause2_Output>}::index<'_, @, core::ops::range::RangeTo<usize>, [@]>", Builtin.slice_subslice_to;
     parse_pattern "core::slice::index::{core::ops::index::IndexMut<[@T], @I, @Clause2_Output>}::index_mut<'_, @, core::ops::range::RangeTo<usize>, [@]>", Builtin.slice_subslice_to;
     parse_pattern "core::slice::index::{core::ops::index::Index<[@T], @I, @Clause2_Output>}::index<'_, @, core::ops::range::RangeFrom<usize>, [@]>", Builtin.slice_subslice_from;
     parse_pattern "core::slice::index::{core::ops::index::IndexMut<[@T], @I, @Clause2_Output>}::index_mut<'_, @, core::ops::range::RangeFrom<usize>, [@]>", Builtin.slice_subslice_from;
-
-    (* arrays *)
+    
+    (* slices: mono *)
+    parse_pattern "core::slice::index::{core::ops::index::Index<[@T], @I>}::index<'_, @, core::ops::range::Range<usize>, [@]>", Builtin.slice_subslice;
+    parse_pattern "core::slice::index::{core::ops::index::IndexMut<[@T], @I>}::index_mut<'_, @, core::ops::range::Range<usize>, [@]>", Builtin.slice_subslice;
+    parse_pattern "core::slice::index::{core::ops::index::Index<[@T], @I>}::index<'_, @, core::ops::range::RangeTo<usize>, [@]>", Builtin.slice_subslice_to;
+    parse_pattern "core::slice::index::{core::ops::index::IndexMut<[@T], @I>}::index_mut<'_, @, core::ops::range::RangeTo<usize>, [@]>", Builtin.slice_subslice_to;
+    parse_pattern "core::slice::index::{core::ops::index::Index<[@T], @I>}::index<'_, @, core::ops::range::RangeFrom<usize>, [@]>", Builtin.slice_subslice_from;
+    parse_pattern "core::slice::index::{core::ops::index::IndexMut<[@T], @I>}::index_mut<'_, @, core::ops::range::RangeFrom<usize>, [@]>", Builtin.slice_subslice_from;
+
+    (* arrays: generics *)
     parse_pattern "core::array::{core::ops::index::Index<[@T; @N], @I, @Clause2_Clause0_Output>}::index<'_, @, core::ops::range::Range<usize>, [@], @>", Builtin.array_to_subslice;
     parse_pattern "core::array::{core::ops::index::IndexMut<[@T; @N], @I, @Clause2_Clause0_Output>}::index_mut<'_, @, core::ops::range::Range<usize>, [@], @>", Builtin.array_to_subslice;
     parse_pattern "core::array::{core::ops::index::Index<[@T; @N], @I, @Clause2_Clause0_Output>}::index<'_, @, core::ops::range::RangeTo<usize>, [@], @>", Builtin.array_to_subslice_to;
@@ -220,13 +230,28 @@ module RustNames = struct
     parse_pattern "core::array::{core::ops::index::Index<[@T; @N], @I, @Clause2_Clause0_Output>}::index<'_, @, core::ops::range::RangeFrom<usize>, [@], @>", Builtin.array_to_subslice_from;
     parse_pattern "core::array::{core::ops::index::IndexMut<[@T; @N], @I, @Clause2_Clause0_Output>}::index_mut<'_, @, core::ops::range::RangeFrom<usize>, [@], @>", Builtin.array_to_subslice_from;
 
+    (* arrays: mono *)
+    parse_pattern "core::array::{core::ops::index::Index<[@T; @N], @I>}::index<'_, @, core::ops::range::Range<usize>, @>", Builtin.array_to_subslice_mono;
+    parse_pattern "core::array::{core::ops::index::IndexMut<[@T; @N], @I>}::index_mut<'_, @, core::ops::range::Range<usize>, @>", Builtin.array_to_subslice_mono;
+    parse_pattern "core::array::{core::ops::index::Index<[@T; @N], @I>}::index<'_, @, core::ops::range::RangeTo<usize>, @>", Builtin.array_to_subslice_to_mono;
+    parse_pattern "core::array::{core::ops::index::IndexMut<[@T; @N], @I>}::index_mut<'_, @, core::ops::range::RangeTo<usize>, @>", Builtin.array_to_subslice_to_mono;
+    parse_pattern "core::array::{core::ops::index::Index<[@T; @N], @I>}::index<'_, @, core::ops::range::RangeFrom<usize>, @>", Builtin.array_to_subslice_from_mono;
+    parse_pattern "core::array::{core::ops::index::IndexMut<[@T; @N], @I>}::index_mut<'_, @, core::ops::range::RangeFrom<usize>, @>", Builtin.array_to_subslice_from_mono;
+
     (* slices <-> arrays *)
     parse_pattern "ArrayToSliceShared<'_, @T, @N>", Builtin.array_to_slice;
     parse_pattern "ArrayToSliceMut<'_, @T, @N>", Builtin.array_to_slice;
+
+    (* slices <-> arrays: generics *)
     parse_pattern "core::convert::{core::convert::TryInto<@T, @U, @Clause2_Error>}::try_into<&'_ [@T], [@T; @], core::array::TryFromSliceError>", Builtin.slice_to_array;
     parse_pattern "core::convert::{core::convert::TryInto<@T, @U, @Clause2_Error>}::try_into<&'_ [@T], &'_ [@T; @], core::array::TryFromSliceError>", Builtin.slice_to_ref_array;
     parse_pattern "core::convert::{core::convert::TryInto<@T, @U, @Clause2_Error>}::try_into<&'_ mut [@T], &'_ mut [@T; @], core::array::TryFromSliceError>", Builtin.slice_to_ref_array;
 
+    (* slices <-> arrays: mono *)
+    parse_pattern "core::convert::{core::convert::TryInto<@T, @U>}::try_into<&'_ [@T], [@T; @], core::array::TryFromSliceError>", Builtin.slice_to_array;
+    parse_pattern "core::convert::{core::convert::TryInto<@T, @U>}::try_into<&'_ [@T], &'_ [@T; @], core::array::TryFromSliceError>", Builtin.slice_to_ref_array;
+    parse_pattern "core::convert::{core::convert::TryInto<@T, @U>}::try_into<&'_ mut [@T], &'_ mut [@T; @], core::array::TryFromSliceError>", Builtin.slice_to_ref_array;
+
     (* iterators XXX are any of these used? *)
     parse_pattern "core::iter::traits::collect::IntoIterator<[@; @]>::into_iter", Builtin.array_into_iter;
 
@@ -281,10 +306,6 @@ let string_of_fn_ptr env fn_ptr = string_of_pattern (pattern_of_fn_ptr env fn_pt
 
 (** Translation of types *)
 
-let lid_of_name (env : env) (name : Charon.Types.name) : K.lident =
-  let prefix, name = Krml.KList.split_at_last name in
-  List.map (string_of_path_elem env) prefix, string_of_path_elem env name
-
 let width_of_integer_type (t : Charon.Types.integer_type) : K.width =
   match t with
   | Signed Isize -> PtrdiffT
@@ -302,10 +323,6 @@ let width_of_integer_type (t : Charon.Types.integer_type) : K.width =
   | Unsigned U128 ->
       failwith "Internal error: `u128` should not be handled in `width_of_integer_type`."
 
-let lid_of_type_decl_id (env : env) (id : C.type_decl_id) =
-  let { C.item_meta; _ } = env.get_nth_type id in
-  lid_of_name env item_meta.name
-
 let constant_of_scalar_value sv =
   let w = width_of_integer_type (Charon.Scalars.get_ty sv) in
   w, Z.to_string (Charon.Scalars.get_val sv)
@@ -385,9 +402,210 @@ let lookup_field env typ_id field_id =
   let field = List.nth fields i in
   ensure_named i field.field_name
 
+let is_var v2 v1 =
+  match v2 with
+  | Var (v2, _) -> v2 = v1
+  | _ -> false
+
+let assert_var = function
+  | Var (v2, ty) -> v2, ty
+  | _ -> assert false
+
+let assert_trait_clause_method = function
+  | TraitClauseMethod { clause_id; item_name; ts; _ } -> clause_id, item_name, ts
+  | _ -> assert false
+
+(* Regular binders *)
+
+let lookup_with_original_type env v1 =
+  let i, (v, t) = findi (fun (v2, _) -> is_var v2 v1) env.binders in
+  let _, ty = assert_var v in
+  i, t, ty
+
+let lookup env v1 =
+  let i, (_, t) = findi (fun (v2, _) -> is_var v2 v1) env.binders in
+  i, t
+
+let lookup_cg_in_expressions (env : env) (v1 : C.const_generic_var_id) =
+  let i, (_, t) = findi (fun (v2, _) -> v2 = ConstGenericVar v1) env.binders in
+  i, t
+
+let expression_of_cg_var_id env v =
+  let i, t = lookup_cg_in_expressions env v in
+  K.(with_type t (EBound i))
+
+let expression_of_var_id (env : env) (v : C.local_id) : K.expr =
+  let i, t = lookup env v in
+  K.(with_type t (EBound i))
+
+(** Assume here the maximum length is 128-bit -- will throw away the larger if larger. This is a
+    helper function to split a 128-bit integer into two 64-bit integers and is not assumed to be
+    used in other contexts. Returns the **expr** pair (high64bits, low64bits) *)
+let split_128bit (value : Z.t) =
+  let mask128 = Z.sub (Z.shift_left Z.one 128) Z.one in
+  let mask64 = Z.sub (Z.shift_left Z.one 64) Z.one in
+  (* Always truncate to 128 bits using bitwise AND *)
+  let value = Z.logand value mask128 in
+  (* Extract low 64 bits *)
+  let low64 = Z.logand mask64 value in
+  (* Shift right without sign extension (use logical shift) *)
+  let high64 = Z.shift_right value 64 in
+  let to_expr_u64bits v =
+    let print_Z z = Z.format "%#x" z in
+    K.with_type (K.TInt UInt64) @@ K.EConstant (UInt64, print_Z v)
+  in
+  to_expr_u64bits high64, to_expr_u64bits low64
+
+let expression_of_int128_t (value : Z.t) =
+  let i128_max = Z.sub (Z.shift_left Z.one 127) Z.one in
+  if value > i128_max then
+    failwith "value is larger than the maximum value of i128";
+  let i128_min = Z.neg (Z.shift_left Z.one 127) in
+  if value < i128_min then
+    failwith "value is smaller than the minimum value of i128";
+  let high64, low64 = split_128bit value in
+  K.(with_type Builtin.int128_t (EApp (Builtin.(get_128_op ("i", "from_bits")), [ high64; low64 ])))
+
+let expression_of_uint128_t (value : Z.t) =
+  let u128_max = Z.sub (Z.shift_left Z.one 128) Z.one in
+  if value > u128_max then
+    failwith "value is larger than the maximum value of u128";
+  let high64, low64 = split_128bit value in
+  K.(
+    with_type Builtin.uint128_t (EApp (Builtin.(get_128_op ("u", "from_bits")), [ high64; low64 ])))
+
+let expression_of_scalar_value sv : K.expr =
+  let int_ty = Charon.Scalars.get_ty sv in
+  let value = Charon.Scalars.get_val sv in
+  match int_ty with
+  | C.Signed C.I128 -> expression_of_int128_t value
+  | C.Unsigned C.U128 -> expression_of_uint128_t value
+  | _ ->
+      let w = width_of_integer_type int_ty in
+      K.(with_type (TInt w) (EConstant (constant_of_scalar_value sv)))
+
+let expression_of_literal (_env : env) (l : C.literal) : K.expr =
+  match l with
+  | VScalar sv -> expression_of_scalar_value sv
+  | VBool b -> K.(with_type TBool (EBool b))
+  | VStr s ->
+      let ascii = Utf8.ascii_of_utf8_str s in
+      let len = String.length s in
+      K.(
+        with_type Builtin.str_t
+          (EFlat
+             [
+               Some "data", with_type Krml.Checker.c_string (EString ascii);
+               Some "len", with_type Krml.Helpers.usize (EConstant (SizeT, string_of_int len));
+             ]))
+  | VChar c -> K.(with_type Builtin.char_t (EConstant (UInt32, string_of_int @@ Uchar.to_int c)))
+  | VByteStr lst ->
+      let str = List.map (Printf.sprintf "%#x") lst |> String.concat "" in
+      K.(with_type Krml.Checker.c_string (EString str))
+  | VFloat { C.float_ty; float_value } ->
+      let w = float_width float_ty in
+      K.(with_type (TInt w) (EConstant (w, float_value)))
+
+let expression_of_const_generic env cg =
+  match cg with
+  | C.CgGlobal _ -> failwith "TODO: CgGLobal"
+  | C.CgVar var -> expression_of_cg_var_id env (C.expect_free_var var)
+  | C.CgValue l -> expression_of_literal env l
+
+(* name::<A, B, C, N> -> (name, [N], [A, B, C]) *)
+let lid_full_generic = Hashtbl.create 41
+
+(* Given the result type, const generics, and type arguments, return the original type such that
+   After applying the const generics and type arguments, we get the result type.
+*)
+let ty_re_polymorphize res_ty cgs ty_args =
+  let n_cgs = List.length cgs in
+  let n = List.length ty_args in
+  if n = 0 && n_cgs = 0 then
+    res_ty
+  else
+    match res_ty with
+    | K.TPoly (ts, t) ->
+        (* If already polymorphic, conservatively widen the scheme by
+           prepending new binders. This is a best–effort reconstruction. *)
+        K.TPoly ({ K.n = ts.n + n; n_cgs = ts.n_cgs + n_cgs }, t)
+    | _ -> K.TPoly ({ K.n; n_cgs }, res_ty)
+
+(* From monomorphized codes `name::<A, B, C>` to the original generic expression.
+   Work by turning the `EQualified` into `ETApp` with the appropriate type
+   Or, if no generics, leave as is.
+*)
+let re_polymorphize expr =
+  (object
+     inherit [_] Krml.Ast.map
+
+     method! visit_EQualified ((), ty) full_name =
+       try
+         let name, cgs, ts, fn_ptrs = Hashtbl.find lid_full_generic full_name in
+         if cgs = [] && ts = [] then
+           EQualified full_name
+         else
+           ETApp (K.with_type (ty_re_polymorphize ty cgs ts) (K.EQualified name), cgs, fn_ptrs, ts)
+       with Not_found -> EQualified full_name
+  end)
+    #visit_expr_w
+    () expr
+
+(* get the charon name without the last PeMonomorphized, used for match blocklist *)
+let pure_c_name (name : C.name) =
+  let pre, last = Krml.KList.split_at_last name in
+  match last with
+  | PeInstantiated _args -> pre
+  | _ -> name
+
+(* get the trait_refs from mono. charon name, used in lookup_fun *)
+let trait_refs_c_name (name : C.name) : C.trait_ref list =
+  let _pre, last = Krml.KList.split_at_last name in
+  match last with
+  | PeInstantiated args -> args.binder_value.trait_refs
+  | _ -> []
+
+let pure_lid_of_name (env : env) (name : Charon.Types.name) : K.lident =
+  let prefix, name = Krml.KList.split_at_last name in
+  List.map (string_of_path_elem env) prefix, string_of_path_elem env name
+
+let update_lid_full_generic_fnptrs (full_name : K.lident) (fn_ptrs : K.expr list) =
+  L.log "AstOfLlbc" "[re-poly] trying to update the fn_ptrs of %a to %a" plid full_name pexprs
+    fn_ptrs;
+  try
+    let name, cgs, ts, _ = Hashtbl.find lid_full_generic full_name in
+    L.log "AstOfLlbc" "[re-poly] updated the fn_ptrs of %a to %a" plid full_name pexprs fn_ptrs;
+    Hashtbl.replace lid_full_generic full_name (name, cgs, ts, fn_ptrs)
+  with Not_found -> failwith "update_lid_full_generic_fnptrs: not found"
+
 let expression_of_struct_Arr (expr_array : K.expr) = K.EFlat [ Some "data", expr_array ]
 
-let rec pre_typ_of_ty (env : env) (ty : Charon.Types.ty) : K.typ =
+let rec insert_lid_full_generic (env : env) (full_name : K.lident) (name : Charon.Types.name) =
+  let item_name, generic =
+    let pre, last = Krml.KList.split_at_last name in
+    match last with
+    | PeInstantiated args -> pure_lid_of_name env pre, (args.binder_value : C.generic_args)
+    | _ -> full_name, { C.types = []; regions = []; const_generics = []; trait_refs = [] }
+  in
+  let cgs, tys =
+    ( List.map (expression_of_const_generic env) generic.const_generics,
+      List.map (typ_of_ty env) generic.types )
+  in
+  if not (Hashtbl.mem lid_full_generic full_name) then
+    L.log "AstOfLlbc" "mono name : %a\n repolyed name : %a with cgs %a and tys %a " plid full_name
+      plid item_name pexprs cgs ptyps tys;
+  Hashtbl.add lid_full_generic full_name (item_name, cgs, tys, [])
+
+and lid_of_name (env : env) (name : Charon.Types.name) : K.lident =
+  let lid = pure_lid_of_name env name in
+  insert_lid_full_generic env lid name;
+  lid
+
+and lid_of_type_decl_id (env : env) (id : C.type_decl_id) =
+  let { C.item_meta; _ } = env.get_nth_type id in
+  lid_of_name env item_meta.name
+
+and pre_typ_of_ty (env : env) (ty : Charon.Types.ty) : K.typ =
   match ty with
   | TVar var -> K.TBound (lookup_typ env (C.expect_free_var var))
   | TLiteral t -> typ_of_literal_ty env t
@@ -495,30 +713,6 @@ let maybe_cg_array (env : env) (t : C.ty) (cg : C.const_generic) =
 
 (* Environment: expressions *)
 
-let is_var v2 v1 =
-  match v2 with
-  | Var (v2, _) -> v2 = v1
-  | _ -> false
-
-let assert_var = function
-  | Var (v2, ty) -> v2, ty
-  | _ -> assert false
-
-let assert_trait_clause_method = function
-  | TraitClauseMethod { clause_id; item_name; ts; _ } -> clause_id, item_name, ts
-  | _ -> assert false
-
-(* Regular binders *)
-
-let lookup env v1 =
-  let i, (_, t) = findi (fun (v2, _) -> is_var v2 v1) env.binders in
-  i, t
-
-let lookup_with_original_type env v1 =
-  let i, (v, t) = findi (fun (v2, _) -> is_var v2 v1) env.binders in
-  let _, ty = assert_var v in
-  i, t, ty
-
 (* Const generic binders *)
 
 let push_cg_binder env (t : C.const_generic_param) =
@@ -596,92 +790,6 @@ let rec with_locals (env : env) (t : K.typ) (locals : C.local list) (k : env ->
       let b = binder_of_var env l in
       K.(with_type t (ELet (b, Krml.Helpers.any, with_locals env t locals k)))
 
-let lookup_cg_in_expressions (env : env) (v1 : C.const_generic_var_id) =
-  let i, (_, t) = findi (fun (v2, _) -> v2 = ConstGenericVar v1) env.binders in
-  i, t
-
-let expression_of_cg_var_id env v =
-  let i, t = lookup_cg_in_expressions env v in
-  K.(with_type t (EBound i))
-
-let expression_of_var_id (env : env) (v : C.local_id) : K.expr =
-  let i, t = lookup env v in
-  K.(with_type t (EBound i))
-
-(** Assume here the maximum length is 128-bit -- will throw away the larger if larger. This is a
-    helper function to split a 128-bit integer into two 64-bit integers and is not assumed to be
-    used in other contexts. Returns the **expr** pair (high64bits, low64bits) *)
-let split_128bit (value : Z.t) =
-  let mask128 = Z.sub (Z.shift_left Z.one 128) Z.one in
-  let mask64 = Z.sub (Z.shift_left Z.one 64) Z.one in
-  (* Always truncate to 128 bits using bitwise AND *)
-  let value = Z.logand value mask128 in
-  (* Extract low 64 bits *)
-  let low64 = Z.logand mask64 value in
-  (* Shift right without sign extension (use logical shift) *)
-  let high64 = Z.shift_right value 64 in
-  let to_expr_u64bits v =
-    let print_Z z = Z.format "%#x" z in
-    K.with_type (K.TInt UInt64) @@ K.EConstant (UInt64, print_Z v)
-  in
-  to_expr_u64bits high64, to_expr_u64bits low64
-
-let expression_of_int128_t (value : Z.t) =
-  let i128_max = Z.sub (Z.shift_left Z.one 127) Z.one in
-  if value > i128_max then
-    failwith "value is larger than the maximum value of i128";
-  let i128_min = Z.neg (Z.shift_left Z.one 127) in
-  if value < i128_min then
-    failwith "value is smaller than the minimum value of i128";
-  let high64, low64 = split_128bit value in
-  K.(with_type Builtin.int128_t (EApp (Builtin.(get_128_op ("i", "from_bits")), [ high64; low64 ])))
-
-let expression_of_uint128_t (value : Z.t) =
-  let u128_max = Z.sub (Z.shift_left Z.one 128) Z.one in
-  if value > u128_max then
-    failwith "value is larger than the maximum value of u128";
-  let high64, low64 = split_128bit value in
-  K.(
-    with_type Builtin.uint128_t (EApp (Builtin.(get_128_op ("u", "from_bits")), [ high64; low64 ])))
-
-let expression_of_scalar_value sv : K.expr =
-  let int_ty = Charon.Scalars.get_ty sv in
-  let value = Charon.Scalars.get_val sv in
-  match int_ty with
-  | C.Signed C.I128 -> expression_of_int128_t value
-  | C.Unsigned C.U128 -> expression_of_uint128_t value
-  | _ ->
-      let w = width_of_integer_type int_ty in
-      K.(with_type (TInt w) (EConstant (constant_of_scalar_value sv)))
-
-let expression_of_literal (_env : env) (l : C.literal) : K.expr =
-  match l with
-  | VScalar sv -> expression_of_scalar_value sv
-  | VBool b -> K.(with_type TBool (EBool b))
-  | VStr s ->
-      let ascii = Utf8.ascii_of_utf8_str s in
-      let len = String.length s in
-      K.(
-        with_type Builtin.str_t
-          (EFlat
-             [
-               Some "data", with_type Krml.Checker.c_string (EString ascii);
-               Some "len", with_type Krml.Helpers.usize (EConstant (SizeT, string_of_int len));
-             ]))
-  | VChar c -> K.(with_type Builtin.char_t (EConstant (UInt32, string_of_int @@ Uchar.to_int c)))
-  | VByteStr lst ->
-      let str = List.map (Printf.sprintf "%#x") lst |> String.concat "" in
-      K.(with_type Krml.Checker.c_string (EString str))
-  | VFloat { C.float_ty; float_value } ->
-      let w = float_width float_ty in
-      K.(with_type (TInt w) (EConstant (w, float_value)))
-
-let expression_of_const_generic env cg =
-  match cg with
-  | C.CgGlobal _ -> failwith "TODO: CgGLobal"
-  | C.CgVar var -> expression_of_cg_var_id env (C.expect_free_var var)
-  | C.CgValue l -> expression_of_literal env l
-
 let rec expression_of_place (env : env) (p : C.place) : K.expr =
   (* We construct a target expression. Callers may still use the original type to tell arrays
      and references apart, since their *uses* (e.g. addr-of) compile in a type-directed way based on
@@ -1255,13 +1363,44 @@ and debug_trait_clause_mapping env (mapping : (var_id * K.typ) list) =
 
 (** Compiling function instantiations into krml application nodes. *)
 
+(* Helper for getting monomorphized generic arguments from a name *)
+let try_get_mono_from_name (name : C.name) =
+  match List.rev name with
+  | PeInstantiated generics :: _ -> Some generics
+  | _ -> None
+
+(* Only get monomorphized generics for known *Eurydice* builtins *)
+let try_get_mono_generics is_known_builtin (env : env) (f : C.fn_ptr) =
+  if not is_known_builtin then
+    None
+  else
+    let get_from_fid fid =
+      let fun_decl = env.get_nth_function fid in
+      try_get_mono_from_name fun_decl.item_meta.name
+    in
+    match f.kind with
+    | FunId (FRegular fid) -> get_from_fid fid
+    (* Builtins are always generic *)
+    | FunId (FBuiltin _) -> None
+    | TraitMethod (_, _, fid) -> get_from_fid fid
+
 (* First step: produce an expression for the un-instantiated function reference, along with all the
    type information required to build a proper instantiation. The function reference is an expression
    that is either a reference to a variable in scope (trait methods), or to a top-level qualified
    name, which encompasses both externally-defined function (builtins), or regular functions. *)
-let lookup_fun (env : env) depth (f : C.fn_ptr) : K.expr' * lookup_result =
+let lookup_fun (env : env) depth (f : C.fn_ptr) : K.expr' * lookup_result * C.trait_ref list =
   let open RustNames in
-  let matches p = Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config p f in
+  let pat = pattern_of_fn_ptr env f in
+  L.log "Calls" "%sLooking up function: %s" depth
+    (Charon.PrintTypes.fn_ptr_to_string env.format_env f);
+  L.log "Calls" "%sfn-ptr-pattern: %s" depth (string_of_pattern pat);
+  let matches (p : Charon.NameMatcher.pattern) =
+    L.log "Calls" "%smatching against pattern: %s" depth
+      (Charon.NameMatcher.pattern_to_string { Charon.NameMatcher.tgt = TkPattern } p);
+    let ret = Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config p f in
+    L.log "Calls" "%smatch result: %b" depth ret;
+    ret
+  in
   let builtin b =
     let { Builtin.name; typ; n_type_args; cg_args; _ } = b in
     let ret_type, arg_types = Krml.Helpers.flatten_arrow typ in
@@ -1269,13 +1408,16 @@ let lookup_fun (env : env) depth (f : C.fn_ptr) : K.expr' * lookup_result =
     K.EQualified name, { ts; arg_types; ret_type; cg_types = cg_args; is_known_builtin = true }
   in
   match List.find_opt (fun (p, _) -> matches p) known_builtins with
-  | Some (_, b) -> builtin b
+  | Some (_, b) ->
+      let hd, res = builtin b in
+      hd, res, []
   | None -> (
       let lookup_result_of_fun_id fun_id =
         let { C.item_meta; signature; _ } = env.get_nth_function fun_id in
         let lid = lid_of_name env item_meta.name in
         L.log "Calls" "%s--> name: %a" depth plid lid;
-        K.EQualified lid, lookup_signature env depth signature
+        let trait_refs = trait_refs_c_name item_meta.name in
+        K.EQualified lid, lookup_signature env depth signature, trait_refs
       in
 
       match f.kind with
@@ -1303,7 +1445,10 @@ let lookup_fun (env : env) depth (f : C.fn_ptr) : K.expr' * lookup_result =
               in
               let ret_type, arg_types = Krml.Helpers.flatten_arrow t in
               let cg_types, arg_types = Krml.KList.split sig_info.n_cgs arg_types in
-              EBound f, { ts = sig_info; cg_types; arg_types; ret_type; is_known_builtin = false }
+              ( EBound f,
+                { ts = sig_info; cg_types; arg_types; ret_type; is_known_builtin = false },
+                [] )
+              (* todo: check whether trait_refs is needed here *)
           | _ ->
               fail "Error looking trait ref: %s %s%!"
                 (Charon.PrintTypes.trait_ref_to_string env.format_env trait_ref)
@@ -1318,14 +1463,24 @@ let fn_ptr_is_opaque env (fn_ptr : C.fn_ptr) =
    contains type application, const generic applications, and application of trait methods to
    implement the dictionary-passing style. *)
 let rec expression_of_fn_ptr env depth (fn_ptr : C.fn_ptr) =
-  let {
-    C.generics = { types = type_args; const_generics = const_generic_args; trait_refs; _ };
-    kind;
-    _;
-  } : C.fn_ptr =
-    fn_ptr
+  let { C.generics; kind; _ } : C.fn_ptr = fn_ptr in
+
+  (* The function itself, along with information about its *signature*. *)
+  let ( f,
+        { ts; arg_types = inputs; ret_type = output; cg_types = cg_inputs; is_known_builtin },
+        trait_refs_mono ) =
+    lookup_fun env depth fn_ptr
   in
 
+  let generics =
+    match try_get_mono_generics is_known_builtin env fn_ptr with
+    | None -> generics
+    (* Essentially, there might still be (late-bound) region arguments in the original generics
+     But we don't care about them (the regions), so just ignore them. *)
+    | Some generics -> generics.binder_value
+  in
+  let { C.types = type_args; const_generics = const_generic_args; trait_refs; _ } = generics in
+
   (* We handle any kind of fn_ptr, whether it's a concrete function call, a
      concrete trait implementation method call, or an abstract trait method call
      (e.g. a call to T::f when T is a trait bound in scope). *)
@@ -1343,9 +1498,14 @@ let rec expression_of_fn_ptr env depth (fn_ptr : C.fn_ptr) =
   let type_args, const_generic_args, trait_refs =
     let generics =
       match kind with
-      | TraitMethod ({ kind = TraitImpl { generics; _ }; _ }, _, _) ->
+      | TraitMethod ({ kind = TraitImpl { generics; id }; _ }, _, _) -> begin
           L.log "Calls" "%s--> this is a trait method" depth;
-          generics
+          let trait_impl = env.get_nth_trait_impl id in
+          match try_get_mono_from_name trait_impl.item_meta.name with
+          (* The same applies here: ignoring potential region arguments *)
+          | Some generics when is_known_builtin -> generics.binder_value
+          | _ -> generics
+        end
       | _ -> C.empty_generic_args
     in
     ( generics.types @ type_args,
@@ -1362,12 +1522,12 @@ let rec expression_of_fn_ptr env depth (fn_ptr : C.fn_ptr) =
   L.log "Calls" "%s--> type_args: %s" depth
     (String.concat ", " (List.map (Charon.PrintTypes.ty_to_string env.format_env) type_args));
 
-  (* The function itself, along with information about its *signature*. *)
-  let f, { ts; arg_types = inputs; ret_type = output; cg_types = cg_inputs; is_known_builtin } =
-    lookup_fun env depth fn_ptr
-  in
   L.log "Calls" "%s--> %d inputs: %a" depth (List.length inputs) ptyps inputs;
   L.log "Calls" "%s--> is_known_builtin?: %b" depth is_known_builtin;
+  L.log "Calls" "%s--> [MONO] trait from mono name: %s\n" depth
+    (String.concat " ++ "
+       (List.map (Charon.PrintTypes.trait_ref_to_string env.format_env) trait_refs));
+  L.log "Calls" "%s--> [MONO] end of trait refs" depth;
 
   (* Translate effective type and cg arguments. *)
   let const_generic_args =
@@ -1393,6 +1553,92 @@ let rec expression_of_fn_ptr env depth (fn_ptr : C.fn_ptr) =
   (* Handling trait implementations for generic trait bounds in the callee. We
      synthesize krml expressions that correspond to each one of the trait methods
      that the callee expects. Order matters here. *)
+
+  (* MUST have the same structure as mk_clause_binders_and_args *)
+  let rec build_trait_ref_mapping depth (trait_refs : C.trait_ref list) =
+    List.concat_map
+      (fun (trait_ref : C.trait_ref) ->
+        let cname =
+          pure_c_name
+            (env.get_nth_trait_decl trait_ref.trait_decl_ref.binder_value.id).item_meta.name
+        in
+        let name = string_of_name env cname in
+        L.log "Calls" "%s--> trait_ref %s: %s\n" depth name (C.show_trait_ref trait_ref);
+
+        match trait_ref.kind with
+        | _ when List.mem name blocklisted_trait_decls ->
+            (* Trait not supported -- don't synthesize arguments *)
+            []
+        | TraitImpl { id = impl_id; generics = _generics } ->
+            (* Call-site has resolved trait clauses into a concrete trait implementation. *)
+            let trait_impl : C.trait_impl = env.get_nth_trait_impl impl_id in
+
+            (* This must be in agreement, and in the same order as mk_clause_binders_and_args *)
+            List.map
+              (fun ((_item_name, { C.id; generics }) : _ * C.global_decl_ref) ->
+                if
+                  not
+                    (generics.types = [] && generics.const_generics = [] && generics.trait_refs = [])
+                then
+                  failwith "TODO: polymorphic globals";
+                let global = env.get_nth_global id in
+                K.with_type (typ_of_ty env global.ty)
+                  (K.EQualified (lid_of_name env global.item_meta.name)))
+              trait_impl.consts
+            @ List.map
+                (fun ((item_name, bound_fn) : _ * C.fun_decl_ref C.binder) ->
+                  let fun_decl_id = bound_fn.C.binder_value.C.id in
+                  let fn_ptr : C.fn_ptr =
+                    {
+                      kind = TraitMethod (trait_ref, item_name, fun_decl_id);
+                      generics = Charon.TypesUtils.empty_generic_args;
+                    }
+                  in
+                  let fn_ptr = fst3 (expression_of_fn_ptr env (depth ^ "  ") fn_ptr) in
+                  fn_ptr)
+                trait_impl.methods
+            @ build_trait_ref_mapping ("  " ^ depth)
+                (let subst =
+                   Charon.Substitute.make_subst_from_generics trait_impl.generics _generics
+                 in
+                 (*_generics.trait_refs*)
+                 List.map
+                   (Charon.Substitute.st_substitute_visitor#visit_trait_ref subst)
+                   trait_impl.implied_trait_refs)
+        | Clause _ as clause_id ->
+            (* Caller it itself polymorphic and refers to one of its own clauses to synthesize
+              the clause arguments at call-site. We must pass whatever is relevant for this
+              clause, *transitively* (this means all the reachable parents). *)
+            let rec relevant = function
+              | C.ParentClause (tref', _) -> relevant tref'.kind
+              | clause_id' -> clause_id = clause_id'
+            in
+            List.rev
+              (Krml.KList.filter_mapi
+                 (fun i (var, t) ->
+                   match var with
+                   | TraitClauseMethod { clause_id = clause_id'; _ }
+                   | TraitClauseConstant { clause_id = clause_id'; _ }
+                     when relevant clause_id' -> Some K.(with_type t (EBound i))
+                   | _ -> None)
+                 env.binders)
+        | ParentClause (tref, clause_id) ->
+            let decl_id = tref.trait_decl_ref.binder_value.id in
+            let trait_decl = env.get_nth_trait_decl decl_id in
+            let name = string_of_name env trait_decl.item_meta.name in
+            let clause_id = C.TraitClauseId.to_int clause_id in
+            let parent_clause = List.nth trait_decl.implied_clauses clause_id in
+            let parent_clause_decl = env.get_nth_trait_decl parent_clause.trait.binder_value.id in
+            let parent_name = string_of_name env parent_clause_decl.item_meta.name in
+            Krml.KPrint.bprintf "looking up parent clause #%d of decl=%s = %s\n" clause_id name
+              parent_name;
+            if List.mem parent_name blocklisted_trait_decls then
+              []
+            else
+              failwith "Don't know how to resolve trait_ref above (1)"
+        | _ -> failwith "Don't know how to resolve trait_ref above (2)")
+      trait_refs
+  in
   let fn_ptrs : K.expr list =
     if is_known_builtin then
       (* If this is a known builtin implementation, we do not materialize trait methods, on the
@@ -1401,96 +1647,26 @@ let rec expression_of_fn_ptr env depth (fn_ptr : C.fn_ptr) =
          anyhow. *)
       []
     else
-      (* MUST have the same structure as mk_clause_binders_and_args *)
-      let rec build_trait_ref_mapping depth (trait_refs : C.trait_ref list) =
-        List.concat_map
-          (fun (trait_ref : C.trait_ref) ->
-            let name =
-              string_of_name env
-                (env.get_nth_trait_decl trait_ref.trait_decl_ref.binder_value.id).item_meta.name
-            in
-            L.log "Calls" "%s--> trait_ref %s: %s\n" depth name (C.show_trait_ref trait_ref);
-
-            match trait_ref.kind with
-            | _ when List.mem name blocklisted_trait_decls ->
-                (* Trait not supported -- don't synthesize arguments *)
-                []
-            | TraitImpl { id = impl_id; generics = _generics } ->
-                (* Call-site has resolved trait clauses into a concrete trait implementation. *)
-                let trait_impl : C.trait_impl = env.get_nth_trait_impl impl_id in
-
-                (* This must be in agreement, and in the same order as mk_clause_binders_and_args *)
-                List.map
-                  (fun ((_item_name, { C.id; generics }) : _ * C.global_decl_ref) ->
-                    if
-                      not
-                        (generics.types = [] && generics.const_generics = []
-                       && generics.trait_refs = [])
-                    then
-                      failwith "TODO: polymorphic globals";
-                    let global = env.get_nth_global id in
-                    K.with_type (typ_of_ty env global.ty)
-                      (K.EQualified (lid_of_name env global.item_meta.name)))
-                  trait_impl.consts
-                @ List.map
-                    (fun ((item_name, bound_fn) : _ * C.fun_decl_ref C.binder) ->
-                      let fun_decl_id = bound_fn.C.binder_value.C.id in
-                      let fn_ptr : C.fn_ptr =
-                        {
-                          kind = TraitMethod (trait_ref, item_name, fun_decl_id);
-                          generics = Charon.TypesUtils.empty_generic_args;
-                        }
-                      in
-                      let fn_ptr = fst3 (expression_of_fn_ptr env (depth ^ "  ") fn_ptr) in
-                      fn_ptr)
-                    trait_impl.methods
-                @ build_trait_ref_mapping ("  " ^ depth)
-                    (let subst =
-                       Charon.Substitute.make_subst_from_generics trait_impl.generics _generics
-                     in
-                     (*_generics.trait_refs*)
-                     List.map
-                       (Charon.Substitute.st_substitute_visitor#visit_trait_ref subst)
-                       trait_impl.implied_trait_refs)
-            | Clause _ as clause_id ->
-                (* Caller it itself polymorphic and refers to one of its own clauses to synthesize
-                   the clause arguments at call-site. We must pass whatever is relevant for this
-                   clause, *transitively* (this means all the reachable parents). *)
-                let rec relevant = function
-                  | C.ParentClause (tref', _) -> relevant tref'.kind
-                  | clause_id' -> clause_id = clause_id'
-                in
-                List.rev
-                  (Krml.KList.filter_mapi
-                     (fun i (var, t) ->
-                       match var with
-                       | TraitClauseMethod { clause_id = clause_id'; _ }
-                       | TraitClauseConstant { clause_id = clause_id'; _ }
-                         when relevant clause_id' -> Some K.(with_type t (EBound i))
-                       | _ -> None)
-                     env.binders)
-            | ParentClause (tref, clause_id) ->
-                let decl_id = tref.trait_decl_ref.binder_value.id in
-                let trait_decl = env.get_nth_trait_decl decl_id in
-                let name = string_of_name env trait_decl.item_meta.name in
-                let clause_id = C.TraitClauseId.to_int clause_id in
-                let parent_clause = List.nth trait_decl.implied_clauses clause_id in
-                let parent_clause_decl =
-                  env.get_nth_trait_decl parent_clause.trait.binder_value.id
-                in
-                let parent_name = string_of_name env parent_clause_decl.item_meta.name in
-                Krml.KPrint.bprintf "looking up parent clause #%d of decl=%s = %s\n" clause_id name
-                  parent_name;
-                if List.mem parent_name blocklisted_trait_decls then
-                  []
-                else
-                  failwith "Don't know how to resolve trait_ref above (1)"
-            | _ -> failwith "Don't know how to resolve trait_ref above (2)")
-          trait_refs
-      in
       build_trait_ref_mapping depth trait_refs
   in
   L.log "Calls" "%s--> trait method impls: %d" depth (List.length fn_ptrs);
+  let fn_ptrs_mono : K.expr list =
+    if is_known_builtin then
+      (* If this is a known builtin implementation, we do not materialize trait methods, on the
+         basis that this is likely something from the standard library that exercises more features
+         that we can support, and that since we hand-write it, we don't need this level of precision
+         anyhow. *)
+      []
+    else
+      build_trait_ref_mapping depth trait_refs_mono
+  in
+  (* update the fn_ptrs_mono in the table *)
+  begin
+    if fn_ptrs_mono <> [] then
+      match f with
+      | EQualified full_name -> update_lid_full_generic_fnptrs full_name fn_ptrs_mono
+      | _ -> ()
+  end;
 
   (* This needs to match what is done in the FunGroup case (i.e. when we extract
      a definition). There are two behaviors depending on whether the function is
@@ -1735,8 +1911,6 @@ let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr =
             Some (lid2, TApp (slice_hd, [ u2 ]), t_u) )
           when lid1 = lid2 && u1 = u2 && slice_hd = Builtin.derefed_slice && lid_arr = Builtin.arr
           ->
-            (* Cast from a struct whose last field is `t data[n]` to a struct whose last field is
-             `Eurydice_derefed_slice data` (a.k.a. `char data[]`) *)
             let len = expression_of_cg env cg in
             let ptr = K.with_type (TBuf (t_u, false)) (K.ECast (e, TBuf (t_u, false))) in
             Builtin.dst_new ~len ~ptr t_u
diff --git a/lib/Builtin.ml b/lib/Builtin.ml
index 40ad7954..a3e9a02e 100644
--- a/lib/Builtin.ml
+++ b/lib/Builtin.ml
@@ -165,6 +165,23 @@ let array_to_subslice =
     arg_names = [ "a"; "r" ];
   }
 
+(* The version of `array_to_subslice` for monomorphic LLBC.
+   Core changes: there is no assoc-ty for the generics `Self::Output`
+   Also, its argument is a monomorphized `Range::<usize>` instead of a generic one.
+   The same as below for `array_to_subslice_to` and `array_to_subslice_from`.
+*)
+let array_to_subslice_mono =
+  {
+    name = [ "Eurydice" ], "array_to_subslice_mono";
+    typ =
+      Krml.Helpers.fold_arrow
+        [ TBuf (TBound 1, false); TQualified ([ "core"; "ops"; "range"; "Range" ], "<usize>") ]
+        (mk_slice (TBound 1));
+    n_type_args = 2;
+    cg_args = [ TInt SizeT ];
+    arg_names = [ "a"; "r" ];
+  }
+
 let array_to_subslice_to =
   {
     name = [ "Eurydice" ], "array_to_subslice_to";
@@ -177,6 +194,19 @@ let array_to_subslice_to =
     arg_names = [ "a"; "r" ];
   }
 
+(* The version of `array_to_subslice_to` for monomorphic LLBC. *)
+let array_to_subslice_to_mono =
+  {
+    name = [ "Eurydice" ], "array_to_subslice_to_mono";
+    typ =
+      Krml.Helpers.fold_arrow
+        [ TBuf (TBound 1, false); TQualified ([ "core"; "ops"; "range"; "RangeTo" ], "<usize>") ]
+        (mk_slice (TBound 1));
+    n_type_args = 2;
+    cg_args = [ TInt SizeT ];
+    arg_names = [ "a"; "r" ];
+  }
+
 let array_to_subslice_from =
   {
     name = [ "Eurydice" ], "array_to_subslice_from";
@@ -189,6 +219,19 @@ let array_to_subslice_from =
     arg_names = [ "a"; "r" ];
   }
 
+(* The version of `array_to_subslice_from` for monomorphic LLBC. *)
+let array_to_subslice_from_mono =
+  {
+    name = [ "Eurydice" ], "array_to_subslice_from_mono";
+    typ =
+      Krml.Helpers.fold_arrow
+        [ TBuf (TBound 1, false); TQualified ([ "core"; "ops"; "range"; "RangeFrom" ], "<usize>") ]
+        (mk_slice (TBound 1));
+    n_type_args = 2;
+    cg_args = [ TInt SizeT ];
+    arg_names = [ "a"; "r" ];
+  }
+
 (* These two are placeholders that are inserted by AstOfLlbc with the intent that they should be
    desugared later on, once monomorphization and data type compilation, respectively, have happened. *)
 let array_repeat =
@@ -301,6 +344,44 @@ let slice_index =
     arg_names = [ "s"; "i" ];
   }
 
+let slice_len =
+  {
+    name = [ "Eurydice" ], "slice_len";
+    typ = Krml.Helpers.fold_arrow [ mk_slice (TBound 0) ] (TInt SizeT);
+    n_type_args = 1;
+    cg_args = [];
+    arg_names = [ "s" ];
+  }
+
+let slice_copy =
+  {
+    name = [ "Eurydice" ], "slice_copy";
+    typ = Krml.Helpers.fold_arrow [ mk_slice (TBound 0); mk_slice (TBound 0) ] TUnit;
+    n_type_args = 1;
+    cg_args = [];
+    arg_names = [ "s" ];
+  }
+
+let slice_split_at =
+  let slice = mk_slice (TBound 0) in
+  {
+    name = [ "Eurydice" ], "slice_split_at";
+    typ = Krml.Helpers.fold_arrow [ slice; TInt SizeT ] (K.TTuple [ slice; slice ]);
+    n_type_args = 1;
+    cg_args = [];
+    arg_names = [ "s"; "mid" ];
+  }
+
+let slice_split_at_mut =
+  let slice = mk_slice (TBound 0) in
+  {
+    name = [ "Eurydice" ], "slice_split_at_mut";
+    typ = Krml.Helpers.fold_arrow [ slice; TInt SizeT ] (K.TTuple [ slice; slice ]);
+    n_type_args = 1;
+    cg_args = [];
+    arg_names = [ "s"; "mid" ];
+  }
+
 let slice_index_outparam =
   {
     name = [ "Eurydice" ], "slice_index_outparam";
@@ -742,11 +823,18 @@ let builtin_funcs =
     array_to_subslice;
     array_to_subslice_to;
     array_to_subslice_from;
+    array_to_subslice_mono;
+    array_to_subslice_to_mono;
+    array_to_subslice_from_mono;
     array_repeat;
     array_into_iter;
     array_eq;
     array_eq_slice;
     slice_eq;
+    slice_len;
+    slice_copy;
+    slice_split_at;
+    slice_split_at_mut;
     slice_index;
     slice_index_outparam;
     slice_subslice;
diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml
index e255c02c..f206b8b7 100644
--- a/lib/Cleanup2.ml
+++ b/lib/Cleanup2.ml
@@ -348,7 +348,8 @@ let remove_array_from_fn files =
         super#visit_DFunction () cc flags n_cgs n t name bs e
 
       method! visit_EApp env e es =
-        match e.node with
+        let e' = AstOfLlbc.re_polymorphize e in
+        match e'.node with
         | ETApp
             ( { node = EQualified ([ "core"; "array" ], "from_fn"); _ },
               [ len ],
@@ -495,7 +496,7 @@ let remove_trivial_into =
     method! visit_EApp env e es =
       let e = self#visit_expr_w () e in
       let es = List.map (self#visit_expr env) es in
-      match e.node, es with
+      match (AstOfLlbc.re_polymorphize e).node, es with
       | ( ETApp ({ node = EQualified ([ "core"; "convert"; _ ], "into"); _ }, [], _, [ t1; t2 ]),
           [ e1 ] )
         when t1 = t2 -> e1.node
@@ -640,6 +641,44 @@ let ends_with_return =
       | EReturn _ -> true
       | _ -> false)
 
+let width_of_int_name name : width =
+  match name with
+  | "<i8>" -> Int8
+  | "<i16>" -> Int16
+  | "<i32>" -> Int32
+  | "<i64>" -> Int64
+  | "<u8>" -> UInt8
+  | "<u16>" -> UInt16
+  | "<u32>" -> UInt32
+  | "<u64>" -> UInt64
+  | "<usize>" -> SizeT
+  | _ -> invalid_arg name
+
+let type_of_int_name name = TInt (width_of_int_name name)
+let node_of_with_type e' = e'.node
+let typ_of_with_type e' = e'.typ
+
+let rest_of_let' e_let =
+  match e_let with
+  | ELet (_, _, e_rest) -> e_rest
+  | _ -> assert false
+
+let rest_of_let e_let' = e_let' |> node_of_with_type |> rest_of_let'
+
+let body_of_while' e_while =
+  match e_while with
+  | EWhile (_, e_body) -> e_body
+  | _ -> assert false
+
+let body_of_while e_while' = e_while' |> node_of_with_type |> body_of_while'
+
+let binder_of_let e_let =
+  match e_let with
+  | ELet (b, _, _) -> b
+  | _ -> assert false
+
+let typ_of_let e_let = e_let |> node_of_with_type |> binder_of_let |> typ_of_with_type
+
 let resugar_loops =
   object(self)
   inherit [_] map as super
@@ -876,6 +915,129 @@ let resugar_loops =
         self#visit_expr env e_body)
       ) :: List.map (fun e -> self#visit_expr env (Krml.DeBruijn.subst eunit 0 e)) rest)
 
+    (* Terminal position (regular range for-loop) *)
+    | [%cremepat {|
+      let iter =
+        core::iter::traits::collect::?::into_iter::?range_name
+          ({ start: ?e_start, end: ?e_end });
+      while true {
+        let x = core::iter::range::?::next::?t1_name(&iter);
+        match x {
+          None -> break,
+          Some ? -> ?e_body
+        }
+      }
+    |}] when Krml.KString.starts_with range_name "<core::ops::range::Range::" ->
+      let open Krml.Helpers in
+      let w = width_of_int_name t1_name in
+      let t1 = TInt w in
+      let t_op = e |> rest_of_let |> body_of_while |> typ_of_let in 
+      let e_some_i = with_type t_op (ECons ("Some", [with_type t1 (EBound 0)])) in
+      with_type e.typ @@ EFor (fresh_binder ~mut:true "i" t1,
+        e_start,
+        mk_lt w (Krml.DeBruijn.lift 1 e_end),
+        mk_incr w,
+        self#visit_expr env (Krml.DeBruijn.subst e_some_i 0 e_body))
+
+    | [%cremepat {|
+      let iter =
+        core::iter::traits::collect::?::into_iter::?range_name
+          ({ start: ?e_start, end: ?e_end });
+      while true {
+        match (core::iter::range::?::next::?t1_name(&iter)) {
+          None -> break,
+          Some ? -> ?e_body
+        }
+      }
+    |}] when Krml.KString.starts_with range_name "<core::ops::range::Range::" ->
+      let open Krml.Helpers in
+      let w = width_of_int_name t1_name in
+      let t1 = TInt w in
+      with_type e.typ @@ EFor (fresh_binder ~mut:true "i" t1,
+        e_start,
+        mk_lt w (Krml.DeBruijn.lift 1 e_end),
+        mk_incr w,
+        self#visit_expr env e_body)
+
+    (* Non-terminal position (regular range for-loop) *)
+    | [%cremepat {|
+      let iter =
+        core::iter::traits::collect::?::into_iter::?range_name
+          ({ start: ?e_start, end: ?e_end });
+      while true {
+        let x = core::iter::range::?::next::?t1_name(&iter);
+        match x {
+          None -> break,
+          Some ? -> ?e_body
+        }
+      };
+      ?rest..
+    |}] when Krml.KString.starts_with range_name "<core::ops::range::Range::"->
+      let open Krml.Helpers in
+      let w = width_of_int_name t1_name in
+      let t1 = TInt w in
+      let t_op = e |> rest_of_let |> body_of_while |> typ_of_let in
+      let e_some_i = with_type t_op (ECons ("Some", [with_type t1 (EBound 0)])) in
+      with_type e.typ @@ ESequence (with_type TUnit (EFor (fresh_binder ~mut:true "i" t1,
+        e_start,
+        mk_lt w (Krml.DeBruijn.lift 1 e_end),
+        mk_incr w,
+        self#visit_expr env (Krml.DeBruijn.subst e_some_i 0 e_body))
+      ) :: List.map (fun e -> self#visit_expr env (Krml.DeBruijn.subst eunit 0 e)) rest)
+
+    (* Special variant that appears in external crates -- TODO: do we need variants of all other
+       patterns? *)
+    | [%cremepat {|
+      let iter =
+        core::iter::traits::collect::?::into_iter::?range_name
+          ({ start: ?e_start, end: ?e_end });
+      while true {
+        let x = core::iter::range::?::next::?t1_name(&iter);
+        match x {
+          None -> ?e2,
+          Some ? -> ?e_body
+        };
+        abort
+      }
+    |}] when Krml.KString.starts_with range_name "<core::ops::range::Range::" && ends_with_return e2 && ends_with_continue e_body
+    (* && x does not appear in e2 *) ->
+      let open Krml.Helpers in
+      let w = width_of_int_name t1_name in
+      let t1 = TInt w in
+      let t_op = e |> rest_of_let |> body_of_while |> typ_of_let in
+      let e_some_i = with_type t_op (ECons ("Some", [with_type t1 (EBound 0)])) in
+      with_type e.typ @@ ESequence [
+        with_type TUnit (EFor (fresh_binder ~mut:true "i" t1,
+          e_start,
+          mk_lt w (Krml.DeBruijn.lift 1 e_end),
+          mk_incr w,
+          self#visit_expr env (Krml.DeBruijn.subst e_some_i 0 e_body))
+        );
+        self#visit_expr env (Krml.DeBruijn.(subst eunit 0 (subst eunit 0 e2)))
+      ]
+
+    | [%cremepat {|
+      let iter =
+        core::iter::traits::collect::?::into_iter::?range_name
+          ({ start: ?e_start, end: ?e_end });
+      while true {
+        match (core::iter::range::?::next::?t1_name(&iter)) {
+          None -> break,
+          Some ? -> ?e_body
+        }
+      };
+      ?rest..
+    |}] when Krml.KString.starts_with range_name "<core::ops::range::Range::" ->
+      let open Krml.Helpers in
+      let w = width_of_int_name t1_name in
+      let t1 = TInt w in
+      with_type e.typ @@ ESequence (with_type TUnit (EFor (fresh_binder ~mut:true "i" t1,
+        e_start,
+        mk_lt w (Krml.DeBruijn.lift 1 e_end),
+        mk_incr w,
+        self#visit_expr env e_body)
+      ) :: List.map (fun e -> self#visit_expr env (Krml.DeBruijn.subst eunit 0 e)) rest)
+
     | _ ->
       super#visit_expr env e
 
@@ -916,6 +1078,19 @@ let improve_names files =
             Krml.Bundle.Lid (fst (Hashtbl.find renamed lid))
         | x -> x)
       !Krml.Options.static_header;
+  let update_expr e =
+    match e.node with
+    | EQualified lid when Hashtbl.mem renamed lid ->
+        { e with node = EQualified (fst (Hashtbl.find renamed lid)) }
+    | _ -> e
+  in
+  let update_value _key value =
+    match value with
+    | name, cgs, ts, fn_ptrs ->
+        let fn_ptrs = List.map update_expr fn_ptrs in
+        Some (name, cgs, ts, fn_ptrs)
+  in
+  Hashtbl.filter_map_inplace update_value AstOfLlbc.lid_full_generic;
   (object (self)
      inherit [_] map
 
@@ -1104,18 +1279,43 @@ let remove_assign_return =
   end
 
 let bonus_cleanups =
-  let open Krml in
   object (self)
     inherit [_] map as super
     method! extend env b = b.node.name :: env
 
-    method! visit_lident _ lid =
-      match lid with
-      | [ "core"; "slice"; "{@Slice<T>}" ], "len" -> [ "Eurydice" ], "slice_len"
-      | [ "core"; "slice"; "{@Slice<T>}" ], "copy_from_slice" -> [ "Eurydice" ], "slice_copy"
-      | [ "core"; "slice"; "{@Slice<T>}" ], "split_at" -> [ "Eurydice" ], "slice_split_at"
-      | [ "core"; "slice"; "{@Slice<T>}" ], "split_at_mut" -> [ "Eurydice" ], "slice_split_at_mut"
-      | _ -> lid
+    method! visit_expr env e =
+      let match_lident lid =
+        let is_slice_t s =
+          let pattern = Str.regexp {|\{@Slice<.*>\}|} in
+          s = "{@Slice<T>}" || Str.string_match pattern s 0
+        in
+        match lid with
+        | [ "core"; "slice"; s ], "len" when is_slice_t s ->
+            true, ([ "Eurydice" ], "slice_len"), Builtin.slice_len.typ
+        | [ "core"; "slice"; s ], "copy_from_slice" when is_slice_t s ->
+            true, ([ "Eurydice" ], "slice_copy"), Builtin.slice_copy.typ
+        | [ "core"; "slice"; s ], "split_at" when is_slice_t s ->
+            true, ([ "Eurydice" ], "slice_split_at"), Builtin.slice_split_at.typ
+        | [ "core"; "slice"; s ], "split_at_mut" when is_slice_t s ->
+            true, ([ "Eurydice" ], "slice_split_at_mut"), Builtin.slice_split_at_mut.typ
+        | _ -> false, lid, TAny
+      in
+      let e' = AstOfLlbc.re_polymorphize e in
+      match e'.node with
+      | ETApp (expr, cgs, [], ts) -> begin
+          match expr.node with
+          | EQualified lid ->
+              L.log "Cleanup2" "[Bonus] Visiting lid: %a\n" plid lid;
+              let matched, lid, t = match_lident lid in
+              if matched then begin
+                L.log "Cleanup2" "[Bonus] lid: %a matched!\n" plid lid;
+                with_type e.typ (ETApp ({ expr with node = EQualified lid; typ = t }, cgs, [], ts))
+              end
+              else
+                super#visit_expr env e
+          | _ -> super#visit_expr env e
+        end
+      | _ -> super#visit_expr env e
 
     method! visit_ELet ((bs, _) as env) b e1 e2 =
       match e1.node, e1.typ, e2.node with
@@ -1123,7 +1323,7 @@ let bonus_cleanups =
       | ( EAny,
           _,
           ESequence [ { node = EAssign ({ node = EBound 0; _ }, e3); _ }; { node = EBound 0; _ } ] )
-        -> (DeBruijn.subst Helpers.eunit 0 e3).node
+        -> Krml.(DeBruijn.subst Helpers.eunit 0 e3).node
       (* let uu; memcpy(uu, ..., src, ...); e2  -->  let copy_of_src; ... *)
       | ( EAny,
           TArray (_, (_, n)),
@@ -1153,11 +1353,12 @@ let bonus_cleanups =
       | ( EApp ({ node = EQualified _; _ }, es),
           _,
           ESequence [ { node = EAssign (e2, { node = EBound 0; _ }); _ }; e3 ] )
-        when Helpers.is_uu b.node.name && List.for_all Helpers.is_readonly_c_expression es ->
+        when Krml.Helpers.is_uu b.node.name && List.for_all Krml.Helpers.is_readonly_c_expression es
+        ->
           ESequence
             [
-              with_type TUnit (EAssign (DeBruijn.subst Helpers.eunit 0 e2, e1));
-              self#visit_expr env (DeBruijn.subst Helpers.eunit 0 e3);
+              with_type TUnit (EAssign (Krml.DeBruijn.subst Krml.Helpers.eunit 0 e2, e1));
+              self#visit_expr env (Krml.DeBruijn.subst Krml.Helpers.eunit 0 e3);
             ]
       | _ -> super#visit_ELet env b e1 e2
   end
@@ -1428,3 +1629,184 @@ let remove_discriminant_reads (map : Krml.DataTypes.map) files =
   end)
     #visit_files
     () files
+
+(* Remove the unused DType declarations *)
+let drop_unused_type files =
+  let open Krml in
+  let seen = Hashtbl.create 41 in
+
+  let body_of_lid = Helpers.build_map files (fun map d -> Hashtbl.add map (lid_of_decl d) d) in
+
+  let visitor =
+    object (self)
+      inherit [_] iter as super
+      method! visit_EQualified (before, _) lid = self#discover before lid
+      method! visit_TQualified before lid = self#discover before lid
+
+      method! visit_TApp before lid ts =
+        self#discover before lid;
+        List.iter (self#visit_typ before) ts
+
+      method private discover before lid =
+        if not (Hashtbl.mem seen lid) then begin
+          Hashtbl.add seen lid ();
+          if Options.debug "reachability" then
+            KPrint.bprintf "REACHABILITY: %a is used (via: %s) \n" plid lid
+              (String.concat " <- " (List.map (fun lid -> KPrint.bsprintf "%a" plid lid) before));
+
+          if Hashtbl.mem body_of_lid lid then
+            ignore (super#visit_decl (lid :: before) (Hashtbl.find body_of_lid lid))
+        end
+    end
+  in
+  visitor#visit_files [] files;
+  filter_decls
+    (fun d ->
+      match d with
+      | DType (lid, _flags, _, _, _) ->
+          if Hashtbl.mem seen lid then
+            Some d
+          else
+            None
+      | _ -> Some d)
+    files
+
+let drop_unused_monoed_func files =
+  let open Krml in
+  let seen = Hashtbl.create 41 in
+
+  let body_of_lid = Helpers.build_map files (fun map d -> Hashtbl.add map (lid_of_decl d) d) in
+
+  let visitor =
+    object (self)
+      inherit [_] iter as super
+      method! visit_EQualified (before, _) lid = self#discover before lid
+      method! visit_TQualified before lid = self#discover before lid
+
+      method! visit_TApp before lid ts =
+        self#discover before lid;
+        List.iter (self#visit_typ before) ts
+
+      method private discover before lid =
+        if not (Hashtbl.mem seen lid) then begin
+          Hashtbl.add seen lid ();
+          if Options.debug "reachability" then
+            KPrint.bprintf "REACHABILITY: %a is used (via: %s) \n" plid lid
+              (String.concat " <- " (List.map (fun lid -> KPrint.bsprintf "%a" plid lid) before));
+
+          if Hashtbl.mem body_of_lid lid then
+            ignore (super#visit_decl (lid :: before) (Hashtbl.find body_of_lid lid))
+        end
+    end
+  in
+  visitor#visit_files [] files;
+  filter_decls
+    (fun d ->
+      match d with
+      | DFunction (_, _, _, _, _, lid, _, _) ->
+          L.log "Cleanup2" "[Drop] visiting function %a \n" plid lid;
+          if Hashtbl.mem seen lid then
+            Some d
+          else begin
+            try
+              let _name, cgs, ts, fn_ptrs = Hashtbl.find AstOfLlbc.lid_full_generic lid in
+              if cgs = [] && ts = [] && fn_ptrs = [] then
+                Some d
+              else begin
+                L.log "Cleanup2" "[Drop] function %a droped as unused monoed func \n" plid lid;
+                None
+              end
+            with Not_found ->
+              begin
+                L.log "Cleanup2" "[Drop] function %a droped as unmapped func \n" plid lid;
+                None
+              end
+          end
+      | DExternal (_, _, _, _, lid, _, _) ->
+          L.log "Cleanup2" "[Drop] visiting function %a \n" plid lid;
+          if Hashtbl.mem seen lid then
+            Some d
+          else begin
+            try
+              let _name, cgs, ts, fn_ptrs = Hashtbl.find AstOfLlbc.lid_full_generic lid in
+              if cgs = [] && ts = [] && fn_ptrs = [] then
+                Some d
+              else begin
+                L.log "Cleanup2" "[Drop] function %a droped as unused monoed func \n" plid lid;
+                None
+              end
+            with Not_found ->
+              begin
+                L.log "Cleanup2" "[Drop] function %a droped as unmapped func \n" plid lid;
+                None
+              end
+          end
+      | _ -> Some d)
+    files
+
+let remove_empty_structs files =
+  let open Krml.Idents in
+  let empty_structs =
+    (object
+       inherit [_] reduce
+       method zero = LidSet.empty
+       method plus = LidSet.union
+
+       method! visit_DType _ lid _ _ _ def =
+         if def = Flat [] then
+           LidSet.singleton lid
+         else
+           LidSet.empty
+    end)
+      #visit_files
+      () files
+  in
+
+  let files =
+    List.map
+      (fun (f, decls) ->
+        f, List.filter (fun d -> not (LidSet.mem (lid_of_decl d) empty_structs)) decls)
+      files
+  in
+
+  let erase_obj =
+    object
+      inherit [_] map as super
+
+      method! visit_TApp _ lid ts =
+        if LidSet.mem lid empty_structs then
+          TUnit
+        else
+          super#visit_TApp () lid ts
+
+      method! visit_TCgApp _ t cg =
+        let lid, _, _ = flatten_tapp (TCgApp (t, cg)) in
+        if LidSet.mem lid empty_structs then
+          TUnit
+        else
+          super#visit_TCgApp () t cg
+
+      method! visit_TQualified _ lid =
+        if LidSet.mem lid empty_structs then
+          TUnit
+        else
+          TQualified lid
+
+      method! visit_EFlat env fields =
+        if fields = [] then begin
+          EUnit
+        end
+        else
+          super#visit_EFlat env fields
+    end
+  in
+  let update_value _key value =
+    match value with
+    | name, cgs, ts, fn_ptrs ->
+        let cgs = List.map (erase_obj#visit_expr_w ()) cgs in
+        let ts = List.map (erase_obj#visit_typ ()) ts in
+        let fn_ptrs = List.map (erase_obj#visit_expr_w ()) fn_ptrs in
+        Some (name, cgs, ts, fn_ptrs)
+  in
+  Hashtbl.filter_map_inplace update_value AstOfLlbc.lid_full_generic;
+  erase_obj#visit_files () files
diff --git a/lib/PreCleanup.ml b/lib/PreCleanup.ml
index f181b3a5..5ce4a76a 100644
--- a/lib/PreCleanup.ml
+++ b/lib/PreCleanup.ml
@@ -48,26 +48,43 @@ let remove_array_eq =
     inherit Krml.DeBruijn.map_counting_cg as super
 
     method! visit_expr (((n_cgs, n_binders) as env), _) e =
-      match e with
+      match AstOfLlbc.re_polymorphize e with
       | [%cremepat {| core::array::equality::?impl::eq[#?n](#?..)<?t,?u>(?a1, ?a2) |}] ->
           let rec is_flat = function
-            | TCgApp (TApp (lid, [ t ]), _) -> lid = Builtin.arr && is_flat t
+            | TArray (t, _) -> is_flat t
             | TInt _ | TBool | TUnit -> true
             | _ -> false
           in
           assert (t = u);
           if is_flat t then
             let diff = n_binders - n_cgs in
-            match impl with
-            | "{core::cmp::PartialEq<@Array<U, N>> for @Array<T, N>}" ->
-                with_type TBool
-                  (EApp (Builtin.(expr_of_builtin_t ~cgs:(diff, [ n ]) array_eq [ t ]), [ a1; a2 ]))
-            | "{core::cmp::PartialEq<&0 (@Slice<U>)> for @Array<T, N>}" ->
-                with_type TBool
-                  (EApp
-                     ( Builtin.(expr_of_builtin_t ~cgs:(diff, [ n ]) array_eq_slice [ t ]),
-                       [ a1; a2 ] ))
-            | _ -> failwith ("unknown array eq impl: " ^ impl)
+            let pattern_array_eq =
+              Str.regexp {|\{core::cmp::PartialEq::<@Array<.*, .*>, @Array<.*, .*>>\}|}
+            in
+            let matches_array_eq_slice =
+              Str.regexp {|\{core::cmp::PartialEq::<&.* @Slice<,*>, @Array<.*, .*)>>\}|}
+            in
+            (*todo: this pattern is not tested yet*)
+            let matches_array_eq s =
+              match s with
+              | "{core::cmp::PartialEq<@Array<U, N>> for @Array<T, N>}" ->
+                  true (* non-monomorphized LLBC *)
+              | _ -> ( try Str.string_match pattern_array_eq s 0 with Not_found -> false)
+            in
+            let matches_array_eq_slice s =
+              match s with
+              | "{core::cmp::PartialEq<&0 (@Slice<U>)> for @Array<T, N>}" -> true
+              | _ -> ( try Str.string_match matches_array_eq_slice s 0 with Not_found -> false)
+            in
+            if matches_array_eq impl then
+              with_type TBool
+                (EApp (Builtin.(expr_of_builtin_t ~cgs:(diff, [ n ]) array_eq [ t ]), [ a1; a2 ]))
+            else if matches_array_eq_slice impl then
+              with_type TBool
+                (EApp
+                   (Builtin.(expr_of_builtin_t ~cgs:(diff, [ n ]) array_eq_slice [ t ]), [ a1; a2 ]))
+            else
+              failwith ("unknown array eq impl: " ^ impl)
           else
             failwith "TODO: non-byteeq array comparison"
       | _ -> super#visit_expr (env, e.typ) e
diff --git a/out/test-array2d/array2d.h b/out/test-array2d/array2d.h
index e53051bf..61719e81 100644
--- a/out/test-array2d/array2d.h
+++ b/out/test-array2d/array2d.h
@@ -15,6 +15,9 @@
 extern "C" {
 #endif
 
+<<<<<<< HEAD
+bool array2d_f(uint32_t x[4U][2U]);
+=======
 extern bool core_cmp_impls__core__cmp__PartialEq_u32__for_u32__eq(uint32_t *x0, uint32_t *x1);
 
 extern bool core_cmp_impls__core__cmp__PartialEq_u32__for_u32__ne(uint32_t *x0, uint32_t *x1);
@@ -36,15 +39,12 @@ with const generics
 typedef struct Eurydice_arr_c0_s { Eurydice_arr_b2 data[4U]; } Eurydice_arr_c0;
 
 bool array2d_f(Eurydice_arr_c0 x);
-
-#define core_panicking_AssertKind_Eq 0
-#define core_panicking_AssertKind_Ne 1
-#define core_panicking_AssertKind_Match 2
-
-typedef uint8_t core_panicking_AssertKind;
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 
 void array2d_main(void);
 
+extern bool core_cmp_impls__core__cmp__PartialEq___u32__u32___eq(uint32_t *x0, uint32_t *x1);
+
 #if defined(__cplusplus)
 }
 #endif
diff --git a/out/test-closure_fn_cast/closure_fn_cast.c b/out/test-closure_fn_cast/closure_fn_cast.c
index afed83cf..841cdbc2 100644
--- a/out/test-closure_fn_cast/closure_fn_cast.c
+++ b/out/test-closure_fn_cast/closure_fn_cast.c
@@ -8,37 +8,37 @@
 #include "closure_fn_cast.h"
 
 /**
-This function found in impl {core::ops::function::Fn<(i32), i32> for closure_fn_cast::main::closure}
+This function found in impl {core::ops::function::Fn::<closure_fn_cast::main::closure, (i32)>}
 */
-int32_t closure_fn_cast_main_call_fd(void **_, int32_t tupled_args)
+int32_t closure_fn_cast_main_call_58(void **_, int32_t tupled_args)
 {
   int32_t x = tupled_args;
   return x + (int32_t)42;
 }
 
 /**
-This function found in impl {core::ops::function::FnMut<(i32), i32> for closure_fn_cast::main::closure}
+This function found in impl {core::ops::function::FnMut::<closure_fn_cast::main::closure, (i32)>}
 */
-int32_t closure_fn_cast_main_call_mut_68(void **state, int32_t args)
+int32_t closure_fn_cast_main_call_mut_2c(void **state, int32_t args)
 {
-  return closure_fn_cast_main_call_fd(state, args);
+  return closure_fn_cast_main_call_58(state, args);
 }
 
 /**
-This function found in impl {core::ops::function::FnOnce<(i32), i32> for closure_fn_cast::main::closure}
+This function found in impl {core::ops::function::FnOnce::<closure_fn_cast::main::closure, (i32)>}
 */
-int32_t closure_fn_cast_main_call_once_fd(int32_t _)
+int32_t closure_fn_cast_main_call_once_ef(int32_t _)
 {
   /* original Rust expression is not an lvalue in C */
   void *lvalue = (void *)0U;
-  return closure_fn_cast_main_call_mut_68(&lvalue, _);
+  return closure_fn_cast_main_call_mut_2c(&lvalue, _);
 }
 
 int32_t closure_fn_cast_main_closure_as_fn(int32_t arg1)
 {
   int32_t args = arg1;
   void *state = (void *)0U;
-  return closure_fn_cast_main_call_once_fd(args);
+  return closure_fn_cast_main_call_once_ef(args);
 }
 
 void closure_fn_cast_main(void)
diff --git a/out/test-closure_fn_cast/closure_fn_cast.h b/out/test-closure_fn_cast/closure_fn_cast.h
index 12076dca..0d6a75d2 100644
--- a/out/test-closure_fn_cast/closure_fn_cast.h
+++ b/out/test-closure_fn_cast/closure_fn_cast.h
@@ -16,19 +16,19 @@ extern "C" {
 #endif
 
 /**
-This function found in impl {core::ops::function::Fn<(i32), i32> for closure_fn_cast::main::closure}
+This function found in impl {core::ops::function::Fn::<closure_fn_cast::main::closure, (i32)>}
 */
-int32_t closure_fn_cast_main_call_fd(void **_, int32_t tupled_args);
+int32_t closure_fn_cast_main_call_58(void **_, int32_t tupled_args);
 
 /**
-This function found in impl {core::ops::function::FnMut<(i32), i32> for closure_fn_cast::main::closure}
+This function found in impl {core::ops::function::FnMut::<closure_fn_cast::main::closure, (i32)>}
 */
-int32_t closure_fn_cast_main_call_mut_68(void **state, int32_t args);
+int32_t closure_fn_cast_main_call_mut_2c(void **state, int32_t args);
 
 /**
-This function found in impl {core::ops::function::FnOnce<(i32), i32> for closure_fn_cast::main::closure}
+This function found in impl {core::ops::function::FnOnce::<closure_fn_cast::main::closure, (i32)>}
 */
-int32_t closure_fn_cast_main_call_once_fd(int32_t _);
+int32_t closure_fn_cast_main_call_once_ef(int32_t _);
 
 int32_t closure_fn_cast_main_closure_as_fn(int32_t arg1);
 
diff --git a/out/test-const_generics/Eurydice.h b/out/test-const_generics/Eurydice.h
index cb39bcb7..92605815 100644
--- a/out/test-const_generics/Eurydice.h
+++ b/out/test-const_generics/Eurydice.h
@@ -15,19 +15,9 @@
 extern "C" {
 #endif
 
-/**
-A monomorphic instance of core.ops.range.RangeTo
-with types size_t
+typedef size_t core_ops_range_RangeTo__usize_;
 
-*/
-typedef size_t core_ops_range_RangeTo_08;
-
-/**
-A monomorphic instance of core.ops.range.RangeFrom
-with types size_t
-
-*/
-typedef size_t core_ops_range_RangeFrom_08;
+typedef size_t core_ops_range_RangeFrom__usize_;
 
 #if defined(__cplusplus)
 }
diff --git a/out/test-const_generics/const_generics.c b/out/test-const_generics/const_generics.c
index 1a40620d..48f1ac73 100644
--- a/out/test-const_generics/const_generics.c
+++ b/out/test-const_generics/const_generics.c
@@ -9,16 +9,43 @@
 
 #include "Eurydice.h"
 
+<<<<<<< HEAD
+void const_generics_serialize__8usize_(Eurydice_slice re, uint8_t ret[8U])
+=======
 /**
 A monomorphic instance of const_generics.serialize
 with const generics
 - OUT_LEN= 8
 */
 Eurydice_arr_c4 const_generics_serialize_3b(Eurydice_slice re)
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 {
   Eurydice_arr_c4 out = { .data = { 0U } };
   Eurydice_slice
   uu____0 =
+<<<<<<< HEAD
+    Eurydice_array_to_subslice_to_mono((size_t)8U,
+      out,
+      (size_t)4U,
+      uint8_t,
+      size_t,
+      Eurydice_slice);
+  uint8_t ret0[4U];
+  core_num__u32__to_be_bytes(Eurydice_slice_index(re, (size_t)0U, uint32_t, uint32_t *), ret0);
+  Eurydice_slice_copy(uu____0, Eurydice_array_to_slice((size_t)4U, ret0, uint8_t), uint8_t);
+  Eurydice_slice
+  uu____1 =
+    Eurydice_array_to_subslice_from_mono((size_t)8U,
+      out,
+      (size_t)4U,
+      uint8_t,
+      size_t,
+      Eurydice_slice);
+  uint8_t ret1[4U];
+  core_num__u32__to_be_bytes(Eurydice_slice_index(re, (size_t)1U, uint32_t, uint32_t *), ret1);
+  Eurydice_slice_copy(uu____1, Eurydice_array_to_slice((size_t)4U, ret1, uint8_t), uint8_t);
+  memcpy(ret, out, (size_t)8U * sizeof (uint8_t));
+=======
     Eurydice_array_to_subslice_to((size_t)8U,
       &out,
       (size_t)4U,
@@ -43,27 +70,62 @@ Eurydice_arr_c4 const_generics_serialize_3b(Eurydice_slice re)
   lvalue = core_num__u32__to_be_bytes(Eurydice_slice_index(re, (size_t)1U, uint32_t, uint32_t *));
   Eurydice_slice_copy(uu____1, Eurydice_array_to_slice((size_t)4U, &lvalue, uint8_t), uint8_t);
   return out;
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 }
 
 void const_generics_main(void)
 {
+<<<<<<< HEAD
+  uint8_t s[8U];
+  uint32_t buf[2U] = { 1U, 2U };
+  const_generics_serialize__8usize_(Eurydice_array_to_slice((size_t)2U, buf, uint32_t), s);
+  EURYDICE_ASSERT(s[3U] == 1U, "panic!");
+  EURYDICE_ASSERT(s[7U] == 2U, "panic!");
+=======
   /* original Rust expression is not an lvalue in C */
   Eurydice_arr_b2 lvalue = { .data = { 1U, 2U } };
   Eurydice_arr_c4
   s = const_generics_serialize_3b(Eurydice_array_to_slice((size_t)2U, &lvalue, uint32_t));
   EURYDICE_ASSERT(s.data[3U] == 1U, "panic!");
   EURYDICE_ASSERT(s.data[7U] == 2U, "panic!");
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 }
 
-/**
-A monomorphic instance of const_generics.mk_pairs
-with types uint32_t, uint64_t
-with const generics
-- N= 2
-- M= 4
-*/
-const_generics_Pair_4e const_generics_mk_pairs_e0(uint32_t x, uint64_t y)
+const_generics_Pair__u32__u32__2usize__2usize_
+const_generics_mk_pairs__u32__u64__2usize__4usize_(uint32_t x, uint64_t y)
 {
+<<<<<<< HEAD
+  uint32_t a1[2U];
+  KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, a1[i] = x;);
+  uint64_t a2[4U];
+  KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, a2[i] = y;);
+  /* Passing arrays by value in Rust generates a copy in C */
+  uint32_t copy_of_a10[2U];
+  memcpy(copy_of_a10, a1, (size_t)2U * sizeof (uint32_t));
+  /* Passing arrays by value in Rust generates a copy in C */
+  uint64_t copy_of_a20[4U];
+  memcpy(copy_of_a20, a2, (size_t)4U * sizeof (uint64_t));
+  const_generics_Pair__u32__u64__2usize__4usize_ p1;
+  memcpy(p1.left, copy_of_a10, (size_t)2U * sizeof (uint32_t));
+  memcpy(p1.right, copy_of_a20, (size_t)4U * sizeof (uint64_t));
+  /* Passing arrays by value in Rust generates a copy in C */
+  uint64_t copy_of_a2[4U];
+  memcpy(copy_of_a2, a2, (size_t)4U * sizeof (uint64_t));
+  /* Passing arrays by value in Rust generates a copy in C */
+  uint32_t copy_of_a1[2U];
+  memcpy(copy_of_a1, a1, (size_t)2U * sizeof (uint32_t));
+  const_generics_Pair__u64__u32__4usize__2usize_ p2;
+  memcpy(p2.left, copy_of_a2, (size_t)4U * sizeof (uint64_t));
+  memcpy(p2.right, copy_of_a1, (size_t)2U * sizeof (uint32_t));
+  uint32_t uu____4[2U];
+  memcpy(uu____4, p1.left, (size_t)2U * sizeof (uint32_t));
+  uint32_t uu____5[2U];
+  memcpy(uu____5, p2.right, (size_t)2U * sizeof (uint32_t));
+  const_generics_Pair__u32__u32__2usize__2usize_ lit;
+  memcpy(lit.left, uu____4, (size_t)2U * sizeof (uint32_t));
+  memcpy(lit.right, uu____5, (size_t)2U * sizeof (uint32_t));
+  return lit;
+=======
   Eurydice_arr_b2 a1;
   uint32_t repeat_expression0[2U];
   KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, repeat_expression0[i] = x;);
@@ -75,6 +137,7 @@ const_generics_Pair_4e const_generics_mk_pairs_e0(uint32_t x, uint64_t y)
   const_generics_Pair_a5 p1 = { .left = a1, .right = a2 };
   const_generics_Pair_87 p2 = { .left = a2, .right = a1 };
   return (KRML_CLITERAL(const_generics_Pair_4e){ .left = p1.left, .right = p2.right });
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 }
 
 typedef struct _uint32_t__x2_s
@@ -86,9 +149,18 @@ _uint32_t__x2;
 
 void const_generics_main1(void)
 {
+<<<<<<< HEAD
+  const_generics_Pair__u32__u32__2usize__2usize_
+  uu____0 = const_generics_mk_pairs__u32__u64__2usize__4usize_(0U, 0ULL);
+  uint32_t left[2U];
+  memcpy(left, uu____0.left, (size_t)2U * sizeof (uint32_t));
+  uint32_t right[2U];
+  memcpy(right, uu____0.right, (size_t)2U * sizeof (uint32_t));
+=======
   const_generics_Pair_4e uu____0 = const_generics_mk_pairs_e0(0U, 0ULL);
   Eurydice_arr_b2 left = uu____0.left;
   Eurydice_arr_b2 right = uu____0.right;
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
   uint32_t expected = 0U;
   _uint32_t__x2 uu____1 = { .fst = left.data, .snd = &expected };
   EURYDICE_ASSERT(uu____1.fst[0U] == uu____1.snd[0U], "panic!");
@@ -100,13 +172,7 @@ void const_generics_main1(void)
   EURYDICE_ASSERT(uu____4.fst[0U] == uu____4.snd[0U], "panic!");
 }
 
-/**
-A monomorphic instance of const_generics.f
-with const generics
-- FOO= 1
-- BAR= 2
-*/
-bool const_generics_f_e5(uint32_t x, size_t y)
+bool const_generics_f__1usize__2u32_(uint32_t x, size_t y)
 {
   Eurydice_arr_a5 arr1;
   uint32_t repeat_expression0[1U];
@@ -132,13 +198,7 @@ bool const_generics_f_e5(uint32_t x, size_t y)
   return uu____0;
 }
 
-/**
-A monomorphic instance of const_generics.f
-with const generics
-- FOO= 3
-- BAR= 4
-*/
-bool const_generics_f_70(uint32_t x, size_t y)
+bool const_generics_f__3usize__4u32_(uint32_t x, size_t y)
 {
   Eurydice_arr_6f arr1;
   uint32_t repeat_expression0[3U];
@@ -160,16 +220,10 @@ bool const_generics_f_70(uint32_t x, size_t y)
   return uu____0;
 }
 
-/**
-A monomorphic instance of const_generics.g
-with const generics
-- BAR= 3
-- FOO= 4
-*/
-bool const_generics_g_70(uint32_t x, size_t y)
+bool const_generics_g__3usize__4u32_(uint32_t x, size_t y)
 {
   bool uu____0;
-  if (const_generics_f_70(x, y))
+  if (const_generics_f__3usize__4u32_(x, y))
   {
     if (x == 4U)
     {
@@ -197,9 +251,9 @@ _bool__x2;
 void const_generics_main3(void)
 {
   bool x;
-  if (const_generics_f_e5(0U, (size_t)0U))
+  if (const_generics_f__1usize__2u32_(0U, (size_t)0U))
   {
-    x = const_generics_g_70(0U, (size_t)0U);
+    x = const_generics_g__3usize__4u32_(0U, (size_t)0U);
   }
   else
   {
diff --git a/out/test-const_generics/const_generics.h b/out/test-const_generics/const_generics.h
index 953869d3..11be94ce 100644
--- a/out/test-const_generics/const_generics.h
+++ b/out/test-const_generics/const_generics.h
@@ -17,6 +17,9 @@ extern "C" {
 
 static inline Eurydice_arr_e9 core_num__u32__to_be_bytes(uint32_t x0);
 
+<<<<<<< HEAD
+void const_generics_serialize__8usize_(Eurydice_slice re, uint8_t ret[8U]);
+=======
 /**
 A monomorphic instance of const_generics.serialize
 with const generics
@@ -31,29 +34,20 @@ with const generics
 - $2size_t
 */
 typedef struct Eurydice_arr_b2_s { uint32_t data[2U]; } Eurydice_arr_b2;
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 
 void const_generics_main(void);
 
-#define core_panicking_AssertKind_Eq 0
-#define core_panicking_AssertKind_Ne 1
-#define core_panicking_AssertKind_Match 2
-
-typedef uint8_t core_panicking_AssertKind;
-
-/**
-A monomorphic instance of const_generics.Pair
-with types uint32_t, uint32_t
-with const generics
-- $2size_t
-- $2size_t
-*/
-typedef struct const_generics_Pair_4e_s
+typedef struct const_generics_Pair__u32__u32__2usize__2usize__s
 {
   Eurydice_arr_b2 left;
   Eurydice_arr_b2 right;
 }
-const_generics_Pair_4e;
+const_generics_Pair__u32__u32__2usize__2usize_;
 
+<<<<<<< HEAD
+typedef struct const_generics_Pair__u32__u64__2usize__4usize__s
+=======
 /**
 A monomorphic instance of Eurydice.arr
 with types uint64_t
@@ -70,37 +64,30 @@ with const generics
 - $4size_t
 */
 typedef struct const_generics_Pair_a5_s
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 {
   Eurydice_arr_b2 left;
   Eurydice_arr_61 right;
 }
-const_generics_Pair_a5;
+const_generics_Pair__u32__u64__2usize__4usize_;
 
-/**
-A monomorphic instance of const_generics.Pair
-with types uint64_t, uint32_t
-with const generics
-- $4size_t
-- $2size_t
-*/
-typedef struct const_generics_Pair_87_s
+typedef struct const_generics_Pair__u64__u32__4usize__2usize__s
 {
   Eurydice_arr_61 left;
   Eurydice_arr_b2 right;
 }
-const_generics_Pair_87;
+const_generics_Pair__u64__u32__4usize__2usize_;
 
-/**
-A monomorphic instance of const_generics.mk_pairs
-with types uint32_t, uint64_t
-with const generics
-- N= 2
-- M= 4
-*/
-const_generics_Pair_4e const_generics_mk_pairs_e0(uint32_t x, uint64_t y);
+const_generics_Pair__u32__u32__2usize__2usize_
+const_generics_mk_pairs__u32__u64__2usize__4usize_(uint32_t x, uint64_t y);
 
 void const_generics_main1(void);
 
+<<<<<<< HEAD
+bool const_generics_f__1usize__2u32_(uint32_t x, size_t y);
+
+bool const_generics_f__3usize__4u32_(uint32_t x, size_t y);
+=======
 /**
 A monomorphic instance of Eurydice.arr
 with types uint32_t
@@ -148,22 +135,36 @@ with const generics
 - BAR= 4
 */
 bool const_generics_f_70(uint32_t x, size_t y);
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 
-/**
-A monomorphic instance of const_generics.g
-with const generics
-- BAR= 3
-- FOO= 4
-*/
-bool const_generics_g_70(uint32_t x, size_t y);
+bool const_generics_g__3usize__4u32_(uint32_t x, size_t y);
 
 void const_generics_main3(void);
 
-extern uint32_t core_clone_impls__core__clone__Clone_for_u32__clone(uint32_t *x0);
+extern uint32_t core_clone_impls__core__clone__Clone___u32___clone(uint32_t *x0);
+
+extern uint64_t core_clone_impls__core__clone__Clone___u64___clone(uint64_t *x0);
 
-extern uint64_t core_clone_impls__core__clone__Clone_for_u64__clone(uint64_t *x0);
+extern uint8_t core_clone_impls__core__clone__Clone___u8___clone(uint8_t *x0);
 
-extern uint8_t core_clone_impls__core__clone__Clone_for_u8__clone(uint8_t *x0);
+#define core_option_Option_None 0
+#define core_option_Option_Some 1
+
+typedef uint8_t core_option_Option________Slice_u8____tags;
+
+typedef struct core_option_Option________Slice_u8____s
+{
+  core_option_Option________Slice_u8____tags tag;
+  Eurydice_slice f0;
+}
+core_option_Option________Slice_u8___;
+
+typedef struct core_option_Option______mut___Slice_u8____s
+{
+  core_option_Option________Slice_u8____tags tag;
+  Eurydice_slice f0;
+}
+core_option_Option______mut___Slice_u8___;
 
 #if defined(__cplusplus)
 }
diff --git a/out/test-floating_points/floating_points.h b/out/test-floating_points/floating_points.h
index e4d37532..7ad72797 100644
--- a/out/test-floating_points/floating_points.h
+++ b/out/test-floating_points/floating_points.h
@@ -15,6 +15,8 @@
 extern "C" {
 #endif
 
+<<<<<<< HEAD
+=======
 #define core_panicking_AssertKind_Eq 0
 #define core_panicking_AssertKind_Ne 1
 #define core_panicking_AssertKind_Match 2
@@ -37,6 +39,7 @@ with const generics
 */
 typedef struct Eurydice_arr_22_s { float64_t data[100U]; } Eurydice_arr_22;
 
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 void floating_points_main(void);
 
 #if defined(__cplusplus)
diff --git a/out/test-fn_cast/fn_cast.c b/out/test-fn_cast/fn_cast.c
index ae2e0a3f..d0ae5c30 100644
--- a/out/test-fn_cast/fn_cast.c
+++ b/out/test-fn_cast/fn_cast.c
@@ -7,24 +7,14 @@
 
 #include "fn_cast.h"
 
-/**
-A monomorphic instance of fn_cast.applies
-with types int32_t, int32_t
-
-*/
-int32_t *fn_cast_applies_99(int32_t *(*f)(int32_t *x0), int32_t *arg)
+int32_t *fn_cast_id_ref__i32_(int32_t *x)
 {
-  return f(arg);
+  return x;
 }
 
-/**
-A monomorphic instance of fn_cast.id_ref
-with types int32_t
-
-*/
-int32_t *fn_cast_id_ref_a8(int32_t *x)
+int32_t *fn_cast_applies__i32__i32_(int32_t *(*f)(int32_t *x0), int32_t *arg)
 {
-  return x;
+  return f(arg);
 }
 
 typedef struct _int32_t__x2_s
@@ -43,7 +33,7 @@ void fn_cast_main(void)
   _int32_t__x2
   uu____0 =
     {
-      .fst = fn_cast_applies_99((int32_t *(*)(int32_t *x0))fn_cast_id_ref_a8, &lvalue0),
+      .fst = fn_cast_applies__i32__i32_((int32_t *(*)(int32_t *x0))fn_cast_id_ref__i32_, &lvalue0),
       .snd = &lvalue
     };
   EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
diff --git a/out/test-fn_cast/fn_cast.h b/out/test-fn_cast/fn_cast.h
index 1c279f13..610c6375 100644
--- a/out/test-fn_cast/fn_cast.h
+++ b/out/test-fn_cast/fn_cast.h
@@ -15,25 +15,9 @@
 extern "C" {
 #endif
 
-#define core_panicking_AssertKind_Eq 0
-#define core_panicking_AssertKind_Ne 1
-#define core_panicking_AssertKind_Match 2
+int32_t *fn_cast_id_ref__i32_(int32_t *x);
 
-typedef uint8_t core_panicking_AssertKind;
-
-/**
-A monomorphic instance of fn_cast.applies
-with types int32_t, int32_t
-
-*/
-int32_t *fn_cast_applies_99(int32_t *(*f)(int32_t *x0), int32_t *arg);
-
-/**
-A monomorphic instance of fn_cast.id_ref
-with types int32_t
-
-*/
-int32_t *fn_cast_id_ref_a8(int32_t *x);
+int32_t *fn_cast_applies__i32__i32_(int32_t *(*f)(int32_t *x0), int32_t *arg);
 
 void fn_cast_main(void);
 
diff --git a/out/test-fn_higher_order/Eurydice.h b/out/test-fn_higher_order/Eurydice.h
index f3e8dae8..0dfb23bd 100644
--- a/out/test-fn_higher_order/Eurydice.h
+++ b/out/test-fn_higher_order/Eurydice.h
@@ -15,17 +15,12 @@
 extern "C" {
 #endif
 
-/**
-A monomorphic instance of core.ops.range.Range
-with types size_t
-
-*/
-typedef struct core_ops_range_Range_08_s
+typedef struct core_ops_range_Range__usize__s
 {
   size_t start;
   size_t end;
 }
-core_ops_range_Range_08;
+core_ops_range_Range__usize_;
 
 #if defined(__cplusplus)
 }
diff --git a/out/test-fn_higher_order/fn_higher_order.c b/out/test-fn_higher_order/fn_higher_order.c
index f73318ef..f1ff678a 100644
--- a/out/test-fn_higher_order/fn_higher_order.c
+++ b/out/test-fn_higher_order/fn_higher_order.c
@@ -7,11 +7,44 @@
 
 #include "fn_higher_order.h"
 
+#include "Eurydice.h"
+
 int32_t fn_higher_order_empty_ptr(int32_t (*f)(void))
 {
   return f();
 }
 
+<<<<<<< HEAD
+size_t fn_higher_order_sum_lst__5usize_(size_t *lst)
+{
+  size_t sum = (size_t)0U;
+  core_ops_range_Range__usize_
+  iter =
+    core_iter_traits_collect__core__iter__traits__collect__IntoIterator___core__ops__range__Range___usize____into_iter__core__ops__range__Range___usize__((
+        KRML_CLITERAL(core_ops_range_Range__usize_){ .start = (size_t)0U, .end = (size_t)5U }
+      ));
+  while (true)
+  {
+    core_option_Option__usize_
+    uu____0 =
+      core_iter_range__core__iter__traits__iterator__Iterator___core__ops__range__Range___usize____next__usize_(&iter);
+    if (uu____0.tag == core_option_Option_None)
+    {
+      break;
+    }
+    else
+    {
+      size_t i = uu____0.f0;
+      sum = sum + lst[i];
+    }
+  }
+  return sum + (size_t)5U;
+}
+
+size_t fn_higher_order_id__usize_(size_t r)
+{
+  return r;
+=======
 int32_t fn_higher_order_more_sum_lst(Eurydice_arr_8d *l)
 {
   int32_t sum = (int32_t)0;
@@ -22,17 +55,17 @@ int32_t fn_higher_order_more_sum_lst(Eurydice_arr_8d *l)
     size_t i0 = i;
     sum = sum + l->data[i0];);
   return sum;
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 }
 
-/**
-A monomorphic instance of fn_higher_order.compose_cg_apply
-with types size_t, size_t, size_t
-with const generics
-- N= 5
-*/
 size_t
+<<<<<<< HEAD
+fn_higher_order_compose_cg_apply__usize__usize__usize__5usize_(
+  size_t (*f)(size_t *x0),
+=======
 fn_higher_order_compose_cg_apply_fd(
   size_t (*f)(Eurydice_arr_99 *x0),
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
   size_t (*g)(size_t x0),
   Eurydice_arr_99 *arg
 )
@@ -41,6 +74,32 @@ fn_higher_order_compose_cg_apply_fd(
   return uu____0(f(arg));
 }
 
+<<<<<<< HEAD
+int32_t fn_higher_order_more_sum_lst(int32_t *l)
+{
+  int32_t sum = (int32_t)0;
+  core_ops_range_Range__usize_
+  iter =
+    core_iter_traits_collect__core__iter__traits__collect__IntoIterator___core__ops__range__Range___usize____into_iter__core__ops__range__Range___usize__((
+        KRML_CLITERAL(core_ops_range_Range__usize_){ .start = (size_t)0U, .end = (size_t)3U }
+      ));
+  while (true)
+  {
+    core_option_Option__usize_
+    uu____0 =
+      core_iter_range__core__iter__traits__iterator__Iterator___core__ops__range__Range___usize____next__usize_(&iter);
+    if (uu____0.tag == core_option_Option_None)
+    {
+      break;
+    }
+    else
+    {
+      size_t i = uu____0.f0;
+      sum = sum + l[i];
+    }
+  }
+  return sum;
+=======
 /**
 A monomorphic instance of fn_higher_order.sum_lst
 with const generics
@@ -56,27 +115,22 @@ size_t fn_higher_order_sum_lst_c9(Eurydice_arr_99 *lst)
     size_t i0 = i;
     sum = sum + lst->data[i0];);
   return sum + (size_t)5U;
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 }
 
-/**
-A monomorphic instance of fn_higher_order.id
-with types size_t
-
-*/
-size_t fn_higher_order_id_37(size_t r)
+int32_t fn_higher_order_id__i32_(int32_t r)
 {
   return r;
 }
 
-/**
-A monomorphic instance of fn_higher_order.compose_cg_apply
-with types int32_t, int32_t, int32_t
-with const generics
-- N= 3
-*/
 int32_t
+<<<<<<< HEAD
+fn_higher_order_compose_cg_apply__i32__i32__i32__3usize_(
+  int32_t (*f)(int32_t *x0),
+=======
 fn_higher_order_compose_cg_apply_82(
   int32_t (*f)(Eurydice_arr_8d *x0),
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
   int32_t (*g)(int32_t x0),
   Eurydice_arr_8d *arg
 )
@@ -85,16 +139,6 @@ fn_higher_order_compose_cg_apply_82(
   return uu____0(f(arg));
 }
 
-/**
-A monomorphic instance of fn_higher_order.id
-with types int32_t
-
-*/
-int32_t fn_higher_order_id_a8(int32_t r)
-{
-  return r;
-}
-
 typedef struct _size_t__x2_s
 {
   size_t *fst;
@@ -116,6 +160,17 @@ void fn_higher_order_use_compose_cg(void)
   lvalue0 = { .data = { (size_t)1U, (size_t)2U, (size_t)3U, (size_t)4U, (size_t)5U } };
   size_t
   x =
+<<<<<<< HEAD
+    fn_higher_order_compose_cg_apply__usize__usize__usize__5usize_(fn_higher_order_sum_lst__5usize_,
+      fn_higher_order_id__usize_,
+      buf0);
+  int32_t buf[3U] = { (int32_t)10, (int32_t)11, (int32_t)12 };
+  int32_t
+  y =
+    fn_higher_order_compose_cg_apply__i32__i32__i32__3usize_(fn_higher_order_more_sum_lst,
+      fn_higher_order_id__i32_,
+      buf);
+=======
     fn_higher_order_compose_cg_apply_fd(fn_higher_order_sum_lst_c9,
       fn_higher_order_id_37,
       &lvalue0);
@@ -126,6 +181,7 @@ void fn_higher_order_use_compose_cg(void)
     fn_higher_order_compose_cg_apply_82(fn_higher_order_more_sum_lst,
       fn_higher_order_id_a8,
       &lvalue1);
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
   /* original Rust expression is not an lvalue in C */
   size_t lvalue = (size_t)20U;
   _size_t__x2 uu____0 = { .fst = &x, .snd = &lvalue };
diff --git a/out/test-fn_higher_order/fn_higher_order.h b/out/test-fn_higher_order/fn_higher_order.h
index 10338183..21cd014f 100644
--- a/out/test-fn_higher_order/fn_higher_order.h
+++ b/out/test-fn_higher_order/fn_higher_order.h
@@ -15,9 +15,11 @@
 extern "C" {
 #endif
 
-extern int32_t core_clone_impls__core__clone__Clone_for_i32__clone(int32_t *x0);
+#include "Eurydice.h"
 
-extern size_t core_clone_impls__core__clone__Clone_for_usize__clone(size_t *x0);
+extern int32_t core_clone_impls__core__clone__Clone___i32___clone(int32_t *x0);
+
+extern size_t core_clone_impls__core__clone__Clone___usize___clone(size_t *x0);
 
 #define core_cmp_Ordering_Less -1
 #define core_cmp_Ordering_Equal 0
@@ -25,69 +27,68 @@ extern size_t core_clone_impls__core__clone__Clone_for_usize__clone(size_t *x0);
 
 typedef int8_t core_cmp_Ordering;
 
-extern bool core_cmp_impls__core__cmp__PartialEq_usize__for_usize__eq(size_t *x0, size_t *x1);
-
-#define core_option_None 0
-#define core_option_Some 1
+extern bool core_cmp_impls__core__cmp__PartialEq___usize__usize___eq(size_t *x0, size_t *x1);
 
-typedef uint8_t core_option_Option_77_tags;
+#define core_option_Option_None 0
+#define core_option_Option_Some 1
 
-/**
-A monomorphic instance of core.option.Option
-with types core_cmp_Ordering
+typedef uint8_t core_option_Option__core__cmp__Ordering__tags;
 
-*/
-typedef struct core_option_Option_77_s
+typedef struct core_option_Option__core__cmp__Ordering__s
 {
-  core_option_Option_77_tags tag;
+  core_option_Option__core__cmp__Ordering__tags tag;
   core_cmp_Ordering f0;
 }
-core_option_Option_77;
+core_option_Option__core__cmp__Ordering_;
 
-extern core_option_Option_77
-core_cmp_impls__core__cmp__PartialOrd_usize__for_usize__partial_cmp(size_t *x0, size_t *x1);
-
-/**
-A monomorphic instance of core.option.Option
-with types size_t
+extern core_option_Option__core__cmp__Ordering_
+core_cmp_impls__core__cmp__PartialOrd___usize__usize___partial_cmp(size_t *x0, size_t *x1);
 
-*/
-typedef struct core_option_Option_08_s
+typedef struct core_option_Option__usize__s
 {
-  core_option_Option_77_tags tag;
+  core_option_Option__core__cmp__Ordering__tags tag;
   size_t f0;
 }
-core_option_Option_08;
+core_option_Option__usize_;
 
-extern core_option_Option_08
-core_iter_range__core__iter__range__Step_for_usize__backward_checked(size_t x0, size_t x1);
+extern core_option_Option__usize_
+core_iter_range__core__iter__range__Step___usize___backward_checked(size_t x0, size_t x1);
 
-extern core_option_Option_08
-core_iter_range__core__iter__range__Step_for_usize__forward_checked(size_t x0, size_t x1);
+extern core_option_Option__usize_
+core_iter_range__core__iter__range__Step___usize___forward_checked(size_t x0, size_t x1);
 
 /**
 A monomorphic instance of K.
-with types size_t, core_option_Option size_t
+with types size_t, core_option_Option_<usize>
 
 */
-typedef struct tuple_04_s
+typedef struct tuple_f6_s
 {
   size_t fst;
-  core_option_Option_08 snd;
+  core_option_Option__usize_ snd;
 }
-tuple_04;
+tuple_f6;
 
-extern tuple_04
-core_iter_range__core__iter__range__Step_for_usize__steps_between(size_t *x0, size_t *x1);
+extern tuple_f6
+core_iter_range__core__iter__range__Step___usize___steps_between(size_t *x0, size_t *x1);
 
-#define core_panicking_AssertKind_Eq 0
-#define core_panicking_AssertKind_Ne 1
-#define core_panicking_AssertKind_Match 2
+extern core_option_Option__usize_
+core_iter_range__core__iter__traits__iterator__Iterator___core__ops__range__Range___usize____next__usize_(
+  core_ops_range_Range__usize_ *x0
+);
 
-typedef uint8_t core_panicking_AssertKind;
+extern core_ops_range_Range__usize_
+core_iter_traits_collect__core__iter__traits__collect__IntoIterator___core__ops__range__Range___usize____into_iter__core__ops__range__Range___usize__(
+  core_ops_range_Range__usize_ x0
+);
 
 int32_t fn_higher_order_empty_ptr(int32_t (*f)(void));
 
+<<<<<<< HEAD
+size_t fn_higher_order_sum_lst__5usize_(size_t *lst);
+
+size_t fn_higher_order_id__usize_(size_t r);
+=======
 /**
 A monomorphic instance of Eurydice.arr
 with types int32_t
@@ -105,54 +106,45 @@ with const generics
 - $5size_t
 */
 typedef struct Eurydice_arr_99_s { size_t data[5U]; } Eurydice_arr_99;
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 
-/**
-A monomorphic instance of fn_higher_order.compose_cg_apply
-with types size_t, size_t, size_t
-with const generics
-- N= 5
-*/
 size_t
+<<<<<<< HEAD
+fn_higher_order_compose_cg_apply__usize__usize__usize__5usize_(
+  size_t (*f)(size_t *x0),
+=======
 fn_higher_order_compose_cg_apply_fd(
   size_t (*f)(Eurydice_arr_99 *x0),
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
   size_t (*g)(size_t x0),
   Eurydice_arr_99 *arg
 );
 
+<<<<<<< HEAD
+int32_t fn_higher_order_more_sum_lst(int32_t *l);
+=======
 /**
 A monomorphic instance of fn_higher_order.sum_lst
 with const generics
 - N= 5
 */
 size_t fn_higher_order_sum_lst_c9(Eurydice_arr_99 *lst);
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 
-/**
-A monomorphic instance of fn_higher_order.id
-with types size_t
+int32_t fn_higher_order_id__i32_(int32_t r);
 
-*/
-size_t fn_higher_order_id_37(size_t r);
-
-/**
-A monomorphic instance of fn_higher_order.compose_cg_apply
-with types int32_t, int32_t, int32_t
-with const generics
-- N= 3
-*/
 int32_t
+<<<<<<< HEAD
+fn_higher_order_compose_cg_apply__i32__i32__i32__3usize_(
+  int32_t (*f)(int32_t *x0),
+=======
 fn_higher_order_compose_cg_apply_82(
   int32_t (*f)(Eurydice_arr_8d *x0),
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
   int32_t (*g)(int32_t x0),
   Eurydice_arr_8d *arg
 );
 
-/**
-A monomorphic instance of fn_higher_order.id
-with types int32_t
-
-*/
-int32_t fn_higher_order_id_a8(int32_t r);
-
 void fn_higher_order_use_compose_cg(void);
 
 void fn_higher_order_main(void);
diff --git a/out/test-global_ref/global_ref.c b/out/test-global_ref/global_ref.c
index cb475eed..f15ae788 100644
--- a/out/test-global_ref/global_ref.c
+++ b/out/test-global_ref/global_ref.c
@@ -33,7 +33,7 @@ void global_ref_main(void)
   /* original Rust expression is not an lvalue in C */
   void *lvalue = (void *)0U;
   _____x2 uu____0 = { .fst = GLOBAL_REF_C_VAL[0U][0U], .snd = &lvalue };
-  EURYDICE_ASSERT(core_cmp_impls__core__cmp__PartialEq_____for_____eq(uu____0.fst, uu____0.snd),
+  EURYDICE_ASSERT(core_cmp_impls__core__cmp__PartialEq____________eq(uu____0.fst, uu____0.snd),
     "panic!");
   EURYDICE_ASSERT(global_ref_S_VAL[0U][0U][0U] == (int32_t)0, "panic!");
 }
diff --git a/out/test-global_ref/global_ref.h b/out/test-global_ref/global_ref.h
index bf8ca97b..501819b5 100644
--- a/out/test-global_ref/global_ref.h
+++ b/out/test-global_ref/global_ref.h
@@ -15,13 +15,7 @@
 extern "C" {
 #endif
 
-extern bool core_cmp_impls__core__cmp__PartialEq_____for_____eq(void **x0, void **x1);
-
-#define core_panicking_AssertKind_Eq 0
-#define core_panicking_AssertKind_Ne 1
-#define core_panicking_AssertKind_Match 2
-
-typedef uint8_t core_panicking_AssertKind;
+extern bool core_cmp_impls__core__cmp__PartialEq____________eq(void **x0, void **x1);
 
 extern void ***global_ref_C_VAL_local_2;
 
diff --git a/out/test-issue_102/issue_102.h b/out/test-issue_102/issue_102.h
index 7dbe6da1..865afbc3 100644
--- a/out/test-issue_102/issue_102.h
+++ b/out/test-issue_102/issue_102.h
@@ -15,16 +15,6 @@
 extern "C" {
 #endif
 
-#define issue_102_Error1_Reason1 1
-#define issue_102_Error1_Reason2 2
-
-typedef uint8_t issue_102_Error1;
-
-#define issue_102_Error2_Reason1 3
-#define issue_102_Error2_Reason2 4
-
-typedef uint8_t issue_102_Error2;
-
 void issue_102_main(void);
 
 #if defined(__cplusplus)
diff --git a/out/test-issue_104/issue_104.c b/out/test-issue_104/issue_104.c
index e8d321ed..61921ae3 100644
--- a/out/test-issue_104/issue_104.c
+++ b/out/test-issue_104/issue_104.c
@@ -7,20 +7,14 @@
 
 #include "issue_104.h"
 
-/**
-A monomorphic instance of issue_104.sth
-with types issue_104_S
-with const generics
-
-*/
-uint8_t issue_104_sth_50(void)
+uint8_t issue_104_sth__issue_104__S_(void)
 {
-  return ISSUE_104__ISSUE_104__FUN_FOR_ISSUE_104__S__VAL;
+  return ISSUE_104__ISSUE_104__FUN___ISSUE_104__S___VAL;
 }
 
 uint8_t issue_104_call(void)
 {
-  return issue_104_sth_50();
+  return issue_104_sth__issue_104__S_();
 }
 
 typedef struct _uint8_t__x2_s
diff --git a/out/test-issue_104/issue_104.h b/out/test-issue_104/issue_104.h
index f3f507c5..37fcedf9 100644
--- a/out/test-issue_104/issue_104.h
+++ b/out/test-issue_104/issue_104.h
@@ -15,21 +15,9 @@
 extern "C" {
 #endif
 
-#define core_panicking_AssertKind_Eq 0
-#define core_panicking_AssertKind_Ne 1
-#define core_panicking_AssertKind_Match 2
+#define ISSUE_104__ISSUE_104__FUN___ISSUE_104__S___VAL (5U)
 
-typedef uint8_t core_panicking_AssertKind;
-
-#define ISSUE_104__ISSUE_104__FUN_FOR_ISSUE_104__S__VAL (5U)
-
-/**
-A monomorphic instance of issue_104.sth
-with types issue_104_S
-with const generics
-
-*/
-uint8_t issue_104_sth_50(void);
+uint8_t issue_104_sth__issue_104__S_(void);
 
 uint8_t issue_104_call(void);
 
diff --git a/out/test-issue_107/issue_107.c b/out/test-issue_107/issue_107.c
index 995bd6a4..c817568e 100644
--- a/out/test-issue_107/issue_107.c
+++ b/out/test-issue_107/issue_107.c
@@ -12,11 +12,3 @@ void issue_107_main(void)
 
 }
 
-/**
-This function found in impl {issue_107::Fun for issue_107::MyStruct}
-*/
-uint8_t issue_107_f_90(void)
-{
-  return 5U;
-}
-
diff --git a/out/test-issue_107/issue_107.h b/out/test-issue_107/issue_107.h
index 49930ae1..96d38cde 100644
--- a/out/test-issue_107/issue_107.h
+++ b/out/test-issue_107/issue_107.h
@@ -17,11 +17,6 @@ extern "C" {
 
 void issue_107_main(void);
 
-/**
-This function found in impl {issue_107::Fun for issue_107::MyStruct}
-*/
-uint8_t issue_107_f_90(void);
-
 #if defined(__cplusplus)
 }
 #endif
diff --git a/out/test-issue_k630/issue_k630.h b/out/test-issue_k630/issue_k630.h
index 5b4bdfd6..12bf896a 100644
--- a/out/test-issue_k630/issue_k630.h
+++ b/out/test-issue_k630/issue_k630.h
@@ -15,6 +15,8 @@
 extern "C" {
 #endif
 
+<<<<<<< HEAD
+=======
 #define core_panicking_AssertKind_Eq 0
 #define core_panicking_AssertKind_Ne 1
 #define core_panicking_AssertKind_Match 2
@@ -37,6 +39,7 @@ with const generics
 */
 typedef struct Eurydice_arr_10_s { Eurydice_arr_a5 data[5U]; } Eurydice_arr_10;
 
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 void issue_k630_main(void);
 
 #if defined(__cplusplus)
diff --git a/out/test-names/names.h b/out/test-names/names.h
index 90c30b17..f902265a 100644
--- a/out/test-names/names.h
+++ b/out/test-names/names.h
@@ -15,34 +15,6 @@
 extern "C" {
 #endif
 
-#define names_Foo 0
-#define names_Bar 1
-
-typedef uint8_t names_Baz_tags;
-
-typedef struct names_Baz_s
-{
-  names_Baz_tags tag;
-  union {
-    struct
-    {
-      uint32_t f0;
-      uint32_t f1;
-    }
-    case_Foo;
-    uint32_t case_Bar;
-  }
-  val;
-}
-names_Baz;
-
-typedef struct names_Foo0_s
-{
-  uint32_t x;
-  uint32_t y;
-}
-names_Foo0;
-
 void names_main(void);
 
 #if defined(__cplusplus)
diff --git a/out/test-nested_arrays/Eurydice.h b/out/test-nested_arrays/Eurydice.h
index f3e8dae8..0dfb23bd 100644
--- a/out/test-nested_arrays/Eurydice.h
+++ b/out/test-nested_arrays/Eurydice.h
@@ -15,17 +15,12 @@
 extern "C" {
 #endif
 
-/**
-A monomorphic instance of core.ops.range.Range
-with types size_t
-
-*/
-typedef struct core_ops_range_Range_08_s
+typedef struct core_ops_range_Range__usize__s
 {
   size_t start;
   size_t end;
 }
-core_ops_range_Range_08;
+core_ops_range_Range__usize_;
 
 #if defined(__cplusplus)
 }
diff --git a/out/test-nested_arrays/nested_arrays.c b/out/test-nested_arrays/nested_arrays.c
index 74019f68..07804f9a 100644
--- a/out/test-nested_arrays/nested_arrays.c
+++ b/out/test-nested_arrays/nested_arrays.c
@@ -7,6 +7,13 @@
 
 #include "nested_arrays.h"
 
+<<<<<<< HEAD
+#include "Eurydice.h"
+
+const uint32_t nested_arrays_ZERO[8U] = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U };
+
+=======
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 typedef struct _uint32_t__x2_s
 {
   uint32_t *fst;
@@ -29,20 +36,80 @@ void nested_arrays_main(void)
     memcpy(lit.data, repeat_expression, (size_t)3U * sizeof (nested_arrays_Key));
     repeat_expression0[i0] = lit;
   }
+<<<<<<< HEAD
+  core_ops_range_Range__usize_
+  iter0 =
+    core_iter_traits_collect__core__iter__traits__collect__IntoIterator___core__ops__range__Range___usize____into_iter__core__ops__range__Range___usize__((
+        KRML_CLITERAL(core_ops_range_Range__usize_){ .start = (size_t)0U, .end = (size_t)3U }
+      ));
+  while (true)
+=======
   memcpy(keys.data, repeat_expression0, (size_t)3U * sizeof (Eurydice_arr_99));
   for (size_t i0 = (size_t)0U; i0 < (size_t)3U; i0++)
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
   {
-    size_t i1 = i0;
-    for (size_t i2 = (size_t)0U; i2 < (size_t)3U; i2++)
+    core_option_Option__usize_
+    uu____0 =
+      core_iter_range__core__iter__traits__iterator__Iterator___core__ops__range__Range___usize____next__usize_(&iter0);
+    if (uu____0.tag == core_option_Option_None)
+    {
+      break;
+    }
+    else
     {
-      size_t j = i2;
-      for (size_t i = (size_t)0U; i < (size_t)8U; i++)
+      size_t i = uu____0.f0;
+      core_ops_range_Range__usize_
+      iter1 =
+        core_iter_traits_collect__core__iter__traits__collect__IntoIterator___core__ops__range__Range___usize____into_iter__core__ops__range__Range___usize__((
+            KRML_CLITERAL(core_ops_range_Range__usize_){ .start = (size_t)0U, .end = (size_t)3U }
+          ));
+      while (true)
       {
+<<<<<<< HEAD
+        core_option_Option__usize_
+        uu____1 =
+          core_iter_range__core__iter__traits__iterator__Iterator___core__ops__range__Range___usize____next__usize_(&iter1);
+        if (uu____1.tag == core_option_Option_None)
+        {
+          break;
+        }
+        else
+        {
+          size_t j = uu____1.f0;
+          core_ops_range_Range__usize_
+          iter =
+            core_iter_traits_collect__core__iter__traits__collect__IntoIterator___core__ops__range__Range___usize____into_iter__core__ops__range__Range___usize__((
+                KRML_CLITERAL(core_ops_range_Range__usize_){
+                  .start = (size_t)0U,
+                  .end = (size_t)8U
+                }
+              ));
+          while (true)
+          {
+            core_option_Option__usize_
+            uu____2 =
+              core_iter_range__core__iter__traits__iterator__Iterator___core__ops__range__Range___usize____next__usize_(&iter);
+            if (uu____2.tag == core_option_Option_None)
+            {
+              break;
+            }
+            else
+            {
+              size_t k = uu____2.f0;
+              uint32_t actual = keys[i][j][k];
+              uint32_t expected = (uint32_t)k;
+              _uint32_t__x2 uu____3 = { .fst = &actual, .snd = &expected };
+              EURYDICE_ASSERT(uu____3.fst[0U] == uu____3.snd[0U], "panic!");
+            }
+          }
+        }
+=======
         size_t k = i;
         uint32_t actual = keys.data[i1].data[j].data[k];
         uint32_t expected = (uint32_t)k;
         _uint32_t__x2 uu____0 = { .fst = &actual, .snd = &expected };
         EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
       }
     }
   }
diff --git a/out/test-nested_arrays/nested_arrays.h b/out/test-nested_arrays/nested_arrays.h
index e2bb3edf..bbbf89cc 100644
--- a/out/test-nested_arrays/nested_arrays.h
+++ b/out/test-nested_arrays/nested_arrays.h
@@ -15,7 +15,9 @@
 extern "C" {
 #endif
 
-extern size_t core_clone_impls__core__clone__Clone_for_usize__clone(size_t *x0);
+#include "Eurydice.h"
+
+extern size_t core_clone_impls__core__clone__Clone___usize___clone(size_t *x0);
 
 #define core_cmp_Ordering_Less -1
 #define core_cmp_Ordering_Equal 0
@@ -23,68 +25,66 @@ extern size_t core_clone_impls__core__clone__Clone_for_usize__clone(size_t *x0);
 
 typedef int8_t core_cmp_Ordering;
 
-extern bool core_cmp_impls__core__cmp__PartialEq_usize__for_usize__eq(size_t *x0, size_t *x1);
-
-#define core_option_None 0
-#define core_option_Some 1
+extern bool core_cmp_impls__core__cmp__PartialEq___usize__usize___eq(size_t *x0, size_t *x1);
 
-typedef uint8_t core_option_Option_77_tags;
+#define core_option_Option_None 0
+#define core_option_Option_Some 1
 
-/**
-A monomorphic instance of core.option.Option
-with types core_cmp_Ordering
+typedef uint8_t core_option_Option__core__cmp__Ordering__tags;
 
-*/
-typedef struct core_option_Option_77_s
+typedef struct core_option_Option__core__cmp__Ordering__s
 {
-  core_option_Option_77_tags tag;
+  core_option_Option__core__cmp__Ordering__tags tag;
   core_cmp_Ordering f0;
 }
-core_option_Option_77;
-
-extern core_option_Option_77
-core_cmp_impls__core__cmp__PartialOrd_usize__for_usize__partial_cmp(size_t *x0, size_t *x1);
+core_option_Option__core__cmp__Ordering_;
 
-/**
-A monomorphic instance of core.option.Option
-with types size_t
+extern core_option_Option__core__cmp__Ordering_
+core_cmp_impls__core__cmp__PartialOrd___usize__usize___partial_cmp(size_t *x0, size_t *x1);
 
-*/
-typedef struct core_option_Option_08_s
+typedef struct core_option_Option__usize__s
 {
-  core_option_Option_77_tags tag;
+  core_option_Option__core__cmp__Ordering__tags tag;
   size_t f0;
 }
-core_option_Option_08;
+core_option_Option__usize_;
 
-extern core_option_Option_08
-core_iter_range__core__iter__range__Step_for_usize__backward_checked(size_t x0, size_t x1);
+extern core_option_Option__usize_
+core_iter_range__core__iter__range__Step___usize___backward_checked(size_t x0, size_t x1);
 
-extern core_option_Option_08
-core_iter_range__core__iter__range__Step_for_usize__forward_checked(size_t x0, size_t x1);
+extern core_option_Option__usize_
+core_iter_range__core__iter__range__Step___usize___forward_checked(size_t x0, size_t x1);
 
 /**
 A monomorphic instance of K.
-with types size_t, core_option_Option size_t
+with types size_t, core_option_Option_<usize>
 
 */
-typedef struct tuple_04_s
+typedef struct tuple_f6_s
 {
   size_t fst;
-  core_option_Option_08 snd;
+  core_option_Option__usize_ snd;
 }
-tuple_04;
-
-extern tuple_04
-core_iter_range__core__iter__range__Step_for_usize__steps_between(size_t *x0, size_t *x1);
-
-#define core_panicking_AssertKind_Eq 0
-#define core_panicking_AssertKind_Ne 1
-#define core_panicking_AssertKind_Match 2
-
+tuple_f6;
+
+extern tuple_f6
+core_iter_range__core__iter__range__Step___usize___steps_between(size_t *x0, size_t *x1);
+
+extern core_option_Option__usize_
+core_iter_range__core__iter__traits__iterator__Iterator___core__ops__range__Range___usize____next__usize_(
+  core_ops_range_Range__usize_ *x0
+);
+
+<<<<<<< HEAD
+extern core_ops_range_Range__usize_
+core_iter_traits_collect__core__iter__traits__collect__IntoIterator___core__ops__range__Range___usize____into_iter__core__ops__range__Range___usize__(
+  core_ops_range_Range__usize_ x0
+);
+=======
 typedef uint8_t core_panicking_AssertKind;
 
 typedef struct nested_arrays_Key_s { uint32_t data[8U]; } nested_arrays_Key;
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 
 #define NESTED_ARRAYS_ZERO ((KRML_CLITERAL(nested_arrays_Key){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U } }))
 
diff --git a/out/test-partial_eq/partial_eq.c b/out/test-partial_eq/partial_eq.c
index 615ac176..64426882 100644
--- a/out/test-partial_eq/partial_eq.c
+++ b/out/test-partial_eq/partial_eq.c
@@ -10,9 +10,9 @@
 #include "Eurydice.h"
 
 /**
-This function found in impl {core::cmp::PartialEq<partial_eq::Enum> for partial_eq::Enum}
+This function found in impl {core::cmp::PartialEq::<partial_eq::Enum, partial_eq::Enum>}
 */
-inline bool partial_eq_eq_31(partial_eq_Enum *self, partial_eq_Enum *other)
+inline bool partial_eq_eq_aa(partial_eq_Enum *self, partial_eq_Enum *other)
 {
   return true;
 }
@@ -35,22 +35,14 @@ void partial_eq_main(void)
 {
   partial_eq_Enum expected = partial_eq_Enum_A;
   _partial_eq_Enum__x2 uu____0 = { .fst = &expected, .snd = &expected };
-  EURYDICE_ASSERT(partial_eq_eq_31(uu____0.fst, uu____0.snd), "panic!");
+  EURYDICE_ASSERT(partial_eq_eq_aa(uu____0.fst, uu____0.snd), "panic!");
   /* original Rust expression is not an lvalue in C */
   partial_eq_Enum *lvalue0 = &expected;
   /* original Rust expression is not an lvalue in C */
   partial_eq_Enum *lvalue = &expected;
   __partial_eq_Enum___x2 uu____1 = { .fst = &lvalue0, .snd = &lvalue };
-  EURYDICE_ASSERT(partial_eq_eq_31(uu____1.fst[0U], uu____1.snd[0U]), "panic!");
-}
-
-/**
-This function found in impl {core::fmt::Debug for partial_eq::Enum}
-*/
-inline core_result_Result_10 partial_eq_fmt_29(partial_eq_Enum *self, core_fmt_Formatter *f)
-{
-  return
-    core_fmt__core__fmt__Formatter__a___write_str(f,
-      (KRML_CLITERAL(Eurydice_str){ .data = "A", .len = (size_t)1U }));
+  EURYDICE_ASSERT(core_cmp_impls__core__cmp__PartialEq________partial_eq__Enum________partial_eq__Enum____eq__________partial_eq__Enum__partial_eq__Enum_(uu____1.fst,
+      uu____1.snd),
+    "panic!");
 }
 
diff --git a/out/test-partial_eq/partial_eq.h b/out/test-partial_eq/partial_eq.h
index f34e0071..e9efa2fe 100644
--- a/out/test-partial_eq/partial_eq.h
+++ b/out/test-partial_eq/partial_eq.h
@@ -17,36 +17,34 @@ extern "C" {
 
 #include "Eurydice.h"
 
-#define core_result_Ok 0
-#define core_result_Err 1
-
-typedef uint8_t core_result_Result_10;
+#define partial_eq_Enum_A 0
 
-extern core_result_Result_10
-core_fmt__core__fmt__Formatter__a___write_str(core_fmt_Formatter *x0, Eurydice_str x1);
+typedef uint8_t partial_eq_Enum;
 
-#define core_panicking_AssertKind_Eq 0
-#define core_panicking_AssertKind_Ne 1
-#define core_panicking_AssertKind_Match 2
+extern bool
+core_cmp_impls__core__cmp__PartialEq________partial_eq__Enum________partial_eq__Enum____eq__________partial_eq__Enum__partial_eq__Enum_(
+  partial_eq_Enum **x0,
+  partial_eq_Enum **x1
+);
 
-typedef uint8_t core_panicking_AssertKind;
+#define core_result_Result_Ok 0
+#define core_result_Result_Err 1
 
-#define partial_eq_Enum_A 0
+typedef uint8_t core_result_Result______core__fmt__Error_;
 
-typedef uint8_t partial_eq_Enum;
+extern core_result_Result______core__fmt__Error_
+core_fmt__core__fmt__Formatter________write_str_____(
+  core_fmt_Formatter_____ *x0,
+  Eurydice_str x1
+);
 
 /**
-This function found in impl {core::cmp::PartialEq<partial_eq::Enum> for partial_eq::Enum}
+This function found in impl {core::cmp::PartialEq::<partial_eq::Enum, partial_eq::Enum>}
 */
-bool partial_eq_eq_31(partial_eq_Enum *self, partial_eq_Enum *other);
+bool partial_eq_eq_aa(partial_eq_Enum *self, partial_eq_Enum *other);
 
 void partial_eq_main(void);
 
-/**
-This function found in impl {core::fmt::Debug for partial_eq::Enum}
-*/
-core_result_Result_10 partial_eq_fmt_29(partial_eq_Enum *self, core_fmt_Formatter *f);
-
 #if defined(__cplusplus)
 }
 #endif
diff --git a/out/test-raw_pointers/raw_pointers.h b/out/test-raw_pointers/raw_pointers.h
index c15e7ea3..3c2c87a1 100644
--- a/out/test-raw_pointers/raw_pointers.h
+++ b/out/test-raw_pointers/raw_pointers.h
@@ -15,12 +15,6 @@
 extern "C" {
 #endif
 
-#define core_panicking_AssertKind_Eq 0
-#define core_panicking_AssertKind_Ne 1
-#define core_panicking_AssertKind_Match 2
-
-typedef uint8_t core_panicking_AssertKind;
-
 void raw_pointers_main(void);
 
 #if defined(__cplusplus)
diff --git a/out/test-reborrow/reborrow.h b/out/test-reborrow/reborrow.h
index 60d6dd9c..f04921cc 100644
--- a/out/test-reborrow/reborrow.h
+++ b/out/test-reborrow/reborrow.h
@@ -15,12 +15,6 @@
 extern "C" {
 #endif
 
-#define core_panicking_AssertKind_Eq 0
-#define core_panicking_AssertKind_Ne 1
-#define core_panicking_AssertKind_Match 2
-
-typedef uint8_t core_panicking_AssertKind;
-
 void reborrow_main(void);
 
 #if defined(__cplusplus)
diff --git a/out/test-slice_array/slice_array.h b/out/test-slice_array/slice_array.h
index 0266e487..83ce295d 100644
--- a/out/test-slice_array/slice_array.h
+++ b/out/test-slice_array/slice_array.h
@@ -15,6 +15,9 @@
 extern "C" {
 #endif
 
+<<<<<<< HEAD
+typedef struct Eurydice_slice_uint8_t_4size_t__x2_s
+=======
 #define core_panicking_AssertKind_Eq 0
 #define core_panicking_AssertKind_Ne 1
 #define core_panicking_AssertKind_Match 2
@@ -30,6 +33,7 @@ with const generics
 typedef struct Eurydice_arr_11_s { Eurydice_arr_e9 data[4U]; } Eurydice_arr_11;
 
 typedef struct Eurydice_slice_Eurydice_arr_uint8_t___4size_t___x2_s
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 {
   Eurydice_slice fst;
   Eurydice_slice snd;
diff --git a/out/test-trait_generics/trait_generics.c b/out/test-trait_generics/trait_generics.c
index ea179f83..77c5576b 100644
--- a/out/test-trait_generics/trait_generics.c
+++ b/out/test-trait_generics/trait_generics.c
@@ -8,31 +8,20 @@
 #include "trait_generics.h"
 
 /**
-This function found in impl {trait_generics::MyFnOnce for trait_generics::Foo<K>}
+This function found in impl {trait_generics::MyFnOnce::<trait_generics::Foo::<10usize>>}
 */
-/**
-A monomorphic instance of trait_generics.call_once_a3
-with const generics
-- K= 10
-*/
-uint32_t trait_generics_call_once_a3_95(void)
+uint32_t trait_generics_call_once__10usize__29(void)
 {
   return 0U;
 }
 
-/**
-A monomorphic instance of trait_generics.from_fn
-with types trait_generics_Foo[[$10size_t]]
-with const generics
-
-*/
-void trait_generics_from_fn_3c(void)
+void trait_generics_from_fn__trait_generics__Foo___10usize__(void)
 {
-  trait_generics_call_once_a3_95();
+  trait_generics_call_once__10usize__29();
 }
 
 void trait_generics_main(void)
 {
-  trait_generics_from_fn_3c();
+  trait_generics_from_fn__trait_generics__Foo___10usize__();
 }
 
diff --git a/out/test-trait_generics/trait_generics.h b/out/test-trait_generics/trait_generics.h
index ef4b5b53..faefeea7 100644
--- a/out/test-trait_generics/trait_generics.h
+++ b/out/test-trait_generics/trait_generics.h
@@ -16,22 +16,11 @@ extern "C" {
 #endif
 
 /**
-This function found in impl {trait_generics::MyFnOnce for trait_generics::Foo<K>}
+This function found in impl {trait_generics::MyFnOnce::<trait_generics::Foo::<10usize>>}
 */
-/**
-A monomorphic instance of trait_generics.call_once_a3
-with const generics
-- K= 10
-*/
-uint32_t trait_generics_call_once_a3_95(void);
+uint32_t trait_generics_call_once__10usize__29(void);
 
-/**
-A monomorphic instance of trait_generics.from_fn
-with types trait_generics_Foo[[$10size_t]]
-with const generics
-
-*/
-void trait_generics_from_fn_3c(void);
+void trait_generics_from_fn__trait_generics__Foo___10usize__(void);
 
 void trait_generics_main(void);
 
diff --git a/out/test-traits/Eurydice.h b/out/test-traits/Eurydice.h
index f3e8dae8..0dfb23bd 100644
--- a/out/test-traits/Eurydice.h
+++ b/out/test-traits/Eurydice.h
@@ -15,17 +15,12 @@
 extern "C" {
 #endif
 
-/**
-A monomorphic instance of core.ops.range.Range
-with types size_t
-
-*/
-typedef struct core_ops_range_Range_08_s
+typedef struct core_ops_range_Range__usize__s
 {
   size_t start;
   size_t end;
 }
-core_ops_range_Range_08;
+core_ops_range_Range__usize_;
 
 #if defined(__cplusplus)
 }
diff --git a/out/test-traits/traits.c b/out/test-traits/traits.c
index 115d887d..aa719dcc 100644
--- a/out/test-traits/traits.c
+++ b/out/test-traits/traits.c
@@ -10,9 +10,9 @@
 #include "Eurydice.h"
 
 /**
-This function found in impl {traits::ToInt for traits::Foo}
+This function found in impl {traits::ToInt::<traits::Foo>}
 */
-uint32_t traits_to_int_ac(traits_Foo *self)
+uint32_t traits_to_int_32(traits_Foo *self)
 {
   switch (self[0U])
   {
@@ -34,16 +34,16 @@ uint32_t traits_to_int_ac(traits_Foo *self)
 }
 
 /**
-This function found in impl {traits::ToInt for &0 (@Slice<traits::Foo>)}
+This function found in impl {traits::ToInt::<&'_ (@Slice<traits::Foo>)>}
 */
-uint32_t traits_to_int_88(Eurydice_slice *self)
+uint32_t traits_to_int______95(Eurydice_slice *self)
 {
   uint32_t
   uu____0 =
-    traits_to_int_ac(&Eurydice_slice_index(self[0U], (size_t)0U, traits_Foo, traits_Foo *));
+    traits_to_int_32(&Eurydice_slice_index(self[0U], (size_t)0U, traits_Foo, traits_Foo *));
   return
     uu____0 *
-      traits_to_int_ac(&Eurydice_slice_index(self[0U], (size_t)1U, traits_Foo, traits_Foo *));
+      traits_to_int_32(&Eurydice_slice_index(self[0U], (size_t)1U, traits_Foo, traits_Foo *));
 }
 
 void traits_main(void)
@@ -51,8 +51,19 @@ void traits_main(void)
   Eurydice_arr_e2 foos = { .data = { traits_Foo_Foo1, traits_Foo_Foo2 } };
   /* original Rust expression is not an lvalue in C */
   Eurydice_slice
+<<<<<<< HEAD
+  lvalue =
+    Eurydice_array_to_subslice_mono((size_t)2U,
+      foos,
+      (KRML_CLITERAL(core_ops_range_Range__usize_){ .start = (size_t)0U, .end = (size_t)2U }),
+      traits_Foo,
+      core_ops_range_Range__usize_,
+      Eurydice_slice);
+  if (!(traits_to_int______95(&lvalue) != 2U))
+=======
   lvalue = Eurydice_array_to_subslice3(&foos, (size_t)0U, (size_t)2U, traits_Foo *);
   if (!(traits_to_int_88(&lvalue) != 2U))
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
   {
     return;
   }
diff --git a/out/test-traits/traits.h b/out/test-traits/traits.h
index 1bea79d7..d8c3dba5 100644
--- a/out/test-traits/traits.h
+++ b/out/test-traits/traits.h
@@ -15,22 +15,39 @@
 extern "C" {
 #endif
 
-#include "Eurydice.h"
-
 #define traits_Foo_Foo1 0
 #define traits_Foo_Foo2 1
 
 typedef uint8_t traits_Foo;
 
+#define core_option_Option_None 0
+#define core_option_Option_Some 1
+
+typedef uint8_t core_option_Option________Slice_traits__Foo____tags;
+
+typedef struct core_option_Option________Slice_traits__Foo____s
+{
+  core_option_Option________Slice_traits__Foo____tags tag;
+  Eurydice_slice f0;
+}
+core_option_Option________Slice_traits__Foo___;
+
+typedef struct core_option_Option______mut___Slice_traits__Foo____s
+{
+  core_option_Option________Slice_traits__Foo____tags tag;
+  Eurydice_slice f0;
+}
+core_option_Option______mut___Slice_traits__Foo___;
+
 /**
-This function found in impl {traits::ToInt for traits::Foo}
+This function found in impl {traits::ToInt::<traits::Foo>}
 */
-uint32_t traits_to_int_ac(traits_Foo *self);
+uint32_t traits_to_int_32(traits_Foo *self);
 
 /**
-This function found in impl {traits::ToInt for &0 (@Slice<traits::Foo>)}
+This function found in impl {traits::ToInt::<&'_ (@Slice<traits::Foo>)>}
 */
-uint32_t traits_to_int_88(Eurydice_slice *self);
+uint32_t traits_to_int______95(Eurydice_slice *self);
 
 /**
 A monomorphic instance of Eurydice.arr
diff --git a/out/test-traits2/traits2.c b/out/test-traits2/traits2.c
index 9e42a8e0..6e274866 100644
--- a/out/test-traits2/traits2.c
+++ b/out/test-traits2/traits2.c
@@ -7,8 +7,6 @@
 
 #include "traits2.h"
 
-#include "Eurydice.h"
-
 void traits2_main(void)
 {
 
diff --git a/out/test-traits2/traits2.h b/out/test-traits2/traits2.h
index 86011594..ade6c128 100644
--- a/out/test-traits2/traits2.h
+++ b/out/test-traits2/traits2.h
@@ -15,71 +15,6 @@
 extern "C" {
 #endif
 
-#include "Eurydice.h"
-
-extern size_t core_clone_impls__core__clone__Clone_for_usize__clone(size_t *x0);
-
-#define core_cmp_Ordering_Less -1
-#define core_cmp_Ordering_Equal 0
-#define core_cmp_Ordering_Greater 1
-
-typedef int8_t core_cmp_Ordering;
-
-extern bool core_cmp_impls__core__cmp__PartialEq_usize__for_usize__eq(size_t *x0, size_t *x1);
-
-#define core_option_None 0
-#define core_option_Some 1
-
-typedef uint8_t core_option_Option_77_tags;
-
-/**
-A monomorphic instance of core.option.Option
-with types core_cmp_Ordering
-
-*/
-typedef struct core_option_Option_77_s
-{
-  core_option_Option_77_tags tag;
-  core_cmp_Ordering f0;
-}
-core_option_Option_77;
-
-extern core_option_Option_77
-core_cmp_impls__core__cmp__PartialOrd_usize__for_usize__partial_cmp(size_t *x0, size_t *x1);
-
-/**
-A monomorphic instance of core.option.Option
-with types size_t
-
-*/
-typedef struct core_option_Option_08_s
-{
-  core_option_Option_77_tags tag;
-  size_t f0;
-}
-core_option_Option_08;
-
-extern core_option_Option_08
-core_iter_range__core__iter__range__Step_for_usize__backward_checked(size_t x0, size_t x1);
-
-extern core_option_Option_08
-core_iter_range__core__iter__range__Step_for_usize__forward_checked(size_t x0, size_t x1);
-
-/**
-A monomorphic instance of K.
-with types size_t, core_option_Option size_t
-
-*/
-typedef struct tuple_04_s
-{
-  size_t fst;
-  core_option_Option_08 snd;
-}
-tuple_04;
-
-extern tuple_04
-core_iter_range__core__iter__range__Step_for_usize__steps_between(size_t *x0, size_t *x1);
-
 void traits2_main(void);
 
 #if defined(__cplusplus)
diff --git a/out/test-traits3/traits3.c b/out/test-traits3/traits3.c
index 05cc984e..a98fa041 100644
--- a/out/test-traits3/traits3.c
+++ b/out/test-traits3/traits3.c
@@ -7,21 +7,7 @@
 
 #include "traits3.h"
 
-/**
-This function found in impl {traits3::internal::KeccakItem<2usize> for (u64, u64)}
-*/
-uint64_t_x2 traits3_zero_c8(void)
-{
-  return (KRML_CLITERAL(uint64_t_x2){ .fst = 0ULL, .snd = 0ULL });
-}
-
-/**
-A monomorphic instance of traits3.keccak
-with types (uint64_t * uint64_t)
-with const generics
-- N= 2
-*/
-void traits3_keccak_cc(void)
+void traits3_keccak___u64__u64___2usize_(void)
 {
 
 }
diff --git a/out/test-traits3/traits3.h b/out/test-traits3/traits3.h
index 1ab47318..975f3311 100644
--- a/out/test-traits3/traits3.h
+++ b/out/test-traits3/traits3.h
@@ -15,31 +15,18 @@
 extern "C" {
 #endif
 
-typedef struct uint64_t_x2_s
-{
-  uint64_t fst;
-  uint64_t snd;
-}
-uint64_t_x2;
-
-/**
-This function found in impl {traits3::internal::KeccakItem<2usize> for (u64, u64)}
-*/
-uint64_t_x2 traits3_zero_c8(void);
-
-/**
-A monomorphic instance of traits3.keccak
-with types (uint64_t * uint64_t)
-with const generics
-- N= 2
-*/
-void traits3_keccak_cc(void);
+void traits3_keccak___u64__u64___2usize_(void);
 
 void traits3_keccakx2(void);
 
 void traits3_main(void);
 
-typedef uint64_t_x2 traits3_uint64x2_t;
+typedef struct traits3_uint64x2_t_s
+{
+  uint64_t fst;
+  uint64_t snd;
+}
+traits3_uint64x2_t;
 
 #if defined(__cplusplus)
 }
diff --git a/out/test-where_clauses_closures/where_clauses_closures.c b/out/test-where_clauses_closures/where_clauses_closures.c
index 08a58997..8fc2aa40 100644
--- a/out/test-where_clauses_closures/where_clauses_closures.c
+++ b/out/test-where_clauses_closures/where_clauses_closures.c
@@ -8,69 +8,31 @@
 #include "where_clauses_closures.h"
 
 /**
-This function found in impl {where_clauses_closures::Ops<1usize> for usize}
+This function found in impl {where_clauses_closures::Ops::<usize, 1usize>}
 */
-size_t where_clauses_closures_zero_38(void)
+size_t where_clauses_closures_zero_77(void)
 {
   return (size_t)0U;
 }
 
-/**
-This function found in impl {where_clauses_closures::Ops<1usize> for usize}
-*/
-size_t where_clauses_closures_of_usize_38(size_t x)
-{
-  return x;
-}
-
-/**
-This function found in impl {core::ops::function::FnMut<(usize), T> for where_clauses_closures::test::closure<T, K>[TraitClause@0, TraitClause@1, TraitClause@2]}
-*/
-/**
-A monomorphic instance of where_clauses_closures.test.call_mut_1a
-with types size_t
-with const generics
-- K= 1
-*/
-size_t where_clauses_closures_test_call_mut_1a_e3(void **_, size_t tupled_args)
-{
-  size_t i = tupled_args;
-  return where_clauses_closures_of_usize_38(i);
-}
-
-/**
-This function found in impl {core::ops::function::FnOnce<(usize), T> for where_clauses_closures::test::closure<T, K>[TraitClause@0, TraitClause@1, TraitClause@2]}
-*/
-/**
-A monomorphic instance of where_clauses_closures.test.call_once_79
-with types size_t
-with const generics
-- K= 1
-*/
-size_t where_clauses_closures_test_call_once_79_e3(size_t _)
-{
-  /* original Rust expression is not an lvalue in C */
-  void *lvalue = (void *)0U;
-  return where_clauses_closures_test_call_mut_1a_e3(&lvalue, _);
-}
-
-/**
-A monomorphic instance of where_clauses_closures.test
-with types size_t
-with const generics
-- K= 1
-*/
-size_t_x2 where_clauses_closures_test_e3(void)
+size_t_x2 where_clauses_closures_test__usize__1usize_(void)
 {
   Eurydice_arr_e4 arr_struct;
   {
     /* original Rust expression is not an lvalue in C */
     void *lvalue = (void *)0U;
+<<<<<<< HEAD
+    x[0U] = where_clauses_closures_test_call_mut__usize__1usize__8a(&lvalue, (size_t)0U);
+  }
+  size_t y = where_clauses_closures_zero_77();
+  return (KRML_CLITERAL(size_t_x2){ .fst = x[0U], .snd = y });
+=======
     arr_struct.data[0U] = where_clauses_closures_test_call_mut_1a_e3(&lvalue, (size_t)0U);
   }
   Eurydice_arr_e4 x = arr_struct;
   size_t y = where_clauses_closures_zero_38();
   return (KRML_CLITERAL(size_t_x2){ .fst = x.data[0U], .snd = y });
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 }
 
 typedef struct _size_t__x2_s
@@ -82,10 +44,27 @@ _size_t__x2;
 
 void where_clauses_closures_main(void)
 {
-  size_t_x2 uu____0 = where_clauses_closures_test_e3();
+  size_t_x2 uu____0 = where_clauses_closures_test__usize__1usize_();
   size_t x = uu____0.fst;
   size_t y = uu____0.snd;
   _size_t__x2 uu____1 = { .fst = &x, .snd = &y };
   EURYDICE_ASSERT(uu____1.fst[0U] == uu____1.snd[0U], "panic!");
 }
 
+/**
+This function found in impl {where_clauses_closures::Ops::<usize, 1usize>}
+*/
+size_t where_clauses_closures_of_usize_77(size_t x)
+{
+  return x;
+}
+
+/**
+This function found in impl {core::ops::function::FnMut::<where_clauses_closures::test::closure::<usize, 1usize>, (usize)>}
+*/
+size_t where_clauses_closures_test_call_mut__usize__1usize__8a(void **_, size_t tupled_args)
+{
+  size_t i = tupled_args;
+  return where_clauses_closures_of_usize_77(i);
+}
+
diff --git a/out/test-where_clauses_closures/where_clauses_closures.h b/out/test-where_clauses_closures/where_clauses_closures.h
index 6763485f..394defa5 100644
--- a/out/test-where_clauses_closures/where_clauses_closures.h
+++ b/out/test-where_clauses_closures/where_clauses_closures.h
@@ -15,45 +15,12 @@
 extern "C" {
 #endif
 
-extern size_t core_clone_impls__core__clone__Clone_for_usize__clone(size_t *x0);
-
-#define core_panicking_AssertKind_Eq 0
-#define core_panicking_AssertKind_Ne 1
-#define core_panicking_AssertKind_Match 2
-
-typedef uint8_t core_panicking_AssertKind;
-
-/**
-This function found in impl {where_clauses_closures::Ops<1usize> for usize}
-*/
-size_t where_clauses_closures_zero_38(void);
-
-/**
-This function found in impl {where_clauses_closures::Ops<1usize> for usize}
-*/
-size_t where_clauses_closures_of_usize_38(size_t x);
+extern size_t core_clone_impls__core__clone__Clone___usize___clone(size_t *x0);
 
 /**
-This function found in impl {core::ops::function::FnMut<(usize), T> for where_clauses_closures::test::closure<T, K>[TraitClause@0, TraitClause@1, TraitClause@2]}
+This function found in impl {where_clauses_closures::Ops::<usize, 1usize>}
 */
-/**
-A monomorphic instance of where_clauses_closures.test.call_mut_1a
-with types size_t
-with const generics
-- K= 1
-*/
-size_t where_clauses_closures_test_call_mut_1a_e3(void **_, size_t tupled_args);
-
-/**
-This function found in impl {core::ops::function::FnOnce<(usize), T> for where_clauses_closures::test::closure<T, K>[TraitClause@0, TraitClause@1, TraitClause@2]}
-*/
-/**
-A monomorphic instance of where_clauses_closures.test.call_once_79
-with types size_t
-with const generics
-- K= 1
-*/
-size_t where_clauses_closures_test_call_once_79_e3(size_t _);
+size_t where_clauses_closures_zero_77(void);
 
 typedef struct size_t_x2_s
 {
@@ -62,6 +29,9 @@ typedef struct size_t_x2_s
 }
 size_t_x2;
 
+<<<<<<< HEAD
+size_t_x2 where_clauses_closures_test__usize__1usize_(void);
+=======
 /**
 A monomorphic instance of Eurydice.arr
 with types size_t
@@ -77,9 +47,20 @@ with const generics
 - K= 1
 */
 size_t_x2 where_clauses_closures_test_e3(void);
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 
 void where_clauses_closures_main(void);
 
+/**
+This function found in impl {where_clauses_closures::Ops::<usize, 1usize>}
+*/
+size_t where_clauses_closures_of_usize_77(size_t x);
+
+/**
+This function found in impl {core::ops::function::FnMut::<where_clauses_closures::test::closure::<usize, 1usize>, (usize)>}
+*/
+size_t where_clauses_closures_test_call_mut__usize__1usize__8a(void **_, size_t tupled_args);
+
 #if defined(__cplusplus)
 }
 #endif
diff --git a/out/test-where_clauses_simple/where_clauses_simple.c b/out/test-where_clauses_simple/where_clauses_simple.c
index 8d0b0abb..e501f395 100644
--- a/out/test-where_clauses_simple/where_clauses_simple.c
+++ b/out/test-where_clauses_simple/where_clauses_simple.c
@@ -8,41 +8,40 @@
 #include "where_clauses_simple.h"
 
 /**
-This function found in impl {where_clauses_simple::Ops<K> for usize}
+This function found in impl {where_clauses_simple::Ops::<usize, 3usize>}
 */
-/**
-A monomorphic instance of where_clauses_simple.of_u16_81
-with const generics
-- K= 3
-*/
-size_t where_clauses_simple_of_u16_81_e0(uint16_t x)
+size_t where_clauses_simple_of_u16__3usize__ad(uint16_t x)
 {
   return (size_t)x;
 }
 
 /**
-This function found in impl {where_clauses_simple::Ops<K> for usize}
+This function found in impl {where_clauses_simple::Ops::<usize, 3usize>}
 */
+<<<<<<< HEAD
+size_t where_clauses_simple_add__3usize__ad(uint16_t x[3U], size_t y)
+=======
 /**
 A monomorphic instance of where_clauses_simple.add_81
 with const generics
 - K= 3
 */
 size_t where_clauses_simple_add_81_e0(Eurydice_arr_7f x, size_t y)
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 {
   return (size_t)x.data[0U] + y + (size_t)3U;
 }
 
-/**
-A monomorphic instance of where_clauses_simple.fn_k
-with types size_t
-with const generics
-- K= 3
-*/
-size_t where_clauses_simple_fn_k_71(void)
+size_t where_clauses_simple_fn_k__usize__3usize_(void)
 {
+<<<<<<< HEAD
+  size_t x = where_clauses_simple_of_u16__3usize__ad(0U);
+  uint16_t buf[3U] = { 0U };
+  return where_clauses_simple_add__3usize__ad(buf, x);
+=======
   size_t x = where_clauses_simple_of_u16_81_e0(0U);
   return where_clauses_simple_add_81_e0((KRML_CLITERAL(Eurydice_arr_7f){ .data = { 0U } }), x);
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 }
 
 typedef struct _size_t__x2_s
@@ -54,15 +53,18 @@ _size_t__x2;
 
 void where_clauses_simple_k_calls_k(void)
 {
-  size_t r = where_clauses_simple_fn_k_71();
+  size_t r = where_clauses_simple_fn_k__usize__3usize_();
   size_t r_expected = (size_t)3U;
   _size_t__x2 uu____0 = { .fst = &r, .snd = &r_expected };
   EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
 }
 
 /**
-This function found in impl {where_clauses_simple::Ops<1usize> for u64}
+This function found in impl {where_clauses_simple::Ops::<u64, 1usize>}
 */
+<<<<<<< HEAD
+uint64_t where_clauses_simple_of_u16_70(uint16_t x)
+=======
 uint64_t where_clauses_simple_add_19(Eurydice_arr_2e x, uint64_t y)
 {
   return (uint64_t)x.data[0U] + y;
@@ -72,20 +74,31 @@ uint64_t where_clauses_simple_add_19(Eurydice_arr_2e x, uint64_t y)
 This function found in impl {where_clauses_simple::Ops<1usize> for u64}
 */
 uint64_t where_clauses_simple_of_u16_19(uint16_t x)
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 {
   return (uint64_t)x;
 }
 
 /**
-A monomorphic instance of where_clauses_simple.fn_k
-with types uint64_t
-with const generics
-- K= 1
+This function found in impl {where_clauses_simple::Ops::<u64, 1usize>}
 */
+<<<<<<< HEAD
+uint64_t where_clauses_simple_add_70(uint16_t x[1U], uint64_t y)
+{
+  return (uint64_t)x[0U] + y;
+}
+
+uint64_t where_clauses_simple_fn_k__u64__1usize_(void)
+{
+  uint64_t x = where_clauses_simple_of_u16_70(0U);
+  uint16_t buf[1U] = { 0U };
+  return where_clauses_simple_add_70(buf, x);
+=======
 uint64_t where_clauses_simple_fn_k_e4(void)
 {
   uint64_t x = where_clauses_simple_of_u16_19(0U);
   return where_clauses_simple_add_19((KRML_CLITERAL(Eurydice_arr_2e){ .data = { 0U } }), x);
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 }
 
 typedef struct _uint64_t__x2_s
@@ -97,38 +110,48 @@ _uint64_t__x2;
 
 void where_clauses_simple_k_calls_one(void)
 {
+<<<<<<< HEAD
+  uint64_t r = where_clauses_simple_fn_k__u64__1usize_();
+=======
   uint64_t r = where_clauses_simple_fn_k_e4();
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
   uint64_t r_expected = 0ULL;
   _uint64_t__x2 uu____0 = { .fst = &r, .snd = &r_expected };
   EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
 }
 
 /**
-This function found in impl {where_clauses_simple::Ops<K> for usize}
-*/
-/**
-A monomorphic instance of where_clauses_simple.of_u16_81
-with const generics
-- K= 1
+This function found in impl {where_clauses_simple::Ops::<usize, 1usize>}
 */
-size_t where_clauses_simple_of_u16_81_74(uint16_t x)
+size_t where_clauses_simple_of_u16__1usize__ff(uint16_t x)
 {
   return (size_t)x;
 }
 
 /**
-This function found in impl {where_clauses_simple::Ops<K> for usize}
+This function found in impl {where_clauses_simple::Ops::<usize, 1usize>}
 */
+<<<<<<< HEAD
+size_t where_clauses_simple_add__1usize__ff(uint16_t x[1U], size_t y)
+=======
 /**
 A monomorphic instance of where_clauses_simple.add_81
 with const generics
 - K= 1
 */
 size_t where_clauses_simple_add_81_74(Eurydice_arr_2e x, size_t y)
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 {
   return (size_t)x.data[0U] + y + (size_t)1U;
 }
 
+<<<<<<< HEAD
+size_t where_clauses_simple_fn_1__usize_(void)
+{
+  size_t x = where_clauses_simple_of_u16__1usize__ff(0U);
+  uint16_t buf[1U] = { 0U };
+  return where_clauses_simple_add__1usize__ff(buf, x);
+=======
 /**
 A monomorphic instance of where_clauses_simple.fn_1
 with types size_t
@@ -139,16 +162,28 @@ size_t where_clauses_simple_fn_1_a5(void)
 {
   size_t x = where_clauses_simple_of_u16_81_74(0U);
   return where_clauses_simple_add_81_74((KRML_CLITERAL(Eurydice_arr_2e){ .data = { 0U } }), x);
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 }
 
 void where_clauses_simple_one_calls_k(void)
 {
+<<<<<<< HEAD
+  size_t r = where_clauses_simple_fn_1__usize_();
+=======
   size_t r = where_clauses_simple_fn_1_a5();
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
   size_t r_expected = (size_t)1U;
   _size_t__x2 uu____0 = { .fst = &r, .snd = &r_expected };
   EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
 }
 
+<<<<<<< HEAD
+uint64_t where_clauses_simple_fn_1__u64_(void)
+{
+  uint64_t x = where_clauses_simple_of_u16_70(0U);
+  uint16_t buf[1U] = { 0U };
+  return where_clauses_simple_add_70(buf, x);
+=======
 /**
 A monomorphic instance of where_clauses_simple.fn_1
 with types uint64_t
@@ -159,16 +194,31 @@ uint64_t where_clauses_simple_fn_1_e5(void)
 {
   uint64_t x = where_clauses_simple_of_u16_19(0U);
   return where_clauses_simple_add_19((KRML_CLITERAL(Eurydice_arr_2e){ .data = { 0U } }), x);
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 }
 
 void where_clauses_simple_one_calls_one(void)
 {
+<<<<<<< HEAD
+  uint64_t r = where_clauses_simple_fn_1__u64_();
+=======
   uint64_t r = where_clauses_simple_fn_1_e5();
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
   uint64_t r_expected = 0ULL;
   _uint64_t__x2 uu____0 = { .fst = &r, .snd = &r_expected };
   EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
 }
 
+<<<<<<< HEAD
+tuple_65 where_clauses_simple_double__u64__usize_(uint64_t x, size_t y)
+{
+  uint16_t buf0[1U] = { 0U };
+  uint64_t uu____0 = where_clauses_simple_add_70(buf0, x);
+  uint16_t buf[1U] = { 0U };
+  return
+    (
+      KRML_CLITERAL(tuple_65){ .fst = uu____0, .snd = where_clauses_simple_add__1usize__ff(buf, y) }
+=======
 /**
 A monomorphic instance of where_clauses_simple.double
 with types uint64_t, size_t
@@ -185,17 +235,18 @@ tuple_65 where_clauses_simple_double_f1(uint64_t x, size_t y)
         .fst = uu____0,
         .snd = where_clauses_simple_add_81_74((KRML_CLITERAL(Eurydice_arr_2e){ .data = { 0U } }), y)
       }
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
     );
 }
 
-/**
-A monomorphic instance of where_clauses_simple.double_k
-with types size_t, uint64_t
-with const generics
-- K= 3
-*/
-tuple_b6 where_clauses_simple_double_k_7b(size_t x, uint64_t y)
+tuple_b6 where_clauses_simple_double_k__usize__u64__3usize_(size_t x, uint64_t y)
 {
+<<<<<<< HEAD
+  uint16_t buf0[3U] = { 0U };
+  size_t uu____0 = where_clauses_simple_add__3usize__ad(buf0, x);
+  uint16_t buf[1U] = { 0U };
+  return (KRML_CLITERAL(tuple_b6){ .fst = uu____0, .snd = where_clauses_simple_add_70(buf, y) });
+=======
   size_t
   uu____0 = where_clauses_simple_add_81_e0((KRML_CLITERAL(Eurydice_arr_7f){ .data = { 0U } }), x);
   return
@@ -205,6 +256,7 @@ tuple_b6 where_clauses_simple_double_k_7b(size_t x, uint64_t y)
         .snd = where_clauses_simple_add_19((KRML_CLITERAL(Eurydice_arr_2e){ .data = { 0U } }), y)
       }
     );
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 }
 
 void where_clauses_simple_main(void)
@@ -213,8 +265,13 @@ void where_clauses_simple_main(void)
   where_clauses_simple_k_calls_one();
   where_clauses_simple_one_calls_k();
   where_clauses_simple_one_calls_one();
+<<<<<<< HEAD
+  tuple_65 x = where_clauses_simple_double__u64__usize_(1ULL, (size_t)1U);
+  tuple_b6 y = where_clauses_simple_double_k__usize__u64__3usize_((size_t)1U, 1ULL);
+=======
   tuple_65 x = where_clauses_simple_double_f1(1ULL, (size_t)1U);
   tuple_b6 y = where_clauses_simple_double_k_7b((size_t)1U, 1ULL);
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
   uint64_t x_0 = 1ULL;
   size_t x_1 = (size_t)2U;
   _uint64_t__x2 uu____0 = { .fst = &x.fst, .snd = &x_0 };
diff --git a/out/test-where_clauses_simple/where_clauses_simple.h b/out/test-where_clauses_simple/where_clauses_simple.h
index f98de829..3dac237e 100644
--- a/out/test-where_clauses_simple/where_clauses_simple.h
+++ b/out/test-where_clauses_simple/where_clauses_simple.h
@@ -15,31 +15,25 @@
 extern "C" {
 #endif
 
-extern uint64_t core_clone_impls__core__clone__Clone_for_u64__clone(uint64_t *x0);
+extern uint64_t core_clone_impls__core__clone__Clone___u64___clone(uint64_t *x0);
 
-extern size_t core_clone_impls__core__clone__Clone_for_usize__clone(size_t *x0);
+extern size_t core_clone_impls__core__clone__Clone___usize___clone(size_t *x0);
 
-static inline uint64_t core_convert_num__core__convert__From_u16__for_u64__from(uint16_t x0);
+static inline uint64_t core_convert_num__core__convert__From___u64__u16___from(uint16_t x0);
 
-static inline size_t core_convert_num__core__convert__From_u16__for_usize__from(uint16_t x0);
+static inline size_t core_convert_num__core__convert__From___usize__u16___from(uint16_t x0);
 
-#define core_panicking_AssertKind_Eq 0
-#define core_panicking_AssertKind_Ne 1
-#define core_panicking_AssertKind_Match 2
-
-typedef uint8_t core_panicking_AssertKind;
-
-/**
-This function found in impl {where_clauses_simple::Ops<K> for usize}
-*/
 /**
-A monomorphic instance of where_clauses_simple.of_u16_81
-with const generics
-- K= 3
+This function found in impl {where_clauses_simple::Ops::<usize, 3usize>}
 */
-size_t where_clauses_simple_of_u16_81_e0(uint16_t x);
+size_t where_clauses_simple_of_u16__3usize__ad(uint16_t x);
 
 /**
+<<<<<<< HEAD
+This function found in impl {where_clauses_simple::Ops::<usize, 3usize>}
+*/
+size_t where_clauses_simple_add__3usize__ad(uint16_t x[3U], size_t y);
+=======
 A monomorphic instance of Eurydice.arr
 with types uint16_t
 with const generics
@@ -56,18 +50,18 @@ with const generics
 - K= 3
 */
 size_t where_clauses_simple_add_81_e0(Eurydice_arr_7f x, size_t y);
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 
-/**
-A monomorphic instance of where_clauses_simple.fn_k
-with types size_t
-with const generics
-- K= 3
-*/
-size_t where_clauses_simple_fn_k_71(void);
+size_t where_clauses_simple_fn_k__usize__3usize_(void);
 
 void where_clauses_simple_k_calls_k(void);
 
 /**
+<<<<<<< HEAD
+This function found in impl {where_clauses_simple::Ops::<u64, 1usize>}
+*/
+uint64_t where_clauses_simple_of_u16_70(uint16_t x);
+=======
 A monomorphic instance of Eurydice.arr
 with types uint16_t
 with const generics
@@ -79,12 +73,16 @@ typedef struct Eurydice_arr_2e_s { uint16_t data[1U]; } Eurydice_arr_2e;
 This function found in impl {where_clauses_simple::Ops<1usize> for u64}
 */
 uint64_t where_clauses_simple_add_19(Eurydice_arr_2e x, uint64_t y);
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 
 /**
-This function found in impl {where_clauses_simple::Ops<1usize> for u64}
+This function found in impl {where_clauses_simple::Ops::<u64, 1usize>}
 */
-uint64_t where_clauses_simple_of_u16_19(uint16_t x);
+uint64_t where_clauses_simple_add_70(uint16_t x[1U], uint64_t y);
 
+<<<<<<< HEAD
+uint64_t where_clauses_simple_fn_k__u64__1usize_(void);
+=======
 /**
 A monomorphic instance of where_clauses_simple.fn_k
 with types uint64_t
@@ -92,22 +90,27 @@ with const generics
 - K= 1
 */
 uint64_t where_clauses_simple_fn_k_e4(void);
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 
 void where_clauses_simple_k_calls_one(void);
 
 /**
-This function found in impl {where_clauses_simple::Ops<K> for usize}
-*/
-/**
-A monomorphic instance of where_clauses_simple.of_u16_81
-with const generics
-- K= 1
+This function found in impl {where_clauses_simple::Ops::<usize, 1usize>}
 */
-size_t where_clauses_simple_of_u16_81_74(uint16_t x);
+size_t where_clauses_simple_of_u16__1usize__ff(uint16_t x);
 
 /**
-This function found in impl {where_clauses_simple::Ops<K> for usize}
+This function found in impl {where_clauses_simple::Ops::<usize, 1usize>}
 */
+<<<<<<< HEAD
+size_t where_clauses_simple_add__1usize__ff(uint16_t x[1U], size_t y);
+
+size_t where_clauses_simple_fn_1__usize_(void);
+
+void where_clauses_simple_one_calls_k(void);
+
+uint64_t where_clauses_simple_fn_1__u64_(void);
+=======
 /**
 A monomorphic instance of where_clauses_simple.add_81
 with const generics
@@ -132,6 +135,7 @@ with const generics
 
 */
 uint64_t where_clauses_simple_fn_1_e5(void);
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 
 void where_clauses_simple_one_calls_one(void);
 
@@ -147,6 +151,9 @@ typedef struct tuple_65_s
 }
 tuple_65;
 
+<<<<<<< HEAD
+tuple_65 where_clauses_simple_double__u64__usize_(uint64_t x, size_t y);
+=======
 /**
 A monomorphic instance of where_clauses_simple.double
 with types uint64_t, size_t
@@ -154,6 +161,7 @@ with const generics
 
 */
 tuple_65 where_clauses_simple_double_f1(uint64_t x, size_t y);
+>>>>>>> 3d7a1f48969c69a2ca824c933a6b0159a355cef3
 
 /**
 A monomorphic instance of K.
@@ -167,13 +175,7 @@ typedef struct tuple_b6_s
 }
 tuple_b6;
 
-/**
-A monomorphic instance of where_clauses_simple.double_k
-with types size_t, uint64_t
-with const generics
-- K= 3
-*/
-tuple_b6 where_clauses_simple_double_k_7b(size_t x, uint64_t y);
+tuple_b6 where_clauses_simple_double_k__usize__u64__3usize_(size_t x, uint64_t y);
 
 void where_clauses_simple_main(void);
 
diff --git a/test/core_cmp_lib.c b/test/core_cmp_lib.c
index 8c1e9ad2..b8f66018 100644
--- a/test/core_cmp_lib.c
+++ b/test/core_cmp_lib.c
@@ -7,3 +7,8 @@
 bool core_cmp_impls__core__cmp__PartialEq_____for_____eq(void **x0, void **x1) {
   return true;
 }
+
+// same implementation for the monomorphized LLBC
+bool core_cmp_impls__core__cmp__PartialEq____________eq(void **x0, void **x1) {
+  return true;
+}
diff --git a/test/partial_eq_stubs.c b/test/partial_eq_stubs.c
index f4cb168c..1a1b3619 100644
--- a/test/partial_eq_stubs.c
+++ b/test/partial_eq_stubs.c
@@ -1,6 +1,17 @@
 #include "partial_eq.h"
 
-extern core_result_Result_10
-core_fmt__core__fmt__Formatter__a___write_str(core_fmt_Formatter *x0, Eurydice_str x1) {
-  return core_result_Ok;
+extern core_result_Result______core__fmt__Error_
+core_fmt__core__fmt__Formatter________write_str_____(
+  core_fmt_Formatter_____ *x0,
+  Eurydice_str x1
+) {
+  return core_result_Result_Ok;
+}
+
+extern bool
+core_cmp_impls__core__cmp__PartialEq________partial_eq__Enum________partial_eq__Enum____eq__________partial_eq__Enum__partial_eq__Enum_(
+  partial_eq_Enum **x0,
+  partial_eq_Enum **x1
+) {
+  return partial_eq_eq_aa(*x0, *x1);
 }
diff --git a/test/where_clauses_from_fn.c b/test/where_clauses_from_fn.c
new file mode 100644
index 00000000..ac27b77c
--- /dev/null
+++ b/test/where_clauses_from_fn.c
@@ -0,0 +1,5 @@
+#include "where_clauses_closures.h"
+
+extern void core_convert__core__convert__Into___usize__usize___into__usize__usize_(size_t x0[1U]) {
+  x0[0U] = where_clauses_closures_test_call_mut__usize__1usize__8a(NULL, 0U);
+}
\ No newline at end of file