diff --git a/proofs/fstar/extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti b/proofs/fstar/extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti
index 478ef7e3c..df3b6b7ee 100644
--- a/proofs/fstar/extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti
+++ b/proofs/fstar/extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti
@@ -7,11 +7,11 @@ open MkSeq
 let int_arr_bitwise_eq
        #t1 #t2 #n1 #n2
        (arr1: t_Array (int_t t1) n1)
-       (d1: bit_num t1)
+       (d1: num_bits t1)
        (arr2: t_Array (x: int_t t2) n2)
-       (d2: bit_num t2 {v n1 * d1 == v n2 * d2})
+       (d2: num_bits t2 {v n1 * d1 == v n2 * d2})
      = forall i. i < v n1 * d1
-       ==> bit_vec_of_int_arr arr1 d1 i == bit_vec_of_int_arr arr2 d2 i
+       ==> bit_vec_of_int_t_array arr1 d1 i == bit_vec_of_int_t_array arr2 d2 i
 
 val compress_coefficients_10_ (coefficient1 coefficient2 coefficient3 coefficient4: i32)
     : Prims.Pure (u8 & u8 & u8 & u8 & u8) 
diff --git a/proofs/fstar/extraction-edited/Spec.Kyber.fst b/proofs/fstar/extraction-edited/Spec.Kyber.fst
index ee07bc60e..36dfe26ed 100644
--- a/proofs/fstar/extraction-edited/Spec.Kyber.fst
+++ b/proofs/fstar/extraction-edited/Spec.Kyber.fst
@@ -170,21 +170,21 @@ let compress_d (d: dT {d <> 12}) (x: field_element): field_element
 let bits_to_bytes (#bytes: usize) (bv: bit_vec (v bytes * 8))
   : Pure (t_Array u8 bytes)
          (requires True)
-         (ensures fun r -> (forall i. bit_vec_of_int_arr r 8 i == bv i))
-  = bit_vec_to_int_arr 8 bv
+         (ensures fun r -> (forall i. bit_vec_of_int_t_array r 8 i == bv i))
+  = bit_vec_to_int_t_array 8 bv
 
 let bytes_to_bits (#bytes: usize) (r: t_Array u8 bytes)
   : Pure (i: bit_vec (v bytes * 8))
          (requires True)
-         (ensures fun f -> (forall i. bit_vec_of_int_arr r 8 i == f i))
-  = bit_vec_of_int_arr r 8
+         (ensures fun f -> (forall i. bit_vec_of_int_t_array r 8 i == f i))
+  = bit_vec_of_int_t_array r 8
 
 let byte_encode (d: dT) (coefficients: polynomial): t_Array u8 (sz (32 * d))
-  = bits_to_bytes #(sz (32 * d)) (bit_vec_of_nat_arr coefficients d)
+  = bits_to_bytes #(sz (32 * d)) (bit_vec_of_nat_array coefficients d)
 
 let byte_decode (d: dT) (coefficients: t_Array u8 (sz (32 * d))): polynomial
-  = let bv = bit_vec_of_int_arr coefficients 8 in
-    let arr: t_Array nat (sz 256) = bit_vec_to_nat_arr d bv in
+  = let bv = bit_vec_of_int_t_array coefficients 8 in
+    let arr: t_Array nat (sz 256) = bit_vec_to_nat_array d bv in
     let p = map' (fun (x: nat) -> x % v v_FIELD_MODULUS <: nat) arr in
     introduce forall i. Seq.index p i < v v_FIELD_MODULUS
     with assert (Seq.index p i == Seq.index p (v (sz i)));