diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst
index 54b447f80..2ae166f32 100644
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst
+++ b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst
@@ -18,18 +18,6 @@ class update_at_tc self idx = {
 
 open Core.Slice
 
-instance impl__index t l n: t_Index (t_Array t l) (int_t n)
-  = { f_Output = t;
-      f_index_pre = (fun (s: t_Array t l) (i: int_t n) -> v i >= 0 && v i < v l);
-      f_index_post = (fun _ _ _ -> true);
-      f_index = (fun s i -> Seq.index s (v i));
-    }
-
-instance update_at_tc_array t l n: update_at_tc (t_Array t l) (int_t n) = {
-  super_index = FStar.Tactics.Typeclasses.solve <: t_Index (t_Array t l) (int_t n);
-  update_at = (fun arr i x -> FStar.Seq.upd arr (v i) x);
-}
-
 /// We have an instance for `int_t n`, but we often work with refined
 /// `int_t n`, and F* typeclass inference doesn't support subtyping
 /// well, hence the instance below.
@@ -47,6 +35,18 @@ instance update_at_tc_array_refined t l n r: update_at_tc (t_Array t l) (x: int_
   update_at = (fun arr i x -> FStar.Seq.upd arr (v i) x);
 }
 
+instance impl__index t l n: t_Index (t_Array t l) (int_t n)
+  = { f_Output = t;
+      f_index_pre = (fun (s: t_Array t l) (i: int_t n) -> v i >= 0 && v i < v l);
+      f_index_post = (fun _ _ _ -> true);
+      f_index = (fun s i -> Seq.index s (v i));
+    }
+
+instance update_at_tc_array t l n: update_at_tc (t_Array t l) (int_t n) = {
+  super_index = FStar.Tactics.Typeclasses.solve <: t_Index (t_Array t l) (int_t n);
+  update_at = (fun arr i x -> FStar.Seq.upd arr (v i) x);
+}
+
 let (.[]<-) #self #idx {| update_at_tc self idx |} (s: self) (i: idx {f_index_pre s i})
   = update_at s i