diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fsti
index bbfabd9ce..37a31b2e7 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fsti
@@ -233,7 +233,7 @@ val compress_then_serialize_ring_element_v
     : Prims.Pure (t_Slice u8)
       (requires
         Spec.MLKEM.is_rank v_K /\
-        v v_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\
+        v_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\
         Seq.length out == v v_OUT_LEN /\ coefficients_field_modulus_range re)
       (ensures
         fun out_future ->
diff --git a/libcrux-ml-kem/src/serialize.rs b/libcrux-ml-kem/src/serialize.rs
index 8e1e91afd..6a3de2749 100644
--- a/libcrux-ml-kem/src/serialize.rs
+++ b/libcrux-ml-kem/src/serialize.rs
@@ -326,7 +326,7 @@ fn compress_then_serialize_5<Vector: Operations>(
 #[inline(always)]
 #[hax_lib::fstar::verification_status(panic_free)]
 #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank v_K /\\ 
-    v $COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\\
+    $COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\\
     Seq.length $out == v $OUT_LEN /\\ coefficients_field_modulus_range $re"))]
 #[hax_lib::ensures(|_|
     fstar!("${out_future.len()} == ${out.len()} /\\