diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
index dab1685c1..8e1000f94 100644
--- a/engine/lib/ast_utils.ml
+++ b/engine/lib/ast_utils.ml
@@ -653,6 +653,11 @@ module Make (F : Features.T) = struct
 
   let make_wild_pat (typ : ty) (span : span) : pat = { p = PWild; span; typ }
 
+  let make_unit_param (span : span) : param =
+    let typ = unit_typ in
+    let pat = make_wild_pat typ span in
+    { pat; typ; typ_span = None; attrs = [] }
+
   let make_seq (e1 : expr) (e2 : expr) : expr =
     make_let (make_wild_pat e1.typ e1.span) e1 e2
 
diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index 8e408632a..faca05316 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -384,6 +384,7 @@ end) : EXPR = struct
                 { f with e = GlobalVar (def_id (AssociatedItem Value) id) }
             | _ -> f
           in
+          let args = if List.is_empty args then [ unit_expr span ] else args in
           App { f; args; generic_args }
       | Box { value } ->
           (U.call Rust_primitives__hax__box_new [ c_expr value ] span typ).e
@@ -616,6 +617,10 @@ end) : EXPR = struct
           let params =
             List.filter_map ~f:(fun p -> Option.map ~f:c_pat p.pat) params
           in
+          let params =
+            if List.is_empty params then [ U.make_wild_pat U.unit_typ span ]
+            else params
+          in
           let body = c_expr body in
           let upvars = List.map ~f:c_expr upvars in
           Closure { body; params; captures = upvars }
@@ -843,7 +848,11 @@ end) : EXPR = struct
     | Float k -> TFloat (match k with F32 -> F32 | F64 -> F64)
     | Arrow value ->
         let ({ inputs; output; _ } : Thir.ty_fn_sig) = value.value in
-        TArrow (List.map ~f:(c_ty span) inputs, c_ty span output)
+        let inputs =
+          if List.is_empty inputs then [ U.unit_typ ]
+          else List.map ~f:(c_ty span) inputs
+        in
+        TArrow (inputs, c_ty span output)
     | Adt { def_id = id; generic_args } ->
         let ident = def_id Type id in
         let args = List.map ~f:(c_generic_value span) generic_args in
@@ -1022,7 +1031,11 @@ end) : EXPR = struct
           | DefaultReturn _span -> unit_typ
           | Return ty -> c_ty span ty
         in
-        TIFn (TArrow (List.map ~f:(c_ty span) inputs, output))
+        let inputs =
+          if List.is_empty inputs then [ U.unit_typ ]
+          else List.map ~f:(c_ty span) inputs
+        in
+        TIFn (TArrow (inputs, output))
     | Type (bounds, None) ->
         let bounds = List.filter_map ~f:(c_predicate_kind span) bounds in
         TIType bounds
@@ -1126,6 +1139,10 @@ and c_item_unwrapped ~ident (item : Thir.item) : item list =
                ty = c_ty item.span ty;
              }
     | Fn (generics, { body; params; _ }) ->
+        let params =
+          if List.is_empty params then [ U.make_unit_param span ]
+          else List.map ~f:(c_param item.span) params
+        in
         mk
         @@ Fn
              {
@@ -1133,7 +1150,7 @@ and c_item_unwrapped ~ident (item : Thir.item) : item list =
                  Concrete_ident.of_def_id Value (Option.value_exn item.def_id);
                generics = c_generics generics;
                body = c_expr body;
-               params = List.map ~f:(c_param item.span) params;
+               params;
              }
     | Enum (variants, generics) ->
         let def_id = Option.value_exn item.def_id in
@@ -1233,12 +1250,16 @@ and c_item_unwrapped ~ident (item : Thir.item) : item list =
             let v =
               match (item.kind : Thir.impl_item_kind) with
               | Fn { body; params; _ } ->
+                  let params =
+                    if List.is_empty params then [ U.make_unit_param span ]
+                    else List.map ~f:(c_param item.span) params
+                  in
                   Fn
                     {
                       name = item_def_id;
                       generics = c_generics generics;
                       body = c_expr body;
-                      params = List.map ~f:(c_param item.span) params;
+                      params;
                     }
               | Const (_ty, e) ->
                   Fn
diff --git a/examples/chacha20/proofs/fstar/extraction/Chacha20.fst b/examples/chacha20/proofs/fstar/extraction/Chacha20.fst
index 311945991..832910bf1 100644
--- a/examples/chacha20/proofs/fstar/extraction/Chacha20.fst
+++ b/examples/chacha20/proofs/fstar/extraction/Chacha20.fst
@@ -138,7 +138,7 @@ let chacha20_key_block0 (key: t_Array u8 (sz 32)) (iv: t_Array u8 (sz 12)) : t_A
 
 let chacha20_update (st0: t_Array u32 (sz 16)) (m: t_Slice u8)
     : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-  let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new in
+  let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new () in
   let num_blocks:usize = (Core.Slice.impl__len m <: usize) /! sz 64 in
   let remainder_len:usize = (Core.Slice.impl__len m <: usize) %! sz 64 in
   let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
diff --git a/examples/limited-order-book/proofs/fstar/extraction/Lob_backend.fst b/examples/limited-order-book/proofs/fstar/extraction/Lob_backend.fst
index 0b58ecf9a..e8ed36ede 100644
--- a/examples/limited-order-book/proofs/fstar/extraction/Lob_backend.fst
+++ b/examples/limited-order-book/proofs/fstar/extraction/Lob_backend.fst
@@ -54,7 +54,7 @@ let process_order
       (other_side: Alloc.Collections.Binary_heap.t_BinaryHeap v_T)
     : (Alloc.Collections.Binary_heap.t_BinaryHeap v_T &
       (Alloc.Vec.t_Vec t_Match Alloc.Alloc.t_Global & Core.Option.t_Option t_Order)) =
-  let matches:Alloc.Vec.t_Vec t_Match Alloc.Alloc.t_Global = Alloc.Vec.impl__new in
+  let matches:Alloc.Vec.t_Vec t_Match Alloc.Alloc.t_Global = Alloc.Vec.impl__new () in
   let done:bool = false in
   let done, matches, order, other_side:(bool & Alloc.Vec.t_Vec t_Match Alloc.Alloc.t_Global &
     t_Order &
@@ -139,7 +139,8 @@ let process_order
             (bool & Alloc.Vec.t_Vec t_Match Alloc.Alloc.t_Global & t_Order &
               Alloc.Collections.Binary_heap.t_BinaryHeap v_T))
   in
-  let output:(Alloc.Vec.t_Vec t_Match Alloc.Alloc.t_Global & Core.Option.t_Option t_Order) =
+  let hax_temp_output:(Alloc.Vec.t_Vec t_Match Alloc.Alloc.t_Global & Core.Option.t_Option t_Order)
+  =
     matches,
     (if order.f_quantity >. 0uL
       then Core.Option.Option_Some order <: Core.Option.t_Option t_Order
@@ -147,7 +148,7 @@ let process_order
     <:
     (Alloc.Vec.t_Vec t_Match Alloc.Alloc.t_Global & Core.Option.t_Option t_Order)
   in
-  other_side, output
+  other_side, hax_temp_output
   <:
   (Alloc.Collections.Binary_heap.t_BinaryHeap v_T &
     (Alloc.Vec.t_Vec t_Match Alloc.Alloc.t_Global & Core.Option.t_Option t_Order))
diff --git a/examples/sha256/proofs/fstar/extraction/Sha256.fst b/examples/sha256/proofs/fstar/extraction/Sha256.fst
index df9f40c24..34b4d9c11 100644
--- a/examples/sha256/proofs/fstar/extraction/Sha256.fst
+++ b/examples/sha256/proofs/fstar/extraction/Sha256.fst
@@ -125,17 +125,33 @@ let shuffle (ws: t_Array u32 (sz 64)) (hashi: t_Array u32 (sz 8)) : t_Array u32
             Core.Num.impl__u32__wrapping_add (sigma a0 (sz 0) (sz 1) <: u32) (maj a0 b0 c0 <: u32)
           in
           let h:t_Array u32 (sz 8) =
-            Rust_primitives.Hax.update_at h (sz 0) (Core.Num.impl__u32__wrapping_add t1 t2 <: u32)
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h
+              (sz 0)
+              (Core.Num.impl__u32__wrapping_add t1 t2 <: u32)
           in
-          let h:t_Array u32 (sz 8) = Rust_primitives.Hax.update_at h (sz 1) a0 in
-          let h:t_Array u32 (sz 8) = Rust_primitives.Hax.update_at h (sz 2) b0 in
-          let h:t_Array u32 (sz 8) = Rust_primitives.Hax.update_at h (sz 3) c0 in
           let h:t_Array u32 (sz 8) =
-            Rust_primitives.Hax.update_at h (sz 4) (Core.Num.impl__u32__wrapping_add d0 t1 <: u32)
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (sz 1) a0
+          in
+          let h:t_Array u32 (sz 8) =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (sz 2) b0
+          in
+          let h:t_Array u32 (sz 8) =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (sz 3) c0
+          in
+          let h:t_Array u32 (sz 8) =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h
+              (sz 4)
+              (Core.Num.impl__u32__wrapping_add d0 t1 <: u32)
+          in
+          let h:t_Array u32 (sz 8) =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (sz 5) e0
+          in
+          let h:t_Array u32 (sz 8) =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (sz 6) f0
+          in
+          let h:t_Array u32 (sz 8) =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (sz 7) g0
           in
-          let h:t_Array u32 (sz 8) = Rust_primitives.Hax.update_at h (sz 5) e0 in
-          let h:t_Array u32 (sz 8) = Rust_primitives.Hax.update_at h (sz 6) f0 in
-          let h:t_Array u32 (sz 8) = Rust_primitives.Hax.update_at h (sz 7) g0 in
           h)
   in
   h
@@ -189,7 +205,9 @@ let schedule (block: t_Array u8 (sz 64)) : t_Array u32 (sz 64) =
           let i:usize = i in
           if i <. sz 16 <: bool
           then
-            let s:t_Array u32 (sz 64) = Rust_primitives.Hax.update_at s i (b.[ i ] <: u32) in
+            let s:t_Array u32 (sz 64) =
+              Rust_primitives.Hax.Monomorphized_update_at.update_at_usize s i (b.[ i ] <: u32)
+            in
             s
           else
             let t16:u32 = s.[ i -! sz 16 <: usize ] in
@@ -199,7 +217,7 @@ let schedule (block: t_Array u8 (sz 64)) : t_Array u32 (sz 64) =
             let s1:u32 = sigma t2 (sz 3) (sz 0) in
             let s0:u32 = sigma t15 (sz 2) (sz 0) in
             let s:t_Array u32 (sz 64) =
-              Rust_primitives.Hax.update_at s
+              Rust_primitives.Hax.Monomorphized_update_at.update_at_usize s
                 i
                 (Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add
                             s1
@@ -233,7 +251,7 @@ let compress (block: t_Array u8 (sz 64)) (h_in: t_Array u32 (sz 8)) : t_Array u3
       (fun h i ->
           let h:t_Array u32 (sz 8) = h in
           let i:usize = i in
-          Rust_primitives.Hax.update_at h
+          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h
             i
             (Core.Num.impl__u32__wrapping_add (h.[ i ] <: u32) (h_in.[ i ] <: u32) <: u32)
           <:
@@ -270,7 +288,7 @@ let u32s_to_be_bytes (state: t_Array u32 (sz 8)) : t_Array u8 (sz 32) =
             (fun out j ->
                 let out:t_Array u8 (sz 32) = out in
                 let j:usize = j in
-                Rust_primitives.Hax.update_at out
+                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out
                   ((i *! sz 4 <: usize) +! j <: usize)
                   (tmp.[ j ] <: u8)
                 <:
@@ -312,7 +330,9 @@ let hash (msg: t_Slice u8) : t_Array u8 (sz 32) =
                 (fun last_block i ->
                     let last_block:t_Array u8 (sz 64) = last_block in
                     let i:usize = i in
-                    Rust_primitives.Hax.update_at last_block i (block.[ i ] <: u8)
+                    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize last_block
+                      i
+                      (block.[ i ] <: u8)
                     <:
                     t_Array u8 (sz 64))
             in
@@ -330,7 +350,7 @@ let hash (msg: t_Slice u8) : t_Array u8 (sz 32) =
             h, last_block, last_block_len <: (t_Array u32 (sz 8) & t_Array u8 (sz 64) & usize))
   in
   let last_block:t_Array u8 (sz 64) =
-    Rust_primitives.Hax.update_at last_block last_block_len 128uy
+    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize last_block last_block_len 128uy
   in
   let len_bist:u64 = cast ((Core.Slice.impl__len msg <: usize) *! sz 8 <: usize) <: u64 in
   let len_bist_bytes:t_Array u8 (sz 8) = Core.Num.impl__u64__to_be_bytes len_bist in
@@ -350,7 +370,7 @@ let hash (msg: t_Slice u8) : t_Array u8 (sz 32) =
           (fun last_block i ->
               let last_block:t_Array u8 (sz 64) = last_block in
               let i:usize = i in
-              Rust_primitives.Hax.update_at last_block
+              Rust_primitives.Hax.Monomorphized_update_at.update_at_usize last_block
                 ((v_BLOCK_SIZE -! v_LEN_SIZE <: usize) +! i <: usize)
                 (len_bist_bytes.[ i ] <: u8)
               <:
@@ -375,7 +395,7 @@ let hash (msg: t_Slice u8) : t_Array u8 (sz 32) =
           (fun pad_block i ->
               let pad_block:t_Array u8 (sz 64) = pad_block in
               let i:usize = i in
-              Rust_primitives.Hax.update_at pad_block
+              Rust_primitives.Hax.Monomorphized_update_at.update_at_usize pad_block
                 ((v_BLOCK_SIZE -! v_LEN_SIZE <: usize) +! i <: usize)
                 (len_bist_bytes.[ i ] <: u8)
               <:
diff --git a/proof-libs/fstar/core/Alloc.Vec.fst b/proof-libs/fstar/core/Alloc.Vec.fst
index ef3dd3301..73c08c75f 100644
--- a/proof-libs/fstar/core/Alloc.Vec.fst
+++ b/proof-libs/fstar/core/Alloc.Vec.fst
@@ -3,12 +3,12 @@ open Rust_primitives
 
 unfold type t_Vec t (_: unit) = s:t_Slice t
 
-let impl__new #t: t_Vec t () = FStar.Seq.empty
+let impl__new #t (): t_Vec t () = FStar.Seq.empty
 
 let impl_2__extend_from_slice #t (self: t_Vec t ()) (other: t_Slice t{Seq.length self + Seq.length other <= max_usize}): t_Vec t ()
   = FStar.Seq.append self other
 
-let impl__with_capacity (_capacity: usize) = impl__new
+let impl__with_capacity (_capacity: usize) = impl__new ()
 
 // TODO: missing precondition For now, `impl_1__push` has a wrong
 // semantics: pushing on a "full" vector does nothing. It should panic
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
new file mode 100644
index 000000000..c64863555
--- /dev/null
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -0,0 +1,57 @@
+---
+source: test-harness/src/harness.rs
+expression: snapshot
+info:
+  kind:
+    Translate:
+      backend: fstar
+  info:
+    name: attributes
+    manifest: attributes/Cargo.toml
+    description: ~
+  spec:
+    optional: false
+    broken: false
+    issue_id: ~
+    positive: true
+    snapshot:
+      stderr: false
+      stdout: true
+---
+exit = 0
+
+[stdout]
+diagnostics = []
+
+[stdout.files]
+"Attributes.fst" = '''
+module Attributes
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let add3_lemma (x: u32)
+    : Lemma Prims.l_True
+      (ensures
+        x <=. 10ul || x >=. (u32_max /! 3ul <: u32) || (add3 x x x <: u32) =. (x *! 3ul <: u32)) =
+  ()
+
+let u32_max: u32 = 90000ul
+
+let add3 (x y z: u32)
+    : Prims.Pure u32
+      (requires x >. 10ul && y >. 10ul && z >. 10ul && ((x +! y <: u32) +! z <: u32) <. u32_max)
+      (ensures
+        fun result ->
+          let result:u32 = result in
+          Hax_lib.implies true
+            (fun temp_0_ ->
+                let _:Prims.unit = temp_0_ in
+                result >. 32ul <: bool)) = (x +! y <: u32) +! z
+
+type t_Foo = {
+  f_x:u32;
+  f_y:f_y: u32{f_y >. 3ul};
+  f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. 3ul}
+}
+'''
diff --git a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap
index 6d179ff1b..673b169ef 100644
--- a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap	
@@ -46,8 +46,8 @@ let array (x: t_Array u8 (sz 10)) : t_Array u8 (sz 10) =
   in
   x
 
-let f: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new in
+let f (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new () in
   let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl_1__push vec 1uy in
   let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl_1__push vec 2uy in
   let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap vec (sz 0) (sz 1) in
@@ -58,7 +58,7 @@ let h (x: u8) : u8 =
   let x:u8 = x +! 10uy in
   x
 
-let build_vec: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+let build_vec (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
   Alloc.Slice.impl__into_vec (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list =
                 [1uy; 2uy; 3uy]
               in
@@ -115,8 +115,8 @@ let index_mutation_unsize (x: t_Array u8 (sz 12)) : u8 =
   in
   42uy
 
-let test_append: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-  let vec1:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new in
+let test_append (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+  let vec1:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new () in
   let vec2:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
     Alloc.Slice.impl__into_vec (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list =
                   [1uy; 2uy; 3uy]
@@ -136,7 +136,7 @@ let test_append: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
   let vec2:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = tmp1 in
   let _:Prims.unit = () in
   let vec1:(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
-    Alloc.Vec.impl_1__append vec1 (build_vec <: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+    Alloc.Vec.impl_1__append vec1 (build_vec () <: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
   in
   vec1
 
diff --git a/test-harness/src/snapshots/toolchain__naming into-coq.snap b/test-harness/src/snapshots/toolchain__naming into-coq.snap
index 6a5a29918..8e9d75e12 100644
--- a/test-harness/src/snapshots/toolchain__naming into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__naming into-coq.snap	
@@ -42,7 +42,7 @@ Definition debug (label : int32) (value : int32) : unit :=
       impl_1__new_display value])))) : unit in
   tt.
 
-Definition f : unit :=
+Definition f (_ : unit) : unit :=
   let a_1 := ((@repr WORDSIZE32 104)) : int32 in
   let a_2 := ((@repr WORDSIZE32 205)) : int32 in
   let a_3 := ((@repr WORDSIZE32 306)) : int32 in
@@ -52,7 +52,7 @@ Definition f : unit :=
   let _ := (debug (@repr WORDSIZE32 1) a_1) : unit in
   debug (@repr WORDSIZE32 4) a.
 
-Definition ff_expand : unit :=
+Definition ff_expand (_ : unit) : unit :=
   let a := ((@repr WORDSIZE32 104)) : int32 in
   let a := ((@repr WORDSIZE32 205)) : int32 in
   let a := ((@repr WORDSIZE32 306)) : int32 in
@@ -70,7 +70,7 @@ Import List.ListNotations.
 Open Scope Z_scope.
 Open Scope bool_scope.
 
-Definition h : unit :=
+Definition h (_ : unit) : unit :=
   tt.
 '''
 "Naming.v" = '''
@@ -127,10 +127,10 @@ Instance t_Foo_t_t_T3_e_for_a : t_T3_e_for_a t_Foo_t := {
 Definition v_INHERENT_CONSTANT : uint_size :=
   (@repr WORDSIZE32 3).
 
-Definition constants : uint_size :=
+Definition constants (_ : unit) : uint_size :=
   f_ASSOCIATED_CONSTANT.+v_INHERENT_CONSTANT.
 
-Definition ff__g : unit :=
+Definition ff__g (_ : unit) : unit :=
   tt.
 
 Record C_f__g__impl__g__Foo_B : Type :={
@@ -203,7 +203,7 @@ Definition f (x : t_Foobar_t) : uint_size :=
 Definition ff__g__impl__g (self : t_B_t) : uint_size :=
   (@repr WORDSIZE32 0).
 
-Definition mk_c : t_C_t :=
+Definition mk_c (_ : unit) : t_C_t :=
   let _ := (Build_Foo_B (@repr WORDSIZE32 3)) : t_Foo_t in
   let _ := (Xt_X_t) : t_X_t in
   Build_C (@repr WORDSIZE32 3).
diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
index 709296796..d13e3d445 100644
--- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
@@ -54,7 +54,7 @@ let debug (label value: u32) : Prims.unit =
   in
   ()
 
-let f: Prims.unit =
+let f (_: Prims.unit) : Prims.unit =
   let a_1_:u32 = 104ul in
   let a_2_:u32 = 205ul in
   let a_3_:u32 = 306ul in
@@ -64,7 +64,7 @@ let f: Prims.unit =
   let _:Prims.unit = debug 1ul a_1_ in
   debug 4ul a
 
-let ff_expand: Prims.unit =
+let ff_expand (_: Prims.unit) : Prims.unit =
   let a:i32 = 104l in
   let a:i32 = 205l in
   let a:i32 = 306l in
@@ -80,7 +80,7 @@ module Naming.F.G.Impl_1.G.Hello
 open Core
 open FStar.Mul
 
-let h: Prims.unit = ()
+let h (_: Prims.unit) : Prims.unit = ()
 '''
 "Naming.fst" = '''
 module Naming
@@ -121,9 +121,10 @@ let constants
       (#v_T: Type)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] ii0: Core.Marker.t_Sized v_T)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] ii1: t_FooTrait v_T)
+      (_: Prims.unit)
     : usize = f_ASSOCIATED_CONSTANT +! v_INHERENT_CONSTANT
 
-let ff__g: Prims.unit = ()
+let ff__g (_: Prims.unit) : Prims.unit = ()
 
 type t_f__g__impl__g__Foo =
   | C_f__g__impl__g__Foo_A : t_f__g__impl__g__Foo
@@ -174,7 +175,7 @@ let f (x: t_Foobar) : usize = ff__g__impl_1__g x.f_a
 
 let ff__g__impl__g (self: t_B) : usize = sz 0
 
-let mk_c: t_C =
+let mk_c (_: Prims.unit) : t_C =
   let _:t_Foo = Foo_B ({ Naming.Foo.f_x = sz 3 }) <: t_Foo in
   let _:t_X = X <: t_X in
   { f_x = sz 3 } <: t_C
diff --git a/test-harness/src/snapshots/toolchain__reordering into-coq.snap b/test-harness/src/snapshots/toolchain__reordering into-coq.snap
index 366b9de66..48829d0aa 100644
--- a/test-harness/src/snapshots/toolchain__reordering into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__reordering into-coq.snap	
@@ -41,16 +41,16 @@ Inductive t_Foo : Type :=
 Definition f (_ : int32) : t_Foo_t :=
   Foo_At_Foo_t.
 
-Definition no_dependency_1_ : unit :=
+Definition no_dependency_1_ (_ : unit) : unit :=
   tt.
 
-Definition no_dependency_2_ : unit :=
+Definition no_dependency_2_ (_ : unit) : unit :=
   tt.
 
 Record t_Bar : Type :={
   0 : t_Foo_t;
 }.
 
-Definition g : t_Bar_t :=
+Definition g (_ : unit) : t_Bar_t :=
   Bar (f (@repr WORDSIZE32 32)).
 '''
diff --git a/test-harness/src/snapshots/toolchain__reordering into-fstar.snap b/test-harness/src/snapshots/toolchain__reordering into-fstar.snap
index a0b540933..ac9e10970 100644
--- a/test-harness/src/snapshots/toolchain__reordering into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__reordering into-fstar.snap	
@@ -36,11 +36,11 @@ type t_Foo =
 
 let f (_: u32) : t_Foo = Foo_A <: t_Foo
 
-let no_dependency_1_: Prims.unit = ()
+let no_dependency_1_ (_: Prims.unit) : Prims.unit = ()
 
-let no_dependency_2_: Prims.unit = ()
+let no_dependency_2_ (_: Prims.unit) : Prims.unit = ()
 
 type t_Bar = | Bar : t_Foo -> t_Bar
 
-let g: t_Bar = Bar (f 32ul) <: t_Bar
+let g (_: Prims.unit) : t_Bar = Bar (f 32ul) <: t_Bar
 '''
diff --git a/tests/Cargo.lock b/tests/Cargo.lock
index b96f861d3..454628b31 100644
--- a/tests/Cargo.lock
+++ b/tests/Cargo.lock
@@ -15,6 +15,7 @@ dependencies = [
 name = "attributes"
 version = "0.1.0"
 dependencies = [
+ "hax-lib",
  "hax-lib-macros",
  "serde",
 ]
@@ -78,6 +79,10 @@ dependencies = [
  "secret_integers",
 ]
 
+[[package]]
+name = "hax-lib"
+version = "0.1.0-pre.1"
+
 [[package]]
 name = "hax-lib-macros"
 version = "0.1.0-pre.1"
diff --git a/tests/attributes/Cargo.toml b/tests/attributes/Cargo.toml
index 121d00f0a..dfe6b8158 100644
--- a/tests/attributes/Cargo.toml
+++ b/tests/attributes/Cargo.toml
@@ -5,7 +5,8 @@ edition = "2021"
 
 [dependencies]
 hax-lib-macros = { path = "../../hax-lib-macros" }
+hax-lib = { path = "../../hax-lib" }
 serde = { version = "1.0", features = ["derive"] }
 
 [package.metadata.hax-tests]
-into."fstar" = { snapshot = "none" }
+into."fstar" = { snapshot = "stdout" }
diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs
index b26e07b53..c069aeaea 100644
--- a/tests/attributes/src/lib.rs
+++ b/tests/attributes/src/lib.rs
@@ -4,7 +4,7 @@ use hax_lib_macros as hax;
 const u32_max: u32 = 90000;
 
 #[hax::requires(x > 10 && y > 10 && z > 10 && x + y + z < u32_max)]
-#[hax::ensures(|result| result > 32)]
+#[hax::ensures(|result| hax_lib::implies(true, || result > 32))]
 fn add3(x: u32, y: u32, z: u32) -> u32 {
     x + y + z
 }