diff --git a/proof-libs/fstar-secret-integers/core/Alloc.Slice.fst b/proof-libs/fstar-secret-integers/core/Alloc.Slice.fst
index f9ea629b7..2927bcc63 100644
--- a/proof-libs/fstar-secret-integers/core/Alloc.Slice.fst
+++ b/proof-libs/fstar-secret-integers/core/Alloc.Slice.fst
@@ -2,4 +2,4 @@ module Alloc.Slice
 open Rust_primitives.Arrays
 open Alloc.Vec
 
-let impl__to_vec (s: t_Slice 'a): t_Vec 'a Alloc.Alloc.t_Global = s
+let impl__to_vec #a (s: t_Slice a): t_Vec a Alloc.Alloc.t_Global = s
diff --git a/proof-libs/fstar-secret-integers/core/Alloc.Vec.fst b/proof-libs/fstar-secret-integers/core/Alloc.Vec.fst
index ef3dd3301..6304829cd 100644
--- a/proof-libs/fstar-secret-integers/core/Alloc.Vec.fst
+++ b/proof-libs/fstar-secret-integers/core/Alloc.Vec.fst
@@ -13,19 +13,19 @@ 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
 // instead.
-let impl_1__push
-  (v: t_Vec 't ())// Removed: {Seq.length v + 1 <= max_usize})
-  (x: 't)
-   : t_Vec 't () = 
+let impl_1__push #t
+  (v: t_Vec t ())// Removed: {Seq.length v + 1 <= max_usize})
+  (x: t)
+   : t_Vec t () = 
      if Seq.length v <= max_usize then v else
      FStar.Seq.append v (FStar.Seq.create 1 x)
 
-let impl_1__len (v: t_Vec 't ()) =
+let impl_1__len #t (v: t_Vec t ()) =
   let n = Seq.length v in
   assert (n <= maxint usize_inttype);
   mk_int #usize_inttype (Seq.length v)
 
-let from_elem (item: 'a) (len: usize) = Seq.create (v len) item
+let from_elem #a (item: a) (len: usize) = Seq.create (v len) item
 
 open Rust_primitives.Hax
 open Core.Ops.Index
diff --git a/proof-libs/fstar-secret-integers/core/Core.Array.fst b/proof-libs/fstar-secret-integers/core/Core.Array.fst
index 6e91fc6ca..c17a58262 100644
--- a/proof-libs/fstar-secret-integers/core/Core.Array.fst
+++ b/proof-libs/fstar-secret-integers/core/Core.Array.fst
@@ -3,8 +3,8 @@ open Rust_primitives
 
 type t_TryFromSliceError = | TryFromSliceError
 
-let impl_23__map n (arr: t_Array 'a n) (f: 'a -> 'b): t_Array 'b n 
+let impl_23__map #a #b n (arr: t_Array a n) (f: a -> b): t_Array b n 
   = map_array arr f
 
-let impl_23__as_slice len (arr: t_Array 'a len): t_Slice 'a = arr
+let impl_23__as_slice #a len (arr: t_Array a len): t_Slice a = arr
 
diff --git a/proof-libs/fstar-secret-integers/core/Core.Ops.Index.fst b/proof-libs/fstar-secret-integers/core/Core.Ops.Index.fst
index b4e4e368f..59621d14e 100644
--- a/proof-libs/fstar-secret-integers/core/Core.Ops.Index.fst
+++ b/proof-libs/fstar-secret-integers/core/Core.Ops.Index.fst
@@ -1,7 +1,7 @@
 module Core.Ops.Index
 
 class t_Index (t_Self:Type0) (t_Idx:Type0) = {
-  f_Output: Type;
+  f_Output: Type0;
   in_range: t_Self -> t_Idx -> Type0;
   f_index: s:t_Self -> i:t_Idx{in_range s i} -> f_Output;
 }
diff --git a/proof-libs/fstar-secret-integers/core/Core.Option.fst b/proof-libs/fstar-secret-integers/core/Core.Option.fst
index 485742318..77e65eff4 100644
--- a/proof-libs/fstar-secret-integers/core/Core.Option.fst
+++ b/proof-libs/fstar-secret-integers/core/Core.Option.fst
@@ -2,12 +2,12 @@ module Core.Option
 
 type t_Option t = | Option_Some of t | Option_None
 
-let impl__and_then (self: t_Option 'self) (f: 'self -> t_Option 't): t_Option 't = 
+let impl__and_then #t #t_Self (self: t_Option t_Self) (f: t_Self -> t_Option t): t_Option t = 
   match self with
   | Option_Some x -> f x
   | Option_None -> Option_None
 
 let impl__unwrap #t (x: t_Option t {Option_Some? x}): t = Option_Some?._0 x
 
-let impl__is_some (self: t_Option 'self): bool =  Option_Some? self
+let impl__is_some #t_Self (self: t_Option t_Self): bool =  Option_Some? self
 
diff --git a/proof-libs/fstar-secret-integers/core/Core.Slice.fsti b/proof-libs/fstar-secret-integers/core/Core.Slice.fsti
index cff5480cf..6851d96bd 100644
--- a/proof-libs/fstar-secret-integers/core/Core.Slice.fsti
+++ b/proof-libs/fstar-secret-integers/core/Core.Slice.fsti
@@ -8,12 +8,12 @@ let impl__len (#t: Type) (s: t_Slice t)
 
 open Core.Slice.Iter
 
-val impl__chunks (x: t_Slice 'a) (cs: usize): t_Chunks 'a
+val impl__chunks #a (x: t_Slice a) (cs: usize): t_Chunks a
 
-let impl__iter (s: t_Slice 't): t_Slice 't = s
+let impl__iter #t (s: t_Slice t): t_Slice t = s
 
-val impl__chunks_exact (x: t_Slice 'a) (cs: usize):
-    Pure (t_Slice (t_Slice 'a))
+val impl__chunks_exact #a (x: t_Slice a) (cs: usize):
+    Pure (t_Slice (t_Slice a))
     (requires True)
     (ensures (fun r -> forall i. i < v (length x) ==> length x ==  cs))
 
diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fst b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fst
index 42b6255de..3df35bd8d 100644
--- a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fst
+++ b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fst
@@ -8,7 +8,7 @@ let to_list (#t:Type) (s: t_Slice t): list t = Seq.seq_to_list s
 let to_of_list_lemma t l = Seq.lemma_list_seq_bij l
 let of_to_list_lemma t l = Seq.lemma_seq_list_bij l
 
-let map_array #n (arr: t_Array 'a n) (f: 'a -> 'b): t_Array 'b n 
+let map_array #a #b #n (arr: t_Array a n) (f: a -> b): t_Array b n 
   = FStar.Seq.map_seq_len f arr;
     FStar.Seq.map_seq f arr 
 
diff --git a/proof-libs/fstar/core/Alloc.Slice.fst b/proof-libs/fstar/core/Alloc.Slice.fst
index f9ea629b7..2927bcc63 100644
--- a/proof-libs/fstar/core/Alloc.Slice.fst
+++ b/proof-libs/fstar/core/Alloc.Slice.fst
@@ -2,4 +2,4 @@ module Alloc.Slice
 open Rust_primitives.Arrays
 open Alloc.Vec
 
-let impl__to_vec (s: t_Slice 'a): t_Vec 'a Alloc.Alloc.t_Global = s
+let impl__to_vec #a (s: t_Slice a): t_Vec a Alloc.Alloc.t_Global = s
diff --git a/proof-libs/fstar/core/Alloc.Vec.fst b/proof-libs/fstar/core/Alloc.Vec.fst
index 73c08c75f..34b6fb87f 100644
--- a/proof-libs/fstar/core/Alloc.Vec.fst
+++ b/proof-libs/fstar/core/Alloc.Vec.fst
@@ -13,19 +13,19 @@ 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
 // instead.
-let impl_1__push
-  (v: t_Vec 't ())// Removed: {Seq.length v + 1 <= max_usize})
-  (x: 't)
-   : t_Vec 't () = 
+let impl_1__push #t
+  (v: t_Vec t ())// Removed: {Seq.length v + 1 <= max_usize})
+  (x: t)
+   : t_Vec t () = 
      if Seq.length v <= max_usize then v else
      FStar.Seq.append v (FStar.Seq.create 1 x)
 
-let impl_1__len (v: t_Vec 't ()) =
+let impl_1__len #t (v: t_Vec t ()) =
   let n = Seq.length v in
   assert (n <= maxint usize_inttype);
   mk_int #usize_inttype (Seq.length v)
 
-let from_elem (item: 'a) (len: usize) = Seq.create (v len) item
+let from_elem #a (item: a) (len: usize) = Seq.create (v len) item
 
 open Rust_primitives.Hax
 open Core.Ops.Index
diff --git a/proof-libs/fstar/core/Core.Array.fst b/proof-libs/fstar/core/Core.Array.fst
index 6e91fc6ca..c17a58262 100644
--- a/proof-libs/fstar/core/Core.Array.fst
+++ b/proof-libs/fstar/core/Core.Array.fst
@@ -3,8 +3,8 @@ open Rust_primitives
 
 type t_TryFromSliceError = | TryFromSliceError
 
-let impl_23__map n (arr: t_Array 'a n) (f: 'a -> 'b): t_Array 'b n 
+let impl_23__map #a #b n (arr: t_Array a n) (f: a -> b): t_Array b n 
   = map_array arr f
 
-let impl_23__as_slice len (arr: t_Array 'a len): t_Slice 'a = arr
+let impl_23__as_slice #a len (arr: t_Array a len): t_Slice a = arr
 
diff --git a/proof-libs/fstar/core/Core.Convert.fst b/proof-libs/fstar/core/Core.Convert.fst
index 785ee8add..826fe9f82 100644
--- a/proof-libs/fstar/core/Core.Convert.fst
+++ b/proof-libs/fstar/core/Core.Convert.fst
@@ -4,7 +4,7 @@ open Rust_primitives
 
 class try_into_tc self t = {
   [@@@FStar.Tactics.Typeclasses.no_method]
-  f_Error: Type;
+  f_Error: Type0;
   f_try_into: self -> Core.Result.t_Result t f_Error
 }
 
@@ -35,7 +35,7 @@ class t_From self t = {
 
 class t_TryFrom self t = {
   [@@@FStar.Tactics.Typeclasses.no_method]
-  f_Error: Type;
+  f_Error: Type0;
   f_try_from: t -> Core.Result.t_Result self f_Error;
 }
 
diff --git a/proof-libs/fstar/core/Core.Iter.Traits.Collect.fst b/proof-libs/fstar/core/Core.Iter.Traits.Collect.fst
index 9051db81f..33b16938c 100644
--- a/proof-libs/fstar/core/Core.Iter.Traits.Collect.fst
+++ b/proof-libs/fstar/core/Core.Iter.Traits.Collect.fst
@@ -1,8 +1,8 @@
 module Core.Iter.Traits.Collect
 
 class into_iterator self = {
-  f_IntoIter: Type;
-  // f_Item: Type;
+  f_IntoIter: Type0;
+  // f_Item: Type0;
   f_into_iter: self -> f_IntoIter;
 }
 
diff --git a/proof-libs/fstar/core/Core.Iter.Traits.Iterator.fst b/proof-libs/fstar/core/Core.Iter.Traits.Iterator.fst
index 5a6c8b837..6a9c67564 100644
--- a/proof-libs/fstar/core/Core.Iter.Traits.Iterator.fst
+++ b/proof-libs/fstar/core/Core.Iter.Traits.Iterator.fst
@@ -21,7 +21,7 @@ unfold type t_all self item
 
 (* Inference behaves strangly with type synonyms... :( *)
 // class iterator (self: Type) = {
-//   f_Item: Type;
+//   f_Item: Type0;
 //   f_next:      t_next      self f_Item;
 //   f_contains:  t_contains  self f_Item; (* hax-specific method *)
 //   f_fold:      t_fold      self f_Item f_contains;
diff --git a/proof-libs/fstar/core/Core.Ops.Index.IndexMut.fst b/proof-libs/fstar/core/Core.Ops.Index.IndexMut.fst
index 486a16af9..a0b61d5ee 100644
--- a/proof-libs/fstar/core/Core.Ops.Index.IndexMut.fst
+++ b/proof-libs/fstar/core/Core.Ops.Index.IndexMut.fst
@@ -1,7 +1,7 @@
 module Core.Ops.Index.IndexMut
 
 class t_IndexMut t_Self t_Idx = {
-  f_Input: Type;
+  f_Input: Type0;
   in_range: t_Self -> t_Idx -> Type0;
   f_index_mut: s:t_Self -> i:t_Idx{in_range s i} -> v:f_Input -> t_Self;
 }
diff --git a/proof-libs/fstar/core/Core.Ops.Index.fst b/proof-libs/fstar/core/Core.Ops.Index.fst
index cfc366569..200d1e250 100644
--- a/proof-libs/fstar/core/Core.Ops.Index.fst
+++ b/proof-libs/fstar/core/Core.Ops.Index.fst
@@ -1,7 +1,7 @@
 module Core.Ops.Index
 
 class t_Index t_Self t_Idx = {
-  f_Output: Type;
+  f_Output: Type0;
   in_range: t_Self -> t_Idx -> Type0;
   f_index: s:t_Self -> i:t_Idx{in_range s i} -> f_Output;
 }
diff --git a/proof-libs/fstar/core/Core.Ops.Range.fsti b/proof-libs/fstar/core/Core.Ops.Range.fsti
index f300ea577..2ad1ee5ec 100644
--- a/proof-libs/fstar/core/Core.Ops.Range.fsti
+++ b/proof-libs/fstar/core/Core.Ops.Range.fsti
@@ -8,10 +8,10 @@ type t_RangeFull           = | RangeFull
 
 open Core.Iter.Traits.Iterator
 
-let rec fold_range' #t
+let rec fold_range' #a #t
   (min: Rust_primitives.int_t t) (max: Rust_primitives.int_t t {v min <= v max})
-  (init: 'a) (f: ('a -> i:Rust_primitives.int_t t{v i < v max /\ v i >= v min} -> 'a))
-  : Tot 'a (decreases (v max - v min))
+  (init: a) (f: (a -> i:Rust_primitives.int_t t{v i < v max /\ v i >= v min} -> a))
+  : Tot a (decreases (v max - v min))
   = if min = max
     then init
     else fold_range' (add min (Rust_primitives.mk_int 1)) max (f init min) f
diff --git a/proof-libs/fstar/core/Core.Ops.Try_trait.fst b/proof-libs/fstar/core/Core.Ops.Try_trait.fst
index 871d2651a..7c167e603 100644
--- a/proof-libs/fstar/core/Core.Ops.Try_trait.fst
+++ b/proof-libs/fstar/core/Core.Ops.Try_trait.fst
@@ -5,8 +5,8 @@ class t_FromResidual self r = {
 }
 
 class t_Try self = {
-   f_Output: Type;
-   f_Residual: Type;
+   f_Output: Type0;
+   f_Residual: Type0;
    [@@@FStar.Tactics.Typeclasses.tcresolve]
    parent_FromResidual: t_FromResidual f_Residual f_Residual;
 
diff --git a/proof-libs/fstar/core/Core.Option.fst b/proof-libs/fstar/core/Core.Option.fst
index 485742318..77e65eff4 100644
--- a/proof-libs/fstar/core/Core.Option.fst
+++ b/proof-libs/fstar/core/Core.Option.fst
@@ -2,12 +2,12 @@ module Core.Option
 
 type t_Option t = | Option_Some of t | Option_None
 
-let impl__and_then (self: t_Option 'self) (f: 'self -> t_Option 't): t_Option 't = 
+let impl__and_then #t #t_Self (self: t_Option t_Self) (f: t_Self -> t_Option t): t_Option t = 
   match self with
   | Option_Some x -> f x
   | Option_None -> Option_None
 
 let impl__unwrap #t (x: t_Option t {Option_Some? x}): t = Option_Some?._0 x
 
-let impl__is_some (self: t_Option 'self): bool =  Option_Some? self
+let impl__is_some #t_Self (self: t_Option t_Self): bool =  Option_Some? self
 
diff --git a/proof-libs/fstar/core/Core.Result.fst b/proof-libs/fstar/core/Core.Result.fst
index 69472da04..ee958b651 100644
--- a/proof-libs/fstar/core/Core.Result.fst
+++ b/proof-libs/fstar/core/Core.Result.fst
@@ -3,7 +3,7 @@ module Core.Result
 type t_Result t e = | Result_Ok: v:t -> t_Result t e
                     | Result_Err of e
 
-let impl__unwrap (x: t_Result 't 'e {Result_Ok? x}): 't = Result_Ok?.v x
+let impl__unwrap #t #e (x: t_Result t e {Result_Ok? x}): t = Result_Ok?.v x
 let impl__map_err #e1 #e2 (x: t_Result 't e1) (f: e1 -> e2): t_Result 't e2
   = match x with
   | Result_Ok v -> Result_Ok v
diff --git a/proof-libs/fstar/core/Core.Slice.fsti b/proof-libs/fstar/core/Core.Slice.fsti
index cff5480cf..6851d96bd 100644
--- a/proof-libs/fstar/core/Core.Slice.fsti
+++ b/proof-libs/fstar/core/Core.Slice.fsti
@@ -8,12 +8,12 @@ let impl__len (#t: Type) (s: t_Slice t)
 
 open Core.Slice.Iter
 
-val impl__chunks (x: t_Slice 'a) (cs: usize): t_Chunks 'a
+val impl__chunks #a (x: t_Slice a) (cs: usize): t_Chunks a
 
-let impl__iter (s: t_Slice 't): t_Slice 't = s
+let impl__iter #t (s: t_Slice t): t_Slice t = s
 
-val impl__chunks_exact (x: t_Slice 'a) (cs: usize):
-    Pure (t_Slice (t_Slice 'a))
+val impl__chunks_exact #a (x: t_Slice a) (cs: usize):
+    Pure (t_Slice (t_Slice a))
     (requires True)
     (ensures (fun r -> forall i. i < v (length x) ==> length x ==  cs))
 
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Arrays.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.Arrays.fst
index b9cf470f2..df8e01342 100644
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.Arrays.fst
+++ b/proof-libs/fstar/rust_primitives/Rust_primitives.Arrays.fst
@@ -8,7 +8,7 @@ let to_list (#t:Type) (s: t_Slice t): list t = Seq.seq_to_list s
 let to_of_list_lemma t l = Seq.lemma_list_seq_bij l
 let of_to_list_lemma t l = Seq.lemma_seq_list_bij l
 
-let map_array #n (arr: t_Array 'a n) (f: 'a -> 'b): t_Array 'b n 
+let map_array #a #b #n (arr: t_Array a n) (f: a -> b): t_Array b n 
   = FStar.Seq.map_seq_len f arr;
     FStar.Seq.map_seq f arr 
 
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Arrays.fsti b/proof-libs/fstar/rust_primitives/Rust_primitives.Arrays.fsti
index 730cec90e..b18d77fd7 100644
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.Arrays.fsti
+++ b/proof-libs/fstar/rust_primitives/Rust_primitives.Arrays.fsti
@@ -7,7 +7,7 @@ type t_Slice t = s:Seq.seq t{Seq.length s <= max_usize}
 type t_Array t (l:usize) = s: Seq.seq t { Seq.length s == v l }
 
 /// Length of a slice
-let length (s: t_Slice 'a): usize = sz (Seq.length s)
+let length (#a: Type) (s: t_Slice a): usize = sz (Seq.length s)
 
 /// Check whether a slice contains an item
 let contains (#t: eqtype) (s: t_Slice t) (x: t): bool = Seq.mem x s
@@ -18,7 +18,7 @@ val of_list (#t:Type) (l: list t {FStar.List.Tot.length l < maxint Lib.IntTypes.
 /// Converts an slice into a F* list
 val to_list (#t:Type) (s: t_Slice t): list t
 
-val map_array #n (arr: t_Array 'a n) (f: 'a -> 'b): t_Array 'b n
+val map_array (#a #b: Type) #n (arr: t_Array a n) (f: a -> b): t_Array b n
 
 /// Creates an array of size `l` using a function `f`
 val createi #t (l:usize) (f:(u:usize{u <. l} -> t))
@@ -26,9 +26,9 @@ val createi #t (l:usize) (f:(u:usize{u <. l} -> t))
       (requires True)
       (ensures (fun res -> (forall i. Seq.index res (v i) == f i)))
 
-unfold let map #p
-  (f:(x:'a{p x} -> 'b))
-  (s: t_Slice 'a {forall (i:nat). i < Seq.length s ==> p (Seq.index s i)}): t_Slice 'b
+unfold let map #a #b #p
+  (f:(x:a{p x} -> b))
+  (s: t_Slice a {forall (i:nat). i < Seq.length s ==> p (Seq.index s i)}): t_Slice b
   = createi (length s) (fun i -> f (Seq.index s (v i)))
 
 /// Concatenates two slices
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Control_flow_monad.Moption.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Control_flow_monad.Moption.fst
index 30f8a3298..c46aa53de 100644
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Control_flow_monad.Moption.fst
+++ b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Control_flow_monad.Moption.fst
@@ -1,6 +1,6 @@
 module Rust_primitives.Hax.Control_flow_monad.Moption
 
-let run (f: Core.Option.t_Option (Core.Option.t_Option 'a)): Core.Option.t_Option 'a
+let run #a (f: Core.Option.t_Option (Core.Option.t_Option a)): Core.Option.t_Option a
     = match f with
     | Core.Option.Option_Some x -> x 
     | Core.Option.Option_None -> Core.Option.Option_None
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Control_flow_monad.Mresult.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Control_flow_monad.Mresult.fst
index e508ada99..12011da8a 100644
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Control_flow_monad.Mresult.fst
+++ b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Control_flow_monad.Mresult.fst
@@ -1,6 +1,6 @@
 module Rust_primitives.Hax.Control_flow_monad.Mresult
 
-let run (f: Core.Result.t_Result (Core.Result.t_Result 'a 'e) 'e): Core.Result.t_Result 'a 'e
+let run #a #e (f: Core.Result.t_Result (Core.Result.t_Result a e) e): Core.Result.t_Result a e
     = match f with
     | Core.Result.Result_Ok x -> x 
     | Core.Result.Result_Err e -> Core.Result.Result_Err e
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fsti b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fsti
index 60e01b18c..3ce6c7581 100644
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fsti
+++ b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fsti
@@ -7,20 +7,21 @@ open Rust_primitives
 open Rust_primitives.Hax
 open Core.Ops.Range
 
-
 val update_at_usize
-  (s: t_Slice 't)
+  (#t: Type0)
+  (s: t_Slice t)
   (i: usize)
-  (x: 't)
-  : Pure (t_Array 't (length s))
+  (x: t)
+  : Pure (t_Array t (length s))
     (requires (v i < Seq.length s))
     (ensures (fun res -> res == Seq.upd s (v i) x))
 
 val update_at_range #n
-  (s: t_Slice 't)
+  (t: Type0)
+  (s: t_Slice t)
   (i: t_Range (int_t n))
-  (x: t_Slice 't)
-  : Pure (t_Array 't (length s))
+  (x: t_Slice t)
+  : Pure (t_Array t (length s))
     (requires (v i.f_start >= 0 /\ v i.f_start <= Seq.length s /\
                v i.f_end <= Seq.length s /\
                Seq.length x == v i.f_end - v i.f_start))
@@ -30,10 +31,11 @@ val update_at_range #n
                 Seq.slice res (v i.f_end) (Seq.length res) == Seq.slice s (v i.f_end) (Seq.length s)))
 
 val update_at_range_to #n
-  (s: t_Slice 't)
+  (t: Type0)
+  (s: t_Slice t)
   (i: t_RangeTo (int_t n))
-  (x: t_Slice 't)
-  : Pure (t_Array 't (length s))
+  (x: t_Slice t)
+  : Pure (t_Array t (length s))
     (requires (v i.f_end >= 0 /\ v i.f_end <= Seq.length s /\
                Seq.length x == v i.f_end))
     (ensures (fun res ->
@@ -41,10 +43,11 @@ val update_at_range_to #n
                 Seq.slice res (v i.f_end) (Seq.length res) == Seq.slice s (v i.f_end) (Seq.length s)))
 
 val update_at_range_from #n
-  (s: t_Slice 't)
+  (t: Type0)
+  (s: t_Slice t)
   (i: t_RangeFrom (int_t n))
-  (x: t_Slice 't)
-  : Pure (t_Array 't (length s))
+  (x: t_Slice t)
+  : Pure (t_Array t (length s))
     (requires ( v i.f_start >= 0 /\ v i.f_start <= Seq.length s /\
                 Seq.length x == Seq.length s - v i.f_start))
     (ensures (fun res ->
@@ -52,9 +55,10 @@ val update_at_range_from #n
                 Seq.slice res (v i.f_start) (Seq.length res) == x))
 
 val update_at_range_full
-  (s: t_Slice 't)
+  (t: Type0)
+  (s: t_Slice t)
   (i: t_RangeFull)
-  (x: t_Slice 't)
-  : Pure (t_Array 't (length s))
+  (x: t_Slice t)
+  : Pure (t_Array t (length s))
     (requires (Seq.length x == Seq.length s))
     (ensures (fun res -> res == x))
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst
index f167b8421..39436f5c4 100644
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst
+++ b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst
@@ -6,7 +6,7 @@ open Rust_primitives.Arrays
 type t_Never = False
 let never_to_any #t: t_Never -> t = (fun _ -> match () with)
 
-let repeat (x: 'a) (len: usize): t_Array 'a len = 
+let repeat #a (x: a) (len: usize): t_Array a len = 
   FStar.Seq.create (v len) x
 
 open Core.Ops.Index
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.fst
index eea9ef6c2..1b9394eec 100644
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.fst
+++ b/proof-libs/fstar/rust_primitives/Rust_primitives.fst
@@ -4,12 +4,14 @@ include Rust_primitives.Integers
 include Rust_primitives.Arrays
 include Rust_primitives.BitVectors
 
-let (let?) (x: Core.Option.t_Option 'a) (f: 'a -> Core.Option.t_Option 'b): Core.Option.t_Option 'b
+let (let?) 
+  (#a #b: Type)
+  (x: Core.Option.t_Option a) (f: a -> Core.Option.t_Option b): Core.Option.t_Option b
   = match x with
   | Core.Option.Option_Some x -> f x
   | Core.Option.Option_None   -> Core.Option.Option_None
 
-let (let|) #e #a #b (x: Core.Result.t_Result a e) (f: a -> Core.Result.t_Result b e)
+let (let|) (#e #a #b: Type) (x: Core.Result.t_Result a e) (f: a -> Core.Result.t_Result b e)
     : Core.Result.t_Result b e
     = match x with
     | Core.Result.Result_Ok x -> f x