diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index 2ec0f58d8..7866c05c8 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -458,7 +458,7 @@ struct
           |> List.map ~f:(function
                | GConst const -> (pexpr const, F.AST.Nothing)
                | GLifetime _ -> .
-               | GType ty -> (pty e.span ty, F.AST.Hash))
+               | GType ty -> (pty e.span ty, F.AST.Nothing))
         in
         let args = List.map ~f:(pexpr &&& Fn.const F.AST.Nothing) args in
         F.mk_app (pexpr f) (generic_args @ args)
@@ -626,7 +626,7 @@ struct
     type kind = Implicit | Tcresolve | Explicit
     type t = { kind : kind; ident : F.Ident.ident; typ : F.AST.term }
 
-    let of_generic_param ?(kind : kind = Implicit) span (p : generic_param) : t
+    let of_generic_param ?(kind : kind = Explicit) span (p : generic_param) : t
         =
       let ident = plocal_ident p.ident in
       match p.kind with
@@ -641,8 +641,8 @@ struct
           let typ = c_trait_goal span goal in
           { kind = Tcresolve; ident = F.id name; typ }
 
-    let of_generics ?(kind : kind = Implicit) span generics : t list =
-      List.map ~f:(of_generic_param ~kind span) generics.params
+    let of_generics ?(kind : kind = Explicit) span generics : t list =
+      List.map ~f:(of_generic_param ~kind:Explicit span) generics.params
       @ List.mapi ~f:(of_generic_constraint span) generics.constraints
 
     let of_typ span (nth : int) typ : t =
@@ -1166,7 +1166,7 @@ struct
             ~f:(fun i ->
               let name = U.Concrete_ident_view.to_definition_name i.ti_ident in
               let generics =
-                FStarBinder.of_generics ~kind:Implicit i.ti_span i.ti_generics
+                FStarBinder.of_generics ~kind:Explicit i.ti_span i.ti_generics
               in
               let bds = generics |> List.map ~f:FStarBinder.to_binder in
               let fields =
diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
index 3e5e8e8fb..d4868435a 100644
--- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap	
@@ -37,7 +37,7 @@ module Attribute_opaque
 open Core
 open FStar.Mul
 
-val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0
+val t_OpaqueEnum (v_X: usize) (v_T v_U: Type0) : Type0
 
-val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0
+val t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) : Type0
 '''
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index eda0b67cf..a08ea4488 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -62,7 +62,7 @@ let impl__SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex =
   else Core.Option.Option_None <: Core.Option.t_Option t_SafeIndex
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIndex =
+let impl_1 (v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIndex =
   {
     f_Output = v_T;
     f_index_pre = (fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) -> true);
@@ -172,8 +172,8 @@ let t_NoE =
   x:
   Alloc.String.t_String
     { let _, out:(Core.Str.Iter.t_Chars & bool) =
-        Core.Iter.Traits.Iterator.f_any #Core.Str.Iter.t_Chars
-          (Core.Str.impl__str__chars (Core.Ops.Deref.f_deref #Alloc.String.t_String x <: string)
+        Core.Iter.Traits.Iterator.f_any Core.Str.Iter.t_Chars
+          (Core.Str.impl__str__chars (Core.Ops.Deref.f_deref Alloc.String.t_String x <: string)
             <:
             Core.Str.Iter.t_Chars)
           (fun ch ->
@@ -183,8 +183,7 @@ let t_NoE =
       ~.out }
 
 let bounded_u8 (x: t_BoundedU8 12uy 15uy) (y: t_BoundedU8 10uy 11uy) : t_BoundedU8 1uy 23uy =
-  (Hax_lib.f_get #(t_BoundedU8 12uy 15uy) x <: u8) +!
-  (Hax_lib.f_get #(t_BoundedU8 10uy 11uy) y <: u8)
+  (Hax_lib.f_get (t_BoundedU8 12uy 15uy) x <: u8) +! (Hax_lib.f_get (t_BoundedU8 10uy 11uy) y <: u8)
   <:
   t_BoundedU8 1uy 23uy
 
diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
index db8f3cd46..d13b45a4d 100644
--- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
@@ -45,7 +45,7 @@ module Generics
 open Core
 open FStar.Mul
 
-let impl__Bar__inherent_impl_generics (#v_T: Type0) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit =
+let impl__Bar__inherent_impl_generics (v_T: Type0) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit =
   ()
 
 class t_Foo (v_Self: Type0) = {
@@ -63,11 +63,8 @@ let impl_Foo_for_usize: t_Foo usize =
     f_const_add = fun (v_N: usize) (self: usize) -> self +! v_N
   }
 
-let dup
-      (#v_T: Type0)
-      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T)
-      (x: v_T)
-    : (v_T & v_T) = Core.Clone.f_clone #v_T x, Core.Clone.f_clone #v_T x <: (v_T & v_T)
+let dup (v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T) (x: v_T)
+    : (v_T & v_T) = Core.Clone.f_clone v_T x, Core.Clone.f_clone v_T x <: (v_T & v_T)
 
 let f (v_N x: usize) : usize = (v_N +! v_N <: usize) +! x
 
@@ -75,14 +72,14 @@ let call_f (_: Prims.unit) : usize = (f (sz 10) (sz 3) <: usize) +! sz 3
 
 let g
       (v_N: usize)
-      (#v_T: Type0)
+      (v_T: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Convert.t_Into v_T (t_Array usize v_N))
       (arr: v_T)
     : usize =
-  (Core.Option.impl__unwrap_or #usize
-      (Core.Iter.Traits.Iterator.f_max #(Core.Array.Iter.t_IntoIter usize v_N)
-          (Core.Iter.Traits.Collect.f_into_iter #(t_Array usize v_N)
-              (Core.Convert.f_into #v_T #(t_Array usize v_N) arr <: t_Array usize v_N)
+  (Core.Option.impl__unwrap_or usize
+      (Core.Iter.Traits.Iterator.f_max (Core.Array.Iter.t_IntoIter usize v_N)
+          (Core.Iter.Traits.Collect.f_into_iter (t_Array usize v_N)
+              (Core.Convert.f_into v_T (t_Array usize v_N) arr <: t_Array usize v_N)
             <:
             Core.Array.Iter.t_IntoIter usize v_N)
         <:
@@ -94,7 +91,7 @@ let g
 
 let call_g (_: Prims.unit) : usize =
   (g (sz 3)
-      #(t_Array usize (sz 3))
+      (t_Array usize (sz 3))
       (let list = [sz 42; sz 3; sz 49] in
         FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
         Rust_primitives.Hax.array_of_list 3 list)
@@ -105,7 +102,7 @@ let call_g (_: Prims.unit) : usize =
 let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize =
   let acc:usize = v_LEN +! sz 9 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range
             usize)
           ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = v_LEN }
             <:
@@ -122,7 +119,7 @@ let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize =
 
 let repeat
       (v_LEN: usize)
-      (#v_T: Type0)
+      (v_T: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Copy v_T)
       (x: v_T)
     : t_Array v_T v_LEN = Rust_primitives.Hax.repeat x v_LEN
diff --git a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap
index a4ce27894..703ee4730 100644
--- a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap	
@@ -42,7 +42,7 @@ let main_a_b (_: Prims.unit) : Prims.unit = ()
 let main_a_c (_: Prims.unit) : Prims.unit = ()
 
 /// Direct dependencies
-let main_a (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait v_T) (x: v_T)
+let main_a (v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait v_T) (x: v_T)
     : Prims.unit =
   let _:Prims.unit = main_a_a () in
   let _:Prims.unit = main_a_b () in
@@ -80,7 +80,7 @@ let impl_Trait_for_Foo: t_Trait t_Foo = { __marker_trait = () }
 
 /// Entrypoint
 let main (_: Prims.unit) : Prims.unit =
-  let _:Prims.unit = main_a #t_Foo (Foo <: t_Foo) in
+  let _:Prims.unit = main_a t_Foo (Foo <: t_Foo) in
   let _:Prims.unit = main_b () in
   let _:Prims.unit = main_c () in
   ()
diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap
index 169518fc5..17a373143 100644
--- a/test-harness/src/snapshots/toolchain__loops into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__loops into-fstar.snap	
@@ -40,14 +40,14 @@ let bool_returning (x: u8) : bool = x <. 10uy
 let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   let acc:usize = sz 0 in
   let chunks:Core.Slice.Iter.t_ChunksExact usize =
-    Core.Slice.impl__chunks_exact #usize
-      (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice usize)
+    Core.Slice.impl__chunks_exact usize
+      (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice usize)
       v_CHUNK_LEN
   in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_ChunksExact
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.Iter.t_ChunksExact
             usize)
-          (Core.Clone.f_clone #(Core.Slice.Iter.t_ChunksExact usize) chunks
+          (Core.Clone.f_clone (Core.Slice.Iter.t_ChunksExact usize) chunks
             <:
             Core.Slice.Iter.t_ChunksExact usize)
         <:
@@ -58,7 +58,7 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global
           let chunk:t_Slice usize = chunk in
           let mean:usize = sz 0 in
           let mean:usize =
-            Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(t_Slice usize)
+            Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (t_Slice usize)
                   chunk
                 <:
                 Core.Slice.Iter.t_Iter usize)
@@ -72,8 +72,8 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global
           acc)
   in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(t_Slice usize)
-          (Core.Slice.Iter.impl_87__remainder #usize chunks <: t_Slice usize)
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (t_Slice usize)
+          (Core.Slice.Iter.impl_87__remainder usize chunks <: t_Slice usize)
         <:
         Core.Slice.Iter.t_Iter usize)
       acc
@@ -87,10 +87,10 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global
 let composed_range (n: usize) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Chain.t_Chain
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Chain.t_Chain
               (Core.Ops.Range.t_Range usize) (Core.Ops.Range.t_Range usize))
-          (Core.Iter.Traits.Iterator.f_chain #(Core.Ops.Range.t_Range usize)
-              #(Core.Ops.Range.t_Range usize)
+          (Core.Iter.Traits.Iterator.f_chain (Core.Ops.Range.t_Range usize)
+              (Core.Ops.Range.t_Range usize)
               ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n }
                 <:
                 Core.Ops.Range.t_Range usize)
@@ -117,11 +117,11 @@ let composed_range (n: usize) : usize =
 let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Enumerate.t_Enumerate
             (Core.Slice.Iter.t_Chunks usize))
-          (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Chunks usize)
-              (Core.Slice.impl__chunks #usize
-                  (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
+          (Core.Iter.Traits.Iterator.f_enumerate (Core.Slice.Iter.t_Chunks usize)
+              (Core.Slice.impl__chunks usize
+                  (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
                     <:
                     t_Slice usize)
                   (sz 4)
@@ -135,10 +135,10 @@ let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
       (fun acc temp_1_ ->
           let acc:usize = acc in
           let i, chunk:(usize & t_Slice usize) = temp_1_ in
-          Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate
+          Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Enumerate.t_Enumerate
                   (Core.Slice.Iter.t_Iter usize))
-                (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Iter usize)
-                    (Core.Slice.impl__iter #usize chunk <: Core.Slice.Iter.t_Iter usize)
+                (Core.Iter.Traits.Iterator.f_enumerate (Core.Slice.Iter.t_Iter usize)
+                    (Core.Slice.impl__iter usize chunk <: Core.Slice.Iter.t_Iter usize)
                   <:
                   Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Iter usize))
               <:
@@ -155,8 +155,7 @@ let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
 
 let f (_: Prims.unit) : u8 =
   let acc:u8 = 0uy in
-  Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range u8
-        )
+  Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range u8)
         ({ Core.Ops.Range.f_start = 1uy; Core.Ops.Range.f_end = 10uy } <: Core.Ops.Range.t_Range u8)
       <:
       Core.Ops.Range.t_Range u8)
@@ -171,10 +170,10 @@ let f (_: Prims.unit) : u8 =
 let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_Iter
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.Iter.t_Iter
             usize)
-          (Core.Slice.impl__iter #usize
-              (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
+          (Core.Slice.impl__iter usize
+              (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
                 <:
                 t_Slice usize)
             <:
@@ -192,10 +191,10 @@ let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
 let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_Iter
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.Iter.t_Iter
             usize)
-          (Core.Slice.impl__iter #usize
-              (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
+          (Core.Slice.impl__iter usize
+              (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
                 <:
                 t_Slice usize)
             <:
@@ -206,9 +205,9 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
       (fun acc item ->
           let acc:usize = acc in
           let item:usize = item in
-          Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev
+          Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Rev.t_Rev
                   (Core.Ops.Range.t_Range usize))
-                (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize)
+                (Core.Iter.Traits.Iterator.f_rev (Core.Ops.Range.t_Range usize)
                     ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = item }
                       <:
                       Core.Ops.Range.t_Range usize)
@@ -221,12 +220,12 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
                 let acc:usize = acc in
                 let i:usize = i in
                 let acc:usize = acc +! sz 1 in
-                Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Zip.t_Zip
+                Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Zip.t_Zip
                           (Core.Slice.Iter.t_Iter usize) (Core.Ops.Range.t_Range usize))
-                      (Core.Iter.Traits.Iterator.f_zip #(Core.Slice.Iter.t_Iter usize)
-                          #(Core.Ops.Range.t_Range usize)
-                          (Core.Slice.impl__iter #usize
-                              (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global)
+                      (Core.Iter.Traits.Iterator.f_zip (Core.Slice.Iter.t_Iter usize)
+                          (Core.Ops.Range.t_Range usize)
+                          (Core.Slice.impl__iter usize
+                              (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global)
                                   arr
                                 <:
                                 t_Slice usize)
@@ -254,7 +253,7 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
 let pattern (arr: Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Alloc.Vec.t_Vec
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Alloc.Vec.t_Vec
               (usize & usize) Alloc.Alloc.t_Global)
           arr
         <:
@@ -270,7 +269,7 @@ let pattern (arr: Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) : usize
 let range1 (_: Prims.unit) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range
             usize)
           ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 15 }
             <:
@@ -288,7 +287,7 @@ let range1 (_: Prims.unit) : usize =
 let range2 (n: usize) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range
             usize)
           ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n +! sz 10 <: usize }
             <:
@@ -306,9 +305,9 @@ let range2 (n: usize) : usize =
 let rev_range (n: usize) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Rev.t_Rev
             (Core.Ops.Range.t_Range usize))
-          (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize)
+          (Core.Iter.Traits.Iterator.f_rev (Core.Ops.Range.t_Range usize)
               ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n }
                 <:
                 Core.Ops.Range.t_Range usize)
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 76f5002cd..a17972835 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	
@@ -45,15 +45,15 @@ let array (x: t_Array u8 (sz 10)) : t_Array u8 (sz 10) =
   x
 
 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 #u8 () in
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new u8 () in
   let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-    Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 1uy
+    Alloc.Vec.impl_1__push u8 Alloc.Alloc.t_Global vec 1uy
   in
   let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-    Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 2uy
+    Alloc.Vec.impl_1__push u8 Alloc.Alloc.t_Global vec 2uy
   in
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap u8 vec (sz 0) (sz 1) in
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap u8 vec (sz 0) (sz 1) in
   vec
 
 let h (x: u8) : u8 =
@@ -83,8 +83,8 @@ let k
   (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64)
 
 let build_vec (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-  Alloc.Slice.impl__into_vec #u8
-    #Alloc.Alloc.t_Global
+  Alloc.Slice.impl__into_vec u8
+    Alloc.Alloc.t_Global
     (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list = [1uy; 2uy; 3uy] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
               Rust_primitives.Hax.array_of_list 3 list)
@@ -95,8 +95,8 @@ let build_vec (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
 
 let index_mutation (x: Core.Ops.Range.t_Range usize) (a: t_Slice u8) : Prims.unit =
   let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-    Alloc.Slice.impl__into_vec #u8
-      #Alloc.Alloc.t_Global
+    Alloc.Slice.impl__into_vec u8
+      Alloc.Alloc.t_Global
       (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list = [1uy] in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                 Rust_primitives.Hax.array_of_list 1 list)
@@ -108,7 +108,7 @@ let index_mutation (x: Core.Ops.Range.t_Range usize) (a: t_Slice u8) : Prims.uni
   let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
     Rust_primitives.Hax.Monomorphized_update_at.update_at_range v
       x
-      (Core.Slice.impl__copy_from_slice #u8 (v.[ x ] <: t_Slice u8) a <: t_Slice u8)
+      (Core.Slice.impl__copy_from_slice u8 (v.[ x ] <: t_Slice u8) a <: t_Slice u8)
   in
   let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
     Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v (sz 1) 3uy
@@ -121,7 +121,7 @@ let index_mutation_unsize (x: t_Array u8 (sz 12)) : u8 =
       ({ Core.Ops.Range.f_start = sz 4; Core.Ops.Range.f_end = sz 5 }
         <:
         Core.Ops.Range.t_Range usize)
-      (Core.Slice.impl__copy_from_slice #u8
+      (Core.Slice.impl__copy_from_slice u8
           (x.[ { Core.Ops.Range.f_start = sz 4; Core.Ops.Range.f_end = sz 5 }
               <:
               Core.Ops.Range.t_Range usize ]
@@ -138,10 +138,10 @@ let index_mutation_unsize (x: t_Array u8 (sz 12)) : u8 =
   42uy
 
 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 #u8 () in
+  let vec1:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new u8 () in
   let vec2:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-    Alloc.Slice.impl__into_vec #u8
-      #Alloc.Alloc.t_Global
+    Alloc.Slice.impl__into_vec u8
+      Alloc.Alloc.t_Global
       (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list = [1uy; 2uy; 3uy] in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
                 Rust_primitives.Hax.array_of_list 3 list)
@@ -152,14 +152,14 @@ let test_append (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
   in
   let tmp0, tmp1:(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
   =
-    Alloc.Vec.impl_1__append #u8 #Alloc.Alloc.t_Global vec1 vec2
+    Alloc.Vec.impl_1__append u8 Alloc.Alloc.t_Global vec1 vec2
   in
   let vec1:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = tmp0 in
   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 #u8
-      #Alloc.Alloc.t_Global
+    Alloc.Vec.impl_1__append u8
+      Alloc.Alloc.t_Global
       vec1
       (build_vec () <: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
   in
@@ -195,7 +195,7 @@ let impl__S__update (self: t_S) (x: u8) : t_S =
 
 let foo (lhs rhs: t_S) : t_S =
   let lhs:t_S =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range
             usize)
           ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 1 }
             <:
@@ -243,7 +243,7 @@ let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
     : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
   let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in
   let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range
             u8)
           ({ Core.Ops.Range.f_start = 1uy; Core.Ops.Range.f_end = 10uy }
             <:
@@ -258,7 +258,7 @@ let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
             x with
             f_a
             =
-            Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global x.f_a i
+            Alloc.Vec.impl_1__push u8 Alloc.Alloc.t_Global x.f_a i
             <:
             Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
           }
@@ -266,14 +266,14 @@ let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
           t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
   in
   let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
-    { x with f_a = Core.Slice.impl__swap #u8 x.f_a (sz 0) (sz 1) }
+    { x with f_a = Core.Slice.impl__swap u8 x.f_a (sz 0) (sz 1) }
     <:
     t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
   in
   let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
     {
       x with
-      f_b = { x.f_b with f_field = Core.Slice.impl__swap #u8 x.f_b.f_field (sz 0) (sz 1) } <: t_Foo
+      f_b = { x.f_b with f_field = Core.Slice.impl__swap u8 x.f_b.f_field (sz 0) (sz 1) } <: t_Foo
     }
     <:
     t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
index 68c009f19..d07cb6cbc 100644
--- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
@@ -43,8 +43,8 @@ let debug (label value: u32) : Prims.unit =
             t_Slice string)
           (Rust_primitives.unsize (let list =
                   [
-                    Core.Fmt.Rt.impl_1__new_display #u32 label <: Core.Fmt.Rt.t_Argument;
-                    Core.Fmt.Rt.impl_1__new_display #u32 value <: Core.Fmt.Rt.t_Argument
+                    Core.Fmt.Rt.impl_1__new_display u32 label <: Core.Fmt.Rt.t_Argument;
+                    Core.Fmt.Rt.impl_1__new_display u32 value <: Core.Fmt.Rt.t_Argument
                   ]
                 in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
@@ -128,7 +128,7 @@ let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a t_Foo = { __marker_trait = () }
 let v_INHERENT_CONSTANT: usize = sz 3
 
 let constants
-      (#v_T: Type0)
+      (v_T: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_FooTrait v_T)
       (_: Prims.unit)
     : usize = f_ASSOCIATED_CONSTANT +! v_INHERENT_CONSTANT
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
index f99f13441..f0a29b925 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
@@ -117,7 +117,7 @@ let local_mutation (x: u32) : u32 =
     let y:u32 = x /! 2ul in
     let y:u32 = Core.Num.impl__u32__wrapping_add y 2ul in
     let y:u32 =
-      Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+      Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range
               u32)
             ({ Core.Ops.Range.f_start = 0ul; Core.Ops.Range.f_end = 10ul }
               <:
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
index 8047ce566..1f6d1158e 100644
--- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
@@ -36,7 +36,7 @@ class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl
-      (#v_P: Type0)
+      (v_P: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i0: Core.Ops.Function.t_FnMut v_P u8)
     : t_Trait v_P = { __marker_trait = () }
 '''
@@ -48,10 +48,10 @@ open FStar.Mul
 
 let minimized_1_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
     : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-  Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter
+  Core.Iter.Traits.Iterator.f_collect (Core.Iter.Adapters.Filter.t_Filter
         (Core.Ops.Range.t_Range u8) (u8 -> bool))
-    #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
-    (Core.Iter.Traits.Iterator.f_filter #(Core.Ops.Range.t_Range u8)
+    (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+    (Core.Iter.Traits.Iterator.f_filter (Core.Ops.Range.t_Range u8)
         ({ Core.Ops.Range.f_start = 0uy; Core.Ops.Range.f_end = 5uy } <: Core.Ops.Range.t_Range u8)
         (fun temp_0_ ->
             let _:u8 = temp_0_ in
@@ -63,9 +63,9 @@ let minimized_2_ (it: Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range
     : Prims.unit =
   let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
   =
-    Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter
+    Core.Iter.Traits.Iterator.f_collect (Core.Iter.Adapters.Filter.t_Filter
           (Core.Ops.Range.t_Range u8) (u8 -> bool))
-      #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+      (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
       it
   in
   ()
@@ -73,18 +73,18 @@ let minimized_2_ (it: Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range
 let original_function_from_495_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) : Prims.unit =
   let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
   =
-    Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter
+    Core.Iter.Traits.Iterator.f_collect (Core.Iter.Adapters.Filter.t_Filter
           (Core.Ops.Range.t_Range u8) (u8 -> bool))
-      #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
-      (Core.Iter.Traits.Iterator.f_filter #(Core.Ops.Range.t_Range u8)
+      (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+      (Core.Iter.Traits.Iterator.f_filter (Core.Ops.Range.t_Range u8)
           ({ Core.Ops.Range.f_start = 0uy; Core.Ops.Range.f_end = 5uy } <: Core.Ops.Range.t_Range u8
           )
           (fun i ->
               let i:u8 = i in
               let _, out:(Core.Slice.Iter.t_Iter u8 & bool) =
-                Core.Iter.Traits.Iterator.f_any #(Core.Slice.Iter.t_Iter u8)
-                  (Core.Slice.impl__iter #u8
-                      (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) list
+                Core.Iter.Traits.Iterator.f_any (Core.Slice.Iter.t_Iter u8)
+                  (Core.Slice.impl__iter u8
+                      (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) list
                         <:
                         t_Slice u8)
                     <:
@@ -111,9 +111,9 @@ class t_Foo (v_Self: Type0) (v_T: Type0) = {
   f_to_t:x0: v_Self -> Prims.Pure v_T (f_to_t_pre x0) (fun result -> f_to_t_post x0 result)
 }
 
-let v__f (#v_X: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_X u8) (x: v_X)
+let v__f (v_X: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_X u8) (x: v_X)
     : Prims.unit =
-  let _:u8 = f_to_t #v_X #u8 x in
+  let _:u8 = f_to_t v_X u8 x in
   ()
 '''
 "Traits.Implicit_dependencies_issue_667_.Define_type.fst" = '''
@@ -170,7 +170,7 @@ let _ =
   ()
 
 let some_function (x: Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType) : Prims.unit =
-  Traits.Implicit_dependencies_issue_667_.Trait_definition.f_my_method #Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType
+  Traits.Implicit_dependencies_issue_667_.Trait_definition.f_my_method Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType
     x
 '''
 "Traits.Unconstrainted_types_issue_677_.fst" = '''
@@ -185,8 +185,8 @@ class t_PolyOp (v_Self: Type0) = {
   f_op:x0: u32 -> x1: u32 -> Prims.Pure u32 (f_op_pre x0 x1) (fun result -> f_op_post x0 x1 result)
 }
 
-let twice (#v_OP: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_PolyOp v_OP) (x: u32)
-    : u32 = f_op #v_OP x x
+let twice (v_OP: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_PolyOp v_OP) (x: u32) : u32 =
+  f_op v_OP x x
 
 type t_Plus = | Plus : t_Plus
 
@@ -208,7 +208,7 @@ let impl_1: t_PolyOp t_Times =
     f_op = fun (x: u32) (y: u32) -> x *! y
   }
 
-let both (x: u32) : (u32 & u32) = twice #t_Plus x, twice #t_Times x <: (u32 & u32)
+let both (x: u32) : (u32 & u32) = twice t_Plus x, twice t_Times x <: (u32 & u32)
 '''
 "Traits.fst" = '''
 module Traits
@@ -222,8 +222,8 @@ class t_Bar (v_Self: Type0) = {
   f_bar:x0: v_Self -> Prims.Pure Prims.unit (f_bar_pre x0) (fun result -> f_bar_post x0 result)
 }
 
-let impl_2__method (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Bar v_T) (x: v_T)
-    : Prims.unit = f_bar #v_T x
+let impl_2__method (v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Bar v_T) (x: v_T)
+    : Prims.unit = f_bar v_T x
 
 type t_Error = | Error_Fail : t_Error
 
@@ -281,35 +281,34 @@ class t_Foo (v_Self: Type0) = {
 }
 
 let closure_impl_expr
-      (#v_I: Type0)
+      (v_I: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Iter.Traits.Iterator.t_Iterator v_I)
       (it: v_I)
     : Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global =
-  Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Map.t_Map v_I (Prims.unit -> Prims.unit))
-    #(Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global)
-    (Core.Iter.Traits.Iterator.f_map #v_I #Prims.unit it (fun x -> x)
+  Core.Iter.Traits.Iterator.f_collect (Core.Iter.Adapters.Map.t_Map v_I (Prims.unit -> Prims.unit))
+    (Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global)
+    (Core.Iter.Traits.Iterator.f_map v_I Prims.unit it (fun x -> x)
       <:
       Core.Iter.Adapters.Map.t_Map v_I (Prims.unit -> Prims.unit))
 
 let closure_impl_expr_fngen
-      (#v_I #v_F: Type0)
+      (v_I v_F: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i2: Core.Iter.Traits.Iterator.t_Iterator v_I)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i3: Core.Ops.Function.t_FnMut v_F Prims.unit)
       (it: v_I)
       (f: v_F)
     : Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global =
-  Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Map.t_Map v_I v_F)
-    #(Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global)
-    (Core.Iter.Traits.Iterator.f_map #v_I #Prims.unit #v_F it f
-      <:
-      Core.Iter.Adapters.Map.t_Map v_I v_F)
+  Core.Iter.Traits.Iterator.f_collect (Core.Iter.Adapters.Map.t_Map v_I v_F)
+    (Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global)
+    (Core.Iter.Traits.Iterator.f_map v_I Prims.unit v_F it f <: Core.Iter.Adapters.Map.t_Map v_I v_F
+    )
 
-let f (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: v_T) : Prims.unit =
-  let _:Prims.unit = f_assoc_f #v_T () in
-  f_method_f #v_T x
+let f (v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: v_T) : Prims.unit =
+  let _:Prims.unit = f_assoc_f v_T () in
+  f_method_f v_T x
 
-let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: i1.f_AssocType)
-    : u32 = f_function_of_super_trait #i1.f_AssocType x
+let g (v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: i1.f_AssocType)
+    : u32 = f_function_of_super_trait i1.f_AssocType x
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_Foo_for_tuple_: t_Foo Prims.unit =
@@ -322,7 +321,7 @@ let impl_Foo_for_tuple_: t_Foo Prims.unit =
     f_assoc_f = (fun (_: Prims.unit) -> () <: Prims.unit);
     f_method_f_pre = (fun (self: Prims.unit) -> true);
     f_method_f_post = (fun (self: Prims.unit) (out: Prims.unit) -> true);
-    f_method_f = (fun (self: Prims.unit) -> f_assoc_f #Prims.unit ());
+    f_method_f = (fun (self: Prims.unit) -> f_assoc_f Prims.unit ());
     f_assoc_type_pre = (fun (_: i32) -> true);
     f_assoc_type_post = (fun (_: i32) (out: Prims.unit) -> true);
     f_assoc_type = fun (_: i32) -> ()