1 files changed, 14 insertions, 14 deletions

diff --git a/tests/fstar/hashmap/Hashmap.Properties.fst b/tests/fstar/hashmap/Hashmap.Properties.fst
index 724ca741..e1d0a541 100644
--- a/tests/fstar/hashmap/Hashmap.Properties.fst
+++ b/tests/fstar/hashmap/Hashmap.Properties.fst
@@ -2704,16 +2704,16 @@ let hash_map_get_fwd_lem #t self key = hash_map_get_fwd_lem_aux #t self key
 (**** get_mut_in_list'fwd *)
 
 val hash_map_get_mut_in_list_loop_fwd_lem
-  (#t : Type0) (key : usize) (ls : list_t t) :
+  (#t : Type0) (ls : list_t t) (key : usize) :
   Lemma
   (ensures (
-    match hash_map_get_mut_in_list_loop_fwd t key ls, slot_t_find_s key ls with
+    match hash_map_get_mut_in_list_loop_fwd t ls key, slot_t_find_s key ls with
     | Fail _, None -> True
     | Return x, Some x' -> x == x'
     | _ -> False))
 
 #push-options "--fuel 1"
-let rec hash_map_get_mut_in_list_loop_fwd_lem #t key ls =
+let rec hash_map_get_mut_in_list_loop_fwd_lem #t ls key =
   begin match ls with
   | ListCons ckey cvalue ls0 ->
     let b = ckey = key in
@@ -2721,8 +2721,8 @@ let rec hash_map_get_mut_in_list_loop_fwd_lem #t key ls =
     then ()
     else
       begin
-      hash_map_get_mut_in_list_loop_fwd_lem key ls0;
-      match hash_map_get_mut_in_list_loop_fwd t key ls0 with
+      hash_map_get_mut_in_list_loop_fwd_lem ls0 key;
+      match hash_map_get_mut_in_list_loop_fwd t ls0 key with
       | Fail _ -> ()
       | Return x -> ()
       end
@@ -2754,8 +2754,8 @@ let hash_map_get_mut_fwd_lem_aux #t self key =
       | Fail _ -> ()
       | Return l ->
         begin
-        hash_map_get_mut_in_list_loop_fwd_lem key l;
-        match hash_map_get_mut_in_list_loop_fwd t key l with
+        hash_map_get_mut_in_list_loop_fwd_lem l key;
+        match hash_map_get_mut_in_list_loop_fwd t l key with
         | Fail _ -> ()
         | Return x -> ()
         end
@@ -2771,17 +2771,17 @@ let hash_map_get_mut_fwd_lem #t self key =
 (**** get_mut_in_list'back *)
 
 val hash_map_get_mut_in_list_loop_back_lem
-  (#t : Type0) (key : usize) (ls : list_t t) (ret : t) :
+  (#t : Type0) (ls : list_t t) (key : usize) (ret : t) :
   Lemma
   (requires (Some? (slot_t_find_s key ls)))
   (ensures (
-    match hash_map_get_mut_in_list_loop_back t key ls ret with
+    match hash_map_get_mut_in_list_loop_back t ls key ret with
     | Fail _ -> False
     | Return ls' -> list_t_v ls' == find_update (same_key key) (list_t_v ls) (key,ret)
     | _ -> False))
 
 #push-options "--fuel 1"
-let rec hash_map_get_mut_in_list_loop_back_lem #t key ls ret =
+let rec hash_map_get_mut_in_list_loop_back_lem #t ls key ret =
   begin match ls with
   | ListCons ckey cvalue ls0 ->
     let b = ckey = key in
@@ -2789,8 +2789,8 @@ let rec hash_map_get_mut_in_list_loop_back_lem #t key ls ret =
     then let ls1 = ListCons ckey ret ls0 in ()
     else
       begin
-      hash_map_get_mut_in_list_loop_back_lem key ls0 ret;
-      match hash_map_get_mut_in_list_loop_back t key ls0 ret with
+      hash_map_get_mut_in_list_loop_back_lem ls0 key ret;
+      match hash_map_get_mut_in_list_loop_back t ls0 key ret with
       | Fail _ -> ()
       | Return l -> let ls1 = ListCons ckey cvalue l in ()
       end
@@ -2828,8 +2828,8 @@ let hash_map_get_mut_back_lem_refin #t self key ret =
       | Fail _ -> ()
       | Return l ->
         begin
-        hash_map_get_mut_in_list_loop_back_lem key l ret;
-        match hash_map_get_mut_in_list_loop_back t key l ret with
+        hash_map_get_mut_in_list_loop_back_lem l key ret;
+        match hash_map_get_mut_in_list_loop_back t l key ret with
         | Fail _ -> ()
         | Return l0 ->
           begin match vec_index_mut_back (list_t t) v hash_mod l0 with