diff --git a/.github/workflows/extract_and_run_coq.yml b/.github/workflows/extract_and_run_coq.yml
index 34f96b605..c4d1c3f61 100644
--- a/.github/workflows/extract_and_run_coq.yml
+++ b/.github/workflows/extract_and_run_coq.yml
@@ -24,6 +24,6 @@ jobs:
       - name: run coq
         working-directory: hax/examples/coverage/proofs/coq/extraction
         run: |
-          sed 's/_impl_f_/_f_/' < Coverage_Test_instance.v > Coverage_Test_instance.v
+          sed 's/_impl_f_/_f_/' < Coverage_Test_instance.v > Coverage_Test_instance.v # TODO: this is a hotfix, should be solved in backend and removed from here.
           nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile"
           nix-shell --packages coq coqPackages.coq-record-update --run "make"
diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml
index ec8327d63..6e33491ed 100644
--- a/engine/backends/coq/coq/coq_backend.ml
+++ b/engine/backends/coq/coq/coq_backend.ml
@@ -119,7 +119,8 @@ let hardcoded_coq_headers =
    (* From Core Require Import Core. *)\n"
 
 let dummy_lib =
-  "Class t_Sized (T : Type) := { }.\n\
+  "(* TODO: Replace this dummy lib with core lib *)\n\
+   Class t_Sized (T : Type) := { }.\n\
    Definition t_u8 := Z.\n\
    Definition t_u16 := Z.\n\
    Definition t_u32 := Z.\n\
@@ -140,7 +141,8 @@ let dummy_lib =
    Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x \
    => x}.\n\
    Definition t_Slice (T : Type) := list T.\n\
-   Definition unsize {T : Type} : list T -> t_Slice T := id.\n"
+   Definition unsize {T : Type} : list T -> t_Slice T := id.\n\
+   (* / dummy lib *)\n"
 
 module BasePrinter = Generic_printer.Make (InputLanguage)
 
@@ -805,7 +807,7 @@ struct
           ^^ string "|}"
         else
           constructor#p
-          ^^ concat_map_with ~pre:space (fun (ident, exp) -> exp#p) fields
+          ^^ concat_map_with ~pre:space (fun (ident, exp) -> parens(exp#p)) fields
 
       method pat'_PConstruct_tuple ~super:_ ~components =
         (* TODO: Only add `'` if you are a top-level pattern *)
diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml
index 7175de961..0a2b4918f 100644
--- a/engine/lib/concrete_ident/concrete_ident.ml
+++ b/engine/lib/concrete_ident/concrete_ident.ml
@@ -560,8 +560,6 @@ let to_debug_string = T.show
 let map_path_strings ~(f : string -> string) (cid : t) : t =
   { cid with def_id = Imported.map_path_strings ~f cid.def_id }
 
-let parent (cid : t) : t = { cid with def_id = Imported.parent cid.def_id }
-
 module DefaultNamePolicy = struct
   let reserved_words = Hash_set.create (module String)
   let index_field_transform = Fn.id
diff --git a/test-harness/src/snapshots/toolchain__assert into-coq.snap b/test-harness/src/snapshots/toolchain__assert into-coq.snap
index a000cc9f9..a44a54125 100644
--- a/test-harness/src/snapshots/toolchain__assert into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__assert into-coq.snap	
@@ -39,11 +39,37 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
+(* From Core Require Import Core. *)
+
+(* TODO: Replace this dummy lib with core lib *)
+Class t_Sized (T : Type) := { }.
+Definition t_u8 := Z.
+Definition t_u16 := Z.
+Definition t_u32 := Z.
+Definition t_u64 := Z.
+Definition t_u128 := Z.
+Definition t_usize := Z.
+Definition t_i8 := Z.
+Definition t_i16 := Z.
+Definition t_i32 := Z.
+Definition t_i64 := Z.
+Definition t_i128 := Z.
+Definition t_isize := Z.
+Definition t_Array T (x : t_usize) := list T.
+Definition t_String := string.
+Definition ToString_f_to_string (x : string) := x.
+Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
+Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
+Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
+Definition t_Slice (T : Type) := list T.
+Definition unsize {T : Type} : list T -> t_Slice T := id.
+(* / dummy lib *)
+
 
 
 (* NotImplementedYet *)
 
-Definition asserts (_ : unit) : unit :=
+Definition asserts '(_ : unit) : unit :=
   let _ := assert (true) in
   let _ := assert (t_PartialEq_f_eq (1) (1)) in
   let _ := match (2,2) with
@@ -56,3 +82,9 @@ Definition asserts (_ : unit) : unit :=
   end in
   tt.
 '''
+_CoqProject = '''
+-R ./ TODO
+-arg -w
+-arg all
+
+Assert.v'''
diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap b/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap
index bfe3bcc0a..1f4ea2056 100644
--- a/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap	
@@ -40,6 +40,32 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
+(* From Core Require Import Core. *)
+
+(* TODO: Replace this dummy lib with core lib *)
+Class t_Sized (T : Type) := { }.
+Definition t_u8 := Z.
+Definition t_u16 := Z.
+Definition t_u32 := Z.
+Definition t_u64 := Z.
+Definition t_u128 := Z.
+Definition t_usize := Z.
+Definition t_i8 := Z.
+Definition t_i16 := Z.
+Definition t_i32 := Z.
+Definition t_i64 := Z.
+Definition t_i128 := Z.
+Definition t_isize := Z.
+Definition t_Array T (x : t_usize) := list T.
+Definition t_String := string.
+Definition ToString_f_to_string (x : string) := x.
+Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
+Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
+Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
+Definition t_Slice (T : Type) := list T.
+Definition unsize {T : Type} : list T -> t_Slice T := id.
+(* / dummy lib *)
+
 
 
 Definition discriminant_EnumWithRepr_ExplicitDiscr1 : t_u16 :=
@@ -53,8 +79,10 @@ Inductive t_EnumWithRepr : Type :=
 | EnumWithRepr_ExplicitDiscr2
 | EnumWithRepr_ImplicitDiscrEmptyTuple
 | EnumWithRepr_ImplicitDiscrEmptyStruct.
-Arguments t_EnumWithRepr:clear implicits.
-Arguments t_EnumWithRepr.
+Arguments EnumWithRepr_ExplicitDiscr1.
+Arguments EnumWithRepr_ExplicitDiscr2.
+Arguments EnumWithRepr_ImplicitDiscrEmptyTuple.
+Arguments EnumWithRepr_ImplicitDiscrEmptyStruct.
 
 Definition t_EnumWithRepr_cast_to_repr (x : t_EnumWithRepr) : t_u16 :=
   match x with
@@ -70,7 +98,7 @@ Definition t_EnumWithRepr_cast_to_repr (x : t_EnumWithRepr) : t_u16 :=
 
 (* NotImplementedYet *)
 
-Definition f (_ : unit) : t_u32 :=
+Definition f '(_ : unit) : t_u32 :=
   let v__x := cast (t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) (0)) in
   t_Add_f_add (cast (t_EnumWithRepr_cast_to_repr (EnumWithRepr_ImplicitDiscrEmptyTuple))) (cast (t_EnumWithRepr_cast_to_repr (EnumWithRepr_ImplicitDiscrEmptyStruct))).
 
@@ -83,3 +111,9 @@ Definition get_casted_repr (x : t_EnumWithRepr) : t_u64 :=
 Definition get_repr (x : t_EnumWithRepr) : t_u16 :=
   t_EnumWithRepr_cast_to_repr (x).
 '''
+_CoqProject = '''
+-R ./ TODO
+-arg -w
+-arg all
+
+Enum_repr.v'''
diff --git a/test-harness/src/snapshots/toolchain__guards into-coq.snap b/test-harness/src/snapshots/toolchain__guards into-coq.snap
index abd2a3274..f229a753e 100644
--- a/test-harness/src/snapshots/toolchain__guards into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__guards into-coq.snap	
@@ -39,6 +39,32 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
+(* From Core Require Import Core. *)
+
+(* TODO: Replace this dummy lib with core lib *)
+Class t_Sized (T : Type) := { }.
+Definition t_u8 := Z.
+Definition t_u16 := Z.
+Definition t_u32 := Z.
+Definition t_u64 := Z.
+Definition t_u128 := Z.
+Definition t_usize := Z.
+Definition t_i8 := Z.
+Definition t_i16 := Z.
+Definition t_i32 := Z.
+Definition t_i64 := Z.
+Definition t_i128 := Z.
+Definition t_isize := Z.
+Definition t_Array T (x : t_usize) := list T.
+Definition t_String := string.
+Definition ToString_f_to_string (x : string) := x.
+Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
+Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
+Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
+Definition t_Slice (T : Type) := list T.
+Definition unsize {T : Type} : list T -> t_Slice T := id.
+(* / dummy lib *)
+
 
 
 (* NotImplementedYet *)
@@ -160,3 +186,9 @@ Definition multiple_guards (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i
     end
   end.
 '''
+_CoqProject = '''
+-R ./ TODO
+-arg -w
+-arg all
+
+Guards.v'''
diff --git a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap
index c86f3b275..2c36a4c47 100644
--- a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap	
@@ -39,21 +39,44 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
+(* From Core Require Import Core. *)
+
+(* TODO: Replace this dummy lib with core lib *)
+Class t_Sized (T : Type) := { }.
+Definition t_u8 := Z.
+Definition t_u16 := Z.
+Definition t_u32 := Z.
+Definition t_u64 := Z.
+Definition t_u128 := Z.
+Definition t_usize := Z.
+Definition t_i8 := Z.
+Definition t_i16 := Z.
+Definition t_i32 := Z.
+Definition t_i64 := Z.
+Definition t_i128 := Z.
+Definition t_isize := Z.
+Definition t_Array T (x : t_usize) := list T.
+Definition t_String := string.
+Definition ToString_f_to_string (x : string) := x.
+Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
+Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
+Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
+Definition t_Slice (T : Type) := list T.
+Definition unsize {T : Type} : list T -> t_Slice T := id.
+(* / dummy lib *)
+
 
 
 Record t_Foo : Type :=
   {
   }.
-Arguments t_Foo:clear implicits.
-Arguments t_Foo.
 Arguments Build_t_Foo.
-#[export] Instance settable_t_Foo : Settable _ :=
-  settable! (@Build_t_Foo) <>.
+#[export]
+Notation "'Foo'" := Build_t_Foo.
 
-Class t_Trait `{v_Self : Type} : Type :=
+Class t_Trait (v_Self : Type) : Type :=
   {
   }.
-Arguments t_Trait:clear implicits.
 Arguments t_Trait (_).
 
 Instance t_Trait_254780795 : t_Trait ((t_Foo)) :=
@@ -62,13 +85,13 @@ Instance t_Trait_254780795 : t_Trait ((t_Foo)) :=
 
 (* NotImplementedYet *)
 
-Definition main_a_a (_ : unit) : unit :=
+Definition main_a_a '(_ : unit) : unit :=
   tt.
 
-Definition main_a_b (_ : unit) : unit :=
+Definition main_a_b '(_ : unit) : unit :=
   tt.
 
-Definition main_a_c (_ : unit) : unit :=
+Definition main_a_c '(_ : unit) : unit :=
   tt.
 
 Definition main_a `{v_T : Type} `{t_Sized (v_T)} `{t_Trait (v_T)} (x : v_T) : unit :=
@@ -77,39 +100,45 @@ Definition main_a `{v_T : Type} `{t_Sized (v_T)} `{t_Trait (v_T)} (x : v_T) : un
   let _ := main_a_c (tt) in
   tt.
 
-Definition main_b_a (_ : unit) : unit :=
+Definition main_b_a '(_ : unit) : unit :=
   tt.
 
-Definition main_b_b (_ : unit) : unit :=
+Definition main_b_b '(_ : unit) : unit :=
   tt.
 
-Definition main_b_c (_ : unit) : unit :=
+Definition main_b_c '(_ : unit) : unit :=
   tt.
 
-Definition main_b (_ : unit) : unit :=
+Definition main_b '(_ : unit) : unit :=
   let _ := main_b_a (tt) in
   let _ := main_b_b (tt) in
   let _ := main_b_c (tt) in
   tt.
 
-Definition main_c_a (_ : unit) : unit :=
+Definition main_c_a '(_ : unit) : unit :=
   tt.
 
-Definition main_c_b (_ : unit) : unit :=
+Definition main_c_b '(_ : unit) : unit :=
   tt.
 
-Definition main_c_c (_ : unit) : unit :=
+Definition main_c_c '(_ : unit) : unit :=
   tt.
 
-Definition main_c (_ : unit) : unit :=
+Definition main_c '(_ : unit) : unit :=
   let _ := main_c_a (tt) in
   let _ := main_c_b (tt) in
   let _ := main_c_c (tt) in
   tt.
 
-Definition main (_ : unit) : unit :=
+Definition main '(_ : unit) : unit :=
   let _ := main_a (Build_t_Foo) in
   let _ := main_b (tt) in
   let _ := main_c (tt) in
   tt.
 '''
+_CoqProject = '''
+-R ./ TODO
+-arg -w
+-arg all
+
+Include_flag.v'''
diff --git a/test-harness/src/snapshots/toolchain__let-else into-coq.snap b/test-harness/src/snapshots/toolchain__let-else into-coq.snap
index 330c601b3..4cd2e8a21 100644
--- a/test-harness/src/snapshots/toolchain__let-else into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__let-else into-coq.snap	
@@ -39,6 +39,32 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
+(* From Core Require Import Core. *)
+
+(* TODO: Replace this dummy lib with core lib *)
+Class t_Sized (T : Type) := { }.
+Definition t_u8 := Z.
+Definition t_u16 := Z.
+Definition t_u32 := Z.
+Definition t_u64 := Z.
+Definition t_u128 := Z.
+Definition t_usize := Z.
+Definition t_i8 := Z.
+Definition t_i16 := Z.
+Definition t_i32 := Z.
+Definition t_i64 := Z.
+Definition t_i128 := Z.
+Definition t_isize := Z.
+Definition t_Array T (x : t_usize) := list T.
+Definition t_String := string.
+Definition ToString_f_to_string (x : string) := x.
+Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
+Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
+Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
+Definition t_Slice (T : Type) := list T.
+Definition unsize {T : Type} : list T -> t_Slice T := id.
+(* / dummy lib *)
+
 
 
 (* NotImplementedYet *)
@@ -60,3 +86,9 @@ Definition let_else_different_type (opt : t_Option ((t_u32))) : bool :=
   end in
   ControlFlow_Continue (let_else (hoist1))).
 '''
+_CoqProject = '''
+-R ./ TODO
+-arg -w
+-arg all
+
+Let_else.v'''
diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap
index 930e617a0..a335feca2 100644
--- a/test-harness/src/snapshots/toolchain__literals into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap	
@@ -40,6 +40,32 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
+(* From Core Require Import Core. *)
+
+(* TODO: Replace this dummy lib with core lib *)
+Class t_Sized (T : Type) := { }.
+Definition t_u8 := Z.
+Definition t_u16 := Z.
+Definition t_u32 := Z.
+Definition t_u64 := Z.
+Definition t_u128 := Z.
+Definition t_usize := Z.
+Definition t_i8 := Z.
+Definition t_i16 := Z.
+Definition t_i32 := Z.
+Definition t_i64 := Z.
+Definition t_i128 := Z.
+Definition t_isize := Z.
+Definition t_Array T (x : t_usize) := list T.
+Definition t_String := string.
+Definition ToString_f_to_string (x : string) := x.
+Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
+Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
+Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
+Definition t_Slice (T : Type) := list T.
+Definition unsize {T : Type} : list T -> t_Slice T := id.
+(* / dummy lib *)
+
 
 
 From Literals Require Import Hax_lib (t_int).
@@ -49,11 +75,10 @@ Record t_Foo : Type :=
   {
     Foo_f_field : t_u8;
   }.
-Arguments t_Foo:clear implicits.
-Arguments t_Foo.
 Arguments Build_t_Foo.
+Arguments Foo_f_field.
 #[export] Instance settable_t_Foo : Settable _ :=
-  settable! (@Build_t_Foo) <Foo_f_field>.
+  settable! (Build_t_Foo) <Foo_f_field>.
 
 (* NotImplementedYet *)
 
@@ -71,7 +96,7 @@ Definition casts (x8 : t_u8) (x16 : t_u16) (x32 : t_u32) (x64 : t_u64) (xs : t_u
   let _ : t_i8 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
   tt.
 
-Definition fn_pointer_cast (_ : unit) : unit :=
+Definition fn_pointer_cast '(_ : unit) : unit :=
   let f : t_u32 -> t_u32 := fun x =>
     x in
   tt.
@@ -100,7 +125,7 @@ Definition math_integers (x : t_Int) `{andb (PartialOrd_f_gt (x) (impl__Int___un
   let _ : t_usize := impl__Int__to_usize (x) in
   impl__Int__to_u8 (Add_f_add (x) (Mul_f_mul (x) (x))).
 
-Definition numeric (_ : unit) : unit :=
+Definition numeric '(_ : unit) : unit :=
   let _ : t_usize := 123 in
   let _ : t_isize := -42 in
   let _ : t_isize := 42 in
@@ -108,7 +133,7 @@ Definition numeric (_ : unit) : unit :=
   let _ : t_u128 := 22222222222222222222 in
   tt.
 
-Definition patterns (_ : unit) : unit :=
+Definition patterns '(_ : unit) : unit :=
   let _ := match 1 with
   | 2 =>
     tt
@@ -122,17 +147,23 @@ Definition patterns (_ : unit) : unit :=
     tt
   end in
   let _ := match Build_t_Foo (4) with
-  | Foo (3) =>
+  | Build_t_Foo (3) =>
     tt
   | _ =>
     tt
   end in
   tt.
 
-Definition panic_with_msg (_ : unit) : unit :=
+Definition panic_with_msg '(_ : unit) : unit :=
   never_to_any (panic_fmt (impl_2__new_const (["with msg"%string]))).
 
-Definition empty_array (_ : unit) : unit :=
+Definition empty_array '(_ : unit) : unit :=
   let _ : t_Slice t_u8 := unsize ([]) in
   tt.
 '''
+_CoqProject = '''
+-R ./ TODO
+-arg -w
+-arg all
+
+Literals.v'''
diff --git a/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap b/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap
index f4b3cbfe0..fe08dfdac 100644
--- a/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap	
@@ -40,13 +40,39 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
+(* From Core Require Import Core. *)
+
+(* TODO: Replace this dummy lib with core lib *)
+Class t_Sized (T : Type) := { }.
+Definition t_u8 := Z.
+Definition t_u16 := Z.
+Definition t_u32 := Z.
+Definition t_u64 := Z.
+Definition t_u128 := Z.
+Definition t_usize := Z.
+Definition t_i8 := Z.
+Definition t_i16 := Z.
+Definition t_i32 := Z.
+Definition t_i64 := Z.
+Definition t_i128 := Z.
+Definition t_isize := Z.
+Definition t_Array T (x : t_usize) := list T.
+Definition t_String := string.
+Definition ToString_f_to_string (x : string) := x.
+Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
+Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
+Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
+Definition t_Slice (T : Type) := list T.
+Definition unsize {T : Type} : list T -> t_Slice T := id.
+(* / dummy lib *)
+
 
 
 Inductive t_E : Type :=
 | E_A
 | E_B.
-Arguments t_E:clear implicits.
-Arguments t_E.
+Arguments E_A.
+Arguments E_B.
 
 Definition t_E_cast_to_repr (x : t_E) : t_isize :=
   match x with
@@ -109,3 +135,9 @@ Definition nested (x : t_Option ((t_i32))) : t_i32 :=
     0
   end.
 '''
+_CoqProject = '''
+-R ./ TODO
+-arg -w
+-arg all
+
+Pattern_or.v'''
diff --git a/test-harness/src/snapshots/toolchain__reordering into-coq.snap b/test-harness/src/snapshots/toolchain__reordering into-coq.snap
index aafff19ec..c83897da7 100644
--- a/test-harness/src/snapshots/toolchain__reordering into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__reordering into-coq.snap	
@@ -39,23 +39,49 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
+(* From Core Require Import Core. *)
+
+(* TODO: Replace this dummy lib with core lib *)
+Class t_Sized (T : Type) := { }.
+Definition t_u8 := Z.
+Definition t_u16 := Z.
+Definition t_u32 := Z.
+Definition t_u64 := Z.
+Definition t_u128 := Z.
+Definition t_usize := Z.
+Definition t_i8 := Z.
+Definition t_i16 := Z.
+Definition t_i32 := Z.
+Definition t_i64 := Z.
+Definition t_i128 := Z.
+Definition t_isize := Z.
+Definition t_Array T (x : t_usize) := list T.
+Definition t_String := string.
+Definition ToString_f_to_string (x : string) := x.
+Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
+Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
+Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
+Definition t_Slice (T : Type) := list T.
+Definition unsize {T : Type} : list T -> t_Slice T := id.
+(* / dummy lib *)
+
 
 
 Inductive t_Foo : Type :=
 | Foo_A
 | Foo_B.
-Arguments t_Foo:clear implicits.
-Arguments t_Foo.
+Arguments Foo_A.
+Arguments Foo_B.
 
 Record t_Bar : Type :=
   {
     Bar_0 : t_Foo;
   }.
-Arguments t_Bar:clear implicits.
-Arguments t_Bar.
 Arguments Build_t_Bar.
+Arguments Bar_0.
 #[export] Instance settable_t_Bar : Settable _ :=
-  settable! (@Build_t_Bar) <Bar_0>.
+  settable! (Build_t_Bar) <Bar_0>.
+Notation "'Bar'" := Build_t_Bar.
 
 Definition t_Foo_cast_to_repr (x : t_Foo) : t_isize :=
   match x with
@@ -67,15 +93,21 @@ Definition t_Foo_cast_to_repr (x : t_Foo) : t_isize :=
 
 (* NotImplementedYet *)
 
-Definition f (_ : t_u32) : t_Foo :=
+Definition f '(_ : t_u32) : t_Foo :=
   Foo_A.
 
-Definition g (_ : unit) : t_Bar :=
+Definition g '(_ : unit) : t_Bar :=
   Build_t_Bar (f (32)).
 
-Definition no_dependency_1_ (_ : unit) : unit :=
+Definition no_dependency_1_ '(_ : unit) : unit :=
   tt.
 
-Definition no_dependency_2_ (_ : unit) : unit :=
+Definition no_dependency_2_ '(_ : unit) : unit :=
   tt.
 '''
+_CoqProject = '''
+-R ./ TODO
+-arg -w
+-arg all
+
+Reordering.v'''
diff --git a/test-harness/src/snapshots/toolchain__slices into-coq.snap b/test-harness/src/snapshots/toolchain__slices into-coq.snap
index 93fa425b0..c755b9ba1 100644
--- a/test-harness/src/snapshots/toolchain__slices into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__slices into-coq.snap	
@@ -40,6 +40,32 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
+(* From Core Require Import Core. *)
+
+(* TODO: Replace this dummy lib with core lib *)
+Class t_Sized (T : Type) := { }.
+Definition t_u8 := Z.
+Definition t_u16 := Z.
+Definition t_u32 := Z.
+Definition t_u64 := Z.
+Definition t_u128 := Z.
+Definition t_usize := Z.
+Definition t_i8 := Z.
+Definition t_i16 := Z.
+Definition t_i32 := Z.
+Definition t_i64 := Z.
+Definition t_i128 := Z.
+Definition t_isize := Z.
+Definition t_Array T (x : t_usize) := list T.
+Definition t_String := string.
+Definition ToString_f_to_string (x : string) := x.
+Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
+Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
+Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
+Definition t_Slice (T : Type) := list T.
+Definition unsize {T : Type} : list T -> t_Slice T := id.
+(* / dummy lib *)
+
 
 
 (* NotImplementedYet *)
@@ -47,12 +73,18 @@ Import RecordSetNotations.
 Definition v_VERSION : t_Slice t_u8 :=
   unsize ([118; 49]).
 
-Definition do_something (_ : t_Slice t_u8) : unit :=
+Definition do_something '(_ : t_Slice t_u8) : unit :=
   tt.
 
-Definition r#unsized (_ : t_Array (t_Slice t_u8) (1)) : unit :=
+Definition r#unsized '(_ : t_Array (t_Slice t_u8) (1)) : unit :=
   tt.
 
 Definition sized (x : t_Array (t_Array (t_u8) (4)) (1)) : unit :=
   r#unsized ([unsize (index (x) (0))]).
 '''
+_CoqProject = '''
+-R ./ TODO
+-arg -w
+-arg all
+
+Slices.v'''