Regenerate the files

10 files changed, 147 insertions, 649 deletions

diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index f4ba7927..628eb2c3 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -13,10 +13,7 @@ let betree_load_internal_node_fwd
   (id : u64) (st : state) :
   result (state & (betree_list_t (u64 & betree_message_t)))
   =
-  begin match betree_utils_load_internal_node_fwd id st with
-  | Fail e -> Fail e
-  | Return (st0, l) -> Return (st0, l)
-  end
+  betree_utils_load_internal_node_fwd id st
 
 (** [betree_main::betree::store_internal_node] *)
 let betree_store_internal_node_fwd
@@ -31,10 +28,7 @@ let betree_store_internal_node_fwd
 (** [betree_main::betree::load_leaf_node] *)
 let betree_load_leaf_node_fwd
   (id : u64) (st : state) : result (state & (betree_list_t (u64 & u64))) =
-  begin match betree_utils_load_leaf_node_fwd id st with
-  | Fail e -> Fail e
-  | Return (st0, l) -> Return (st0, l)
-  end
+  betree_utils_load_leaf_node_fwd id st
 
 (** [betree_main::betree::store_leaf_node] *)
 let betree_store_leaf_node_fwd
@@ -54,11 +48,7 @@ let betree_fresh_node_id_fwd (counter : u64) : result u64 =
   end
 
 (** [betree_main::betree::fresh_node_id] *)
-let betree_fresh_node_id_back (counter : u64) : result u64 =
-  begin match u64_add counter 1 with
-  | Fail e -> Fail e
-  | Return counter0 -> Return counter0
-  end
+let betree_fresh_node_id_back (counter : u64) : result u64 = u64_add counter 1
 
 (** [betree_main::betree::NodeIdCounter::{0}::new] *)
 let betree_node_id_counter_new_fwd : result betree_node_id_counter_t =
@@ -99,22 +89,10 @@ let betree_upsert_update_fwd
       begin match u64_sub core_num_u64_max_c prev0 with
       | Fail e -> Fail e
       | Return margin ->
-        if margin >= v
-        then
-          begin match u64_add prev0 v with
-          | Fail e -> Fail e
-          | Return i -> Return i
-          end
-        else Return core_num_u64_max_c
+        if margin >= v then u64_add prev0 v else Return core_num_u64_max_c
       end
     | BetreeUpsertFunStateSub v ->
-      if prev0 >= v
-      then
-        begin match u64_sub prev0 v with
-        | Fail e -> Fail e
-        | Return i -> Return i
-        end
-      else Return 0
+      if prev0 >= v then u64_sub prev0 v else Return 0
     end
   end
 
@@ -127,11 +105,7 @@ let rec betree_list_len_fwd
   | BetreeListCons x tl ->
     begin match betree_list_len_fwd t tl with
     | Fail e -> Fail e
-    | Return i ->
-      begin match u64_add 1 i with
-      | Fail e -> Fail e
-      | Return i0 -> Return i0
-      end
+    | Return i -> u64_add 1 i
     end
   | BetreeListNil -> Return 0
   end
@@ -299,11 +273,7 @@ let betree_leaf_split_back
               begin match betree_store_leaf_node_fwd id1 content1 st0 with
               | Fail e -> Fail e
               | Return (_, _) ->
-                begin match betree_node_id_counter_fresh_id_back node_id_cnt0
-                  with
-                | Fail e -> Fail e
-                | Return node_id_cnt1 -> Return node_id_cnt1
-                end
+                betree_node_id_counter_fresh_id_back node_id_cnt0
               end
             end
           end
@@ -326,11 +296,7 @@ let rec betree_node_lookup_in_bindings_fwd
     else
       if i > key
       then Return None
-      else
-        begin match betree_node_lookup_in_bindings_fwd key tl with
-        | Fail e -> Fail e
-        | Return opt -> Return opt
-        end
+      else betree_node_lookup_in_bindings_fwd key tl
   | BetreeListNil -> Return None
   end
 
@@ -345,12 +311,7 @@ let rec betree_node_lookup_first_message_for_key_fwd
     let (i, m) = x in
     if i >= key
     then Return (BetreeListCons (i, m) next_msgs)
-    else
-      begin match betree_node_lookup_first_message_for_key_fwd key next_msgs
-        with
-      | Fail e -> Fail e
-      | Return l -> Return l
-      end
+    else betree_node_lookup_first_message_for_key_fwd key next_msgs
   | BetreeListNil -> Return BetreeListNil
   end
 
@@ -402,11 +363,7 @@ let rec betree_node_apply_upserts_fwd
               betree_list_pop_front_back (u64 & betree_message_t) msgs with
             | Fail e -> Fail e
             | Return msgs0 ->
-              begin match betree_node_apply_upserts_fwd msgs0 (Some v) key st
-                with
-              | Fail e -> Fail e
-              | Return (st0, i) -> Return (st0, i)
-              end
+              betree_node_apply_upserts_fwd msgs0 (Some v) key st
             end
           end
         end
@@ -451,11 +408,7 @@ let rec betree_node_apply_upserts_back
               betree_list_pop_front_back (u64 & betree_message_t) msgs with
             | Fail e -> Fail e
             | Return msgs0 ->
-              begin match betree_node_apply_upserts_back msgs0 (Some v) key st
-                with
-              | Fail e -> Fail e
-              | Return msgs1 -> Return msgs1
-              end
+              betree_node_apply_upserts_back msgs0 (Some v) key st
             end
           end
         end
@@ -464,12 +417,8 @@ let rec betree_node_apply_upserts_back
       begin match core_option_option_unwrap_fwd u64 prev st with
       | Fail e -> Fail e
       | Return (_, v) ->
-        begin match
-          betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
-            BetreeMessageInsert v) with
-        | Fail e -> Fail e
-        | Return msgs0 -> Return msgs0
-        end
+        betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
+          BetreeMessageInsert v)
       end
   end
 
@@ -695,16 +644,8 @@ and betree_internal_lookup_in_children_fwd
   (decreases (betree_internal_lookup_in_children_decreases self key st))
   =
   if key < self.betree_internal_pivot
-  then
-    begin match betree_node_lookup_fwd self.betree_internal_left key st with
-    | Fail e -> Fail e
-    | Return (st0, opt) -> Return (st0, opt)
-    end
-  else
-    begin match betree_node_lookup_fwd self.betree_internal_right key st with
-    | Fail e -> Fail e
-    | Return (st0, opt) -> Return (st0, opt)
-    end
+  then betree_node_lookup_fwd self.betree_internal_left key st
+  else betree_node_lookup_fwd self.betree_internal_right key st
 
 (** [betree_main::betree::Internal::{4}::lookup_in_children] *)
 and betree_internal_lookup_in_children_back
@@ -739,11 +680,7 @@ let rec betree_node_lookup_mut_in_bindings_fwd
     let (i, i0) = hd in
     if i >= key
     then Return (BetreeListCons (i, i0) tl)
-    else
-      begin match betree_node_lookup_mut_in_bindings_fwd key tl with
-      | Fail e -> Fail e
-      | Return l -> Return l
-      end
+    else betree_node_lookup_mut_in_bindings_fwd key tl
   | BetreeListNil -> Return BetreeListNil
   end
 
@@ -794,24 +731,14 @@ let betree_node_apply_to_leaf_fwd_back
                 with
               | Fail e -> Fail e
               | Return bindings2 ->
-                begin match
-                  betree_node_lookup_mut_in_bindings_back key bindings
-                    bindings2 with
-                | Fail e -> Fail e
-                | Return bindings3 -> Return bindings3
-                end
+                betree_node_lookup_mut_in_bindings_back key bindings bindings2
               end
             end
           | BetreeMessageDelete ->
             begin match betree_list_pop_front_back (u64 & u64) bindings0 with
             | Fail e -> Fail e
             | Return bindings1 ->
-              begin match
-                betree_node_lookup_mut_in_bindings_back key bindings bindings1
-                with
-              | Fail e -> Fail e
-              | Return bindings2 -> Return bindings2
-              end
+              betree_node_lookup_mut_in_bindings_back key bindings bindings1
             end
           | BetreeMessageUpsert s ->
             let (_, i) = hd in
@@ -826,12 +753,8 @@ let betree_node_apply_to_leaf_fwd_back
                     v) with
                 | Fail e -> Fail e
                 | Return bindings2 ->
-                  begin match
-                    betree_node_lookup_mut_in_bindings_back key bindings
-                      bindings2 with
-                  | Fail e -> Fail e
-                  | Return bindings3 -> Return bindings3
-                  end
+                  betree_node_lookup_mut_in_bindings_back key bindings
+                    bindings2
                 end
               end
             end
@@ -844,19 +767,10 @@ let betree_node_apply_to_leaf_fwd_back
             betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) with
           | Fail e -> Fail e
           | Return bindings1 ->
-            begin match
-              betree_node_lookup_mut_in_bindings_back key bindings bindings1
-              with
-            | Fail e -> Fail e
-            | Return bindings2 -> Return bindings2
-            end
+            betree_node_lookup_mut_in_bindings_back key bindings bindings1
           end
         | BetreeMessageDelete ->
-          begin match
-            betree_node_lookup_mut_in_bindings_back key bindings bindings0 with
-          | Fail e -> Fail e
-          | Return bindings1 -> Return bindings1
-          end
+          betree_node_lookup_mut_in_bindings_back key bindings bindings0
         | BetreeMessageUpsert s ->
           begin match betree_upsert_update_fwd None s with
           | Fail e -> Fail e
@@ -866,12 +780,7 @@ let betree_node_apply_to_leaf_fwd_back
               with
             | Fail e -> Fail e
             | Return bindings1 ->
-              begin match
-                betree_node_lookup_mut_in_bindings_back key bindings bindings1
-                with
-              | Fail e -> Fail e
-              | Return bindings2 -> Return bindings2
-              end
+              betree_node_lookup_mut_in_bindings_back key bindings bindings1
             end
           end
         end
@@ -891,11 +800,7 @@ let rec betree_node_apply_messages_to_leaf_fwd_back
     begin match betree_node_apply_to_leaf_fwd_back bindings i m with
     | Fail e -> Fail e
     | Return bindings0 ->
-      begin match
-        betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl with
-      | Fail e -> Fail e
-      | Return bindings1 -> Return bindings1
-      end
+      betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
     end
   | BetreeListNil -> Return bindings
   end
@@ -915,11 +820,7 @@ let rec betree_node_filter_messages_for_key_fwd_back
         betree_list_pop_front_back (u64 & betree_message_t) (BetreeListCons (k,
           m) l) with
       | Fail e -> Fail e
-      | Return msgs0 ->
-        begin match betree_node_filter_messages_for_key_fwd_back key msgs0 with
-        | Fail e -> Fail e
-        | Return msgs1 -> Return msgs1
-        end
+      | Return msgs0 -> betree_node_filter_messages_for_key_fwd_back key msgs0
       end
     else Return (BetreeListCons (k, m) l)
   | BetreeListNil -> Return BetreeListNil
@@ -935,12 +836,7 @@ let rec betree_node_lookup_first_message_after_key_fwd
   | BetreeListCons p next_msgs ->
     let (k, m) = p in
     if k = key
-    then
-      begin match betree_node_lookup_first_message_after_key_fwd key next_msgs
-        with
-      | Fail e -> Fail e
-      | Return l -> Return l
-      end
+    then betree_node_lookup_first_message_after_key_fwd key next_msgs
     else Return (BetreeListCons (k, m) next_msgs)
   | BetreeListNil -> Return BetreeListNil
   end
@@ -991,12 +887,7 @@ let betree_node_apply_to_internal_fwd_back
                 (key, BetreeMessageInsert i) with
             | Fail e -> Fail e
             | Return msgs2 ->
-              begin match
-                betree_node_lookup_first_message_for_key_back key msgs msgs2
-                with
-              | Fail e -> Fail e
-              | Return msgs3 -> Return msgs3
-              end
+              betree_node_lookup_first_message_for_key_back key msgs msgs2
             end
           end
         | BetreeMessageDelete ->
@@ -1009,12 +900,7 @@ let betree_node_apply_to_internal_fwd_back
                 (key, BetreeMessageDelete) with
             | Fail e -> Fail e
             | Return msgs2 ->
-              begin match
-                betree_node_lookup_first_message_for_key_back key msgs msgs2
-                with
-              | Fail e -> Fail e
-              | Return msgs3 -> Return msgs3
-              end
+              betree_node_lookup_first_message_for_key_back key msgs msgs2
             end
           end
         | BetreeMessageUpsert s ->
@@ -1037,12 +923,8 @@ let betree_node_apply_to_internal_fwd_back
                       msgs1 (key, BetreeMessageInsert v) with
                   | Fail e -> Fail e
                   | Return msgs2 ->
-                    begin match
-                      betree_node_lookup_first_message_for_key_back key msgs
-                        msgs2 with
-                    | Fail e -> Fail e
-                    | Return msgs3 -> Return msgs3
-                    end
+                    betree_node_lookup_first_message_for_key_back key msgs
+                      msgs2
                   end
                 end
               end
@@ -1060,12 +942,8 @@ let betree_node_apply_to_internal_fwd_back
                       msgs1 (key, BetreeMessageInsert v) with
                   | Fail e -> Fail e
                   | Return msgs2 ->
-                    begin match
-                      betree_node_lookup_first_message_for_key_back key msgs
-                        msgs2 with
-                    | Fail e -> Fail e
-                    | Return msgs3 -> Return msgs3
-                    end
+                    betree_node_lookup_first_message_for_key_back key msgs
+                      msgs2
                   end
                 end
               end
@@ -1084,12 +962,8 @@ let betree_node_apply_to_internal_fwd_back
                       msgs2 with
                   | Fail e -> Fail e
                   | Return msgs3 ->
-                    begin match
-                      betree_node_lookup_first_message_for_key_back key msgs
-                        msgs3 with
-                    | Fail e -> Fail e
-                    | Return msgs4 -> Return msgs4
-                    end
+                    betree_node_lookup_first_message_for_key_back key msgs
+                      msgs3
                   end
                 end
               end
@@ -1102,11 +976,7 @@ let betree_node_apply_to_internal_fwd_back
             new_msg) with
         | Fail e -> Fail e
         | Return msgs1 ->
-          begin match
-            betree_node_lookup_first_message_for_key_back key msgs msgs1 with
-          | Fail e -> Fail e
-          | Return msgs2 -> Return msgs2
-          end
+          betree_node_lookup_first_message_for_key_back key msgs msgs1
         end
     end
   end
@@ -1124,11 +994,7 @@ let rec betree_node_apply_messages_to_internal_fwd_back
     begin match betree_node_apply_to_internal_fwd_back msgs i m with
     | Fail e -> Fail e
     | Return msgs0 ->
-      begin match
-        betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl with
-      | Fail e -> Fail e
-      | Return msgs1 -> Return msgs1
-      end
+      betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl
     end
   | BetreeListNil -> Return msgs
   end
@@ -1484,12 +1350,8 @@ let betree_node_apply_back
   result (betree_node_t & betree_node_id_counter_t)
   =
   let l = BetreeListNil in
-  begin match
-    betree_node_apply_messages_back self params node_id_cnt (BetreeListCons
-      (key, new_msg) l) st with
-  | Fail e -> Fail e
-  | Return (self0, node_id_cnt0) -> Return (self0, node_id_cnt0)
-  end
+  betree_node_apply_messages_back self params node_id_cnt (BetreeListCons (key,
+    new_msg) l) st
 
 (** [betree_main::betree::BeTree::{6}::new] *)
 let betree_be_tree_new_fwd
@@ -1568,11 +1430,7 @@ let betree_be_tree_insert_back
   (self : betree_be_tree_t) (key : u64) (value : u64) (st : state) :
   result betree_be_tree_t
   =
-  begin match betree_be_tree_apply_back self key (BetreeMessageInsert value) st
-    with
-  | Fail e -> Fail e
-  | Return self0 -> Return self0
-  end
+  betree_be_tree_apply_back self key (BetreeMessageInsert value) st
 
 (** [betree_main::betree::BeTree::{6}::delete] *)
 let betree_be_tree_delete_fwd
@@ -1591,10 +1449,7 @@ let betree_be_tree_delete_back
   (self : betree_be_tree_t) (key : u64) (st : state) :
   result betree_be_tree_t
   =
-  begin match betree_be_tree_apply_back self key BetreeMessageDelete st with
-  | Fail e -> Fail e
-  | Return self0 -> Return self0
-  end
+  betree_be_tree_apply_back self key BetreeMessageDelete st
 
 (** [betree_main::betree::BeTree::{6}::upsert] *)
 let betree_be_tree_upsert_fwd
@@ -1619,21 +1474,14 @@ let betree_be_tree_upsert_back
   (st : state) :
   result betree_be_tree_t
   =
-  begin match betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st
-    with
-  | Fail e -> Fail e
-  | Return self0 -> Return self0
-  end
+  betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st
 
 (** [betree_main::betree::BeTree::{6}::lookup] *)
 let betree_be_tree_lookup_fwd
   (self : betree_be_tree_t) (key : u64) (st : state) :
   result (state & (option u64))
   =
-  begin match betree_node_lookup_fwd self.betree_be_tree_root key st with
-  | Fail e -> Fail e
-  | Return (st0, opt) -> Return (st0, opt)
-  end
+  betree_node_lookup_fwd self.betree_be_tree_root key st
 
 (** [betree_main::betree::BeTree::{6}::lookup] *)
 let betree_be_tree_lookup_back
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 1560624b..c06a6b9e 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -13,10 +13,7 @@ let betree_load_internal_node_fwd
   (id : u64) (st : state) :
   result (state & (betree_list_t (u64 & betree_message_t)))
   =
-  begin match betree_utils_load_internal_node_fwd id st with
-  | Fail e -> Fail e
-  | Return (st0, l) -> Return (st0, l)
-  end
+  betree_utils_load_internal_node_fwd id st
 
 (** [betree_main::betree::store_internal_node] *)
 let betree_store_internal_node_fwd
@@ -31,10 +28,7 @@ let betree_store_internal_node_fwd
 (** [betree_main::betree::load_leaf_node] *)
 let betree_load_leaf_node_fwd
   (id : u64) (st : state) : result (state & (betree_list_t (u64 & u64))) =
-  begin match betree_utils_load_leaf_node_fwd id st with
-  | Fail e -> Fail e
-  | Return (st0, l) -> Return (st0, l)
-  end
+  betree_utils_load_leaf_node_fwd id st
 
 (** [betree_main::betree::store_leaf_node] *)
 let betree_store_leaf_node_fwd
@@ -54,11 +48,7 @@ let betree_fresh_node_id_fwd (counter : u64) : result u64 =
   end
 
 (** [betree_main::betree::fresh_node_id] *)
-let betree_fresh_node_id_back (counter : u64) : result u64 =
-  begin match u64_add counter 1 with
-  | Fail e -> Fail e
-  | Return counter0 -> Return counter0
-  end
+let betree_fresh_node_id_back (counter : u64) : result u64 = u64_add counter 1
 
 (** [betree_main::betree::NodeIdCounter::{0}::new] *)
 let betree_node_id_counter_new_fwd : result betree_node_id_counter_t =
@@ -99,22 +89,10 @@ let betree_upsert_update_fwd
       begin match u64_sub core_num_u64_max_c prev0 with
       | Fail e -> Fail e
       | Return margin ->
-        if margin >= v
-        then
-          begin match u64_add prev0 v with
-          | Fail e -> Fail e
-          | Return i -> Return i
-          end
-        else Return core_num_u64_max_c
+        if margin >= v then u64_add prev0 v else Return core_num_u64_max_c
       end
     | BetreeUpsertFunStateSub v ->
-      if prev0 >= v
-      then
-        begin match u64_sub prev0 v with
-        | Fail e -> Fail e
-        | Return i -> Return i
-        end
-      else Return 0
+      if prev0 >= v then u64_sub prev0 v else Return 0
     end
   end
 
@@ -127,11 +105,7 @@ let rec betree_list_len_fwd
   | BetreeListCons x tl ->
     begin match betree_list_len_fwd t tl with
     | Fail e -> Fail e
-    | Return i ->
-      begin match u64_add 1 i with
-      | Fail e -> Fail e
-      | Return i0 -> Return i0
-      end
+    | Return i -> u64_add 1 i
     end
   | BetreeListNil -> Return 0
   end
@@ -404,11 +378,7 @@ let rec betree_node_lookup_in_bindings_fwd
     else
       if i > key
       then Return None
-      else
-        begin match betree_node_lookup_in_bindings_fwd key tl with
-        | Fail e -> Fail e
-        | Return opt -> Return opt
-        end
+      else betree_node_lookup_in_bindings_fwd key tl
   | BetreeListNil -> Return None
   end
 
@@ -423,12 +393,7 @@ let rec betree_node_lookup_first_message_for_key_fwd
     let (i, m) = x in
     if i >= key
     then Return (BetreeListCons (i, m) next_msgs)
-    else
-      begin match betree_node_lookup_first_message_for_key_fwd key next_msgs
-        with
-      | Fail e -> Fail e
-      | Return l -> Return l
-      end
+    else betree_node_lookup_first_message_for_key_fwd key next_msgs
   | BetreeListNil -> Return BetreeListNil
   end
 
@@ -480,11 +445,7 @@ let rec betree_node_apply_upserts_fwd
               betree_list_pop_front_back (u64 & betree_message_t) msgs with
             | Fail e -> Fail e
             | Return msgs0 ->
-              begin match betree_node_apply_upserts_fwd msgs0 (Some v) key st
-                with
-              | Fail e -> Fail e
-              | Return (st0, i) -> Return (st0, i)
-              end
+              betree_node_apply_upserts_fwd msgs0 (Some v) key st
             end
           end
         end
@@ -529,11 +490,7 @@ let rec betree_node_apply_upserts_back
               betree_list_pop_front_back (u64 & betree_message_t) msgs with
             | Fail e -> Fail e
             | Return msgs0 ->
-              begin match
-                betree_node_apply_upserts_back msgs0 (Some v) key st st0 with
-              | Fail e -> Fail e
-              | Return (st1, msgs1) -> Return (st1, msgs1)
-              end
+              betree_node_apply_upserts_back msgs0 (Some v) key st st0
             end
           end
         end
@@ -776,16 +733,8 @@ and betree_internal_lookup_in_children_fwd
   (decreases (betree_internal_lookup_in_children_decreases self key st))
   =
   if key < self.betree_internal_pivot
-  then
-    begin match betree_node_lookup_fwd self.betree_internal_left key st with
-    | Fail e -> Fail e
-    | Return (st0, opt) -> Return (st0, opt)
-    end
-  else
-    begin match betree_node_lookup_fwd self.betree_internal_right key st with
-    | Fail e -> Fail e
-    | Return (st0, opt) -> Return (st0, opt)
-    end
+  then betree_node_lookup_fwd self.betree_internal_left key st
+  else betree_node_lookup_fwd self.betree_internal_right key st
 
 (** [betree_main::betree::Internal::{4}::lookup_in_children] *)
 and betree_internal_lookup_in_children_back
@@ -822,11 +771,7 @@ let rec betree_node_lookup_mut_in_bindings_fwd
     let (i, i0) = hd in
     if i >= key
     then Return (BetreeListCons (i, i0) tl)
-    else
-      begin match betree_node_lookup_mut_in_bindings_fwd key tl with
-      | Fail e -> Fail e
-      | Return l -> Return l
-      end
+    else betree_node_lookup_mut_in_bindings_fwd key tl
   | BetreeListNil -> Return BetreeListNil
   end
 
@@ -877,24 +822,14 @@ let betree_node_apply_to_leaf_fwd_back
                 with
               | Fail e -> Fail e
               | Return bindings2 ->
-                begin match
-                  betree_node_lookup_mut_in_bindings_back key bindings
-                    bindings2 with
-                | Fail e -> Fail e
-                | Return bindings3 -> Return bindings3
-                end
+                betree_node_lookup_mut_in_bindings_back key bindings bindings2
               end
             end
           | BetreeMessageDelete ->
             begin match betree_list_pop_front_back (u64 & u64) bindings0 with
             | Fail e -> Fail e
             | Return bindings1 ->
-              begin match
-                betree_node_lookup_mut_in_bindings_back key bindings bindings1
-                with
-              | Fail e -> Fail e
-              | Return bindings2 -> Return bindings2
-              end
+              betree_node_lookup_mut_in_bindings_back key bindings bindings1
             end
           | BetreeMessageUpsert s ->
             let (_, i) = hd in
@@ -909,12 +844,8 @@ let betree_node_apply_to_leaf_fwd_back
                     v) with
                 | Fail e -> Fail e
                 | Return bindings2 ->
-                  begin match
-                    betree_node_lookup_mut_in_bindings_back key bindings
-                      bindings2 with
-                  | Fail e -> Fail e
-                  | Return bindings3 -> Return bindings3
-                  end
+                  betree_node_lookup_mut_in_bindings_back key bindings
+                    bindings2
                 end
               end
             end
@@ -927,19 +858,10 @@ let betree_node_apply_to_leaf_fwd_back
             betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) with
           | Fail e -> Fail e
           | Return bindings1 ->
-            begin match
-              betree_node_lookup_mut_in_bindings_back key bindings bindings1
-              with
-            | Fail e -> Fail e
-            | Return bindings2 -> Return bindings2
-            end
+            betree_node_lookup_mut_in_bindings_back key bindings bindings1
           end
         | BetreeMessageDelete ->
-          begin match
-            betree_node_lookup_mut_in_bindings_back key bindings bindings0 with
-          | Fail e -> Fail e
-          | Return bindings1 -> Return bindings1
-          end
+          betree_node_lookup_mut_in_bindings_back key bindings bindings0
         | BetreeMessageUpsert s ->
           begin match betree_upsert_update_fwd None s with
           | Fail e -> Fail e
@@ -949,12 +871,7 @@ let betree_node_apply_to_leaf_fwd_back
               with
             | Fail e -> Fail e
             | Return bindings1 ->
-              begin match
-                betree_node_lookup_mut_in_bindings_back key bindings bindings1
-                with
-              | Fail e -> Fail e
-              | Return bindings2 -> Return bindings2
-              end
+              betree_node_lookup_mut_in_bindings_back key bindings bindings1
             end
           end
         end
@@ -974,11 +891,7 @@ let rec betree_node_apply_messages_to_leaf_fwd_back
     begin match betree_node_apply_to_leaf_fwd_back bindings i m with
     | Fail e -> Fail e
     | Return bindings0 ->
-      begin match
-        betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl with
-      | Fail e -> Fail e
-      | Return bindings1 -> Return bindings1
-      end
+      betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
     end
   | BetreeListNil -> Return bindings
   end
@@ -998,11 +911,7 @@ let rec betree_node_filter_messages_for_key_fwd_back
         betree_list_pop_front_back (u64 & betree_message_t) (BetreeListCons (k,
           m) l) with
       | Fail e -> Fail e
-      | Return msgs0 ->
-        begin match betree_node_filter_messages_for_key_fwd_back key msgs0 with
-        | Fail e -> Fail e
-        | Return msgs1 -> Return msgs1
-        end
+      | Return msgs0 -> betree_node_filter_messages_for_key_fwd_back key msgs0
       end
     else Return (BetreeListCons (k, m) l)
   | BetreeListNil -> Return BetreeListNil
@@ -1018,12 +927,7 @@ let rec betree_node_lookup_first_message_after_key_fwd
   | BetreeListCons p next_msgs ->
     let (k, m) = p in
     if k = key
-    then
-      begin match betree_node_lookup_first_message_after_key_fwd key next_msgs
-        with
-      | Fail e -> Fail e
-      | Return l -> Return l
-      end
+    then betree_node_lookup_first_message_after_key_fwd key next_msgs
     else Return (BetreeListCons (k, m) next_msgs)
   | BetreeListNil -> Return BetreeListNil
   end
@@ -1074,12 +978,7 @@ let betree_node_apply_to_internal_fwd_back
                 (key, BetreeMessageInsert i) with
             | Fail e -> Fail e
             | Return msgs2 ->
-              begin match
-                betree_node_lookup_first_message_for_key_back key msgs msgs2
-                with
-              | Fail e -> Fail e
-              | Return msgs3 -> Return msgs3
-              end
+              betree_node_lookup_first_message_for_key_back key msgs msgs2
             end
           end
         | BetreeMessageDelete ->
@@ -1092,12 +991,7 @@ let betree_node_apply_to_internal_fwd_back
                 (key, BetreeMessageDelete) with
             | Fail e -> Fail e
             | Return msgs2 ->
-              begin match
-                betree_node_lookup_first_message_for_key_back key msgs msgs2
-                with
-              | Fail e -> Fail e
-              | Return msgs3 -> Return msgs3
-              end
+              betree_node_lookup_first_message_for_key_back key msgs msgs2
             end
           end
         | BetreeMessageUpsert s ->
@@ -1120,12 +1014,8 @@ let betree_node_apply_to_internal_fwd_back
                       msgs1 (key, BetreeMessageInsert v) with
                   | Fail e -> Fail e
                   | Return msgs2 ->
-                    begin match
-                      betree_node_lookup_first_message_for_key_back key msgs
-                        msgs2 with
-                    | Fail e -> Fail e
-                    | Return msgs3 -> Return msgs3
-                    end
+                    betree_node_lookup_first_message_for_key_back key msgs
+                      msgs2
                   end
                 end
               end
@@ -1143,12 +1033,8 @@ let betree_node_apply_to_internal_fwd_back
                       msgs1 (key, BetreeMessageInsert v) with
                   | Fail e -> Fail e
                   | Return msgs2 ->
-                    begin match
-                      betree_node_lookup_first_message_for_key_back key msgs
-                        msgs2 with
-                    | Fail e -> Fail e
-                    | Return msgs3 -> Return msgs3
-                    end
+                    betree_node_lookup_first_message_for_key_back key msgs
+                      msgs2
                   end
                 end
               end
@@ -1167,12 +1053,8 @@ let betree_node_apply_to_internal_fwd_back
                       msgs2 with
                   | Fail e -> Fail e
                   | Return msgs3 ->
-                    begin match
-                      betree_node_lookup_first_message_for_key_back key msgs
-                        msgs3 with
-                    | Fail e -> Fail e
-                    | Return msgs4 -> Return msgs4
-                    end
+                    betree_node_lookup_first_message_for_key_back key msgs
+                      msgs3
                   end
                 end
               end
@@ -1185,11 +1067,7 @@ let betree_node_apply_to_internal_fwd_back
             new_msg) with
         | Fail e -> Fail e
         | Return msgs1 ->
-          begin match
-            betree_node_lookup_first_message_for_key_back key msgs msgs1 with
-          | Fail e -> Fail e
-          | Return msgs2 -> Return msgs2
-          end
+          betree_node_lookup_first_message_for_key_back key msgs msgs1
         end
     end
   end
@@ -1207,11 +1085,7 @@ let rec betree_node_apply_messages_to_internal_fwd_back
     begin match betree_node_apply_to_internal_fwd_back msgs i m with
     | Fail e -> Fail e
     | Return msgs0 ->
-      begin match
-        betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl with
-      | Fail e -> Fail e
-      | Return msgs1 -> Return msgs1
-      end
+      betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl
     end
   | BetreeListNil -> Return msgs
   end
@@ -1291,12 +1165,8 @@ let rec betree_node_apply_messages_fwd
                     st1 with
                 | Fail e -> Fail e
                 | Return (st2, _) ->
-                  begin match
-                    betree_leaf_split_back0 node content0 params node_id_cnt
-                      st0 st2 with
-                  | Fail e -> Fail e
-                  | Return (st3, ()) -> Return (st3, ())
-                  end
+                  betree_leaf_split_back0 node content0 params node_id_cnt st0
+                    st2
                 end
               end
             else
@@ -1457,12 +1327,8 @@ and betree_node_apply_messages_back1
                     content1 st3 with
                 | Fail e -> Fail e
                 | Return (_, _) ->
-                  begin match
-                    betree_internal_flush_back1 node params node_id_cnt
-                      content0 st1 st0 with
-                  | Fail e -> Fail e
-                  | Return (st4, ()) -> Return (st4, ())
-                  end
+                  betree_internal_flush_back1 node params node_id_cnt content0
+                    st1 st0
                 end
               end
             end
@@ -1505,12 +1371,8 @@ and betree_node_apply_messages_back1
                       st1 st3 with
                   | Fail e -> Fail e
                   | Return (_, ()) ->
-                    begin match
-                      betree_leaf_split_back1 node content0 params node_id_cnt
-                        st1 st0 with
-                    | Fail e -> Fail e
-                    | Return (st4, ()) -> Return (st4, ())
-                    end
+                    betree_leaf_split_back1 node content0 params node_id_cnt
+                      st1 st0
                   end
                 end
               end
@@ -1820,12 +1682,8 @@ let betree_node_apply_fwd
         (key, new_msg) l) st st0 with
     | Fail e -> Fail e
     | Return (st1, (_, _)) ->
-      begin match
-        betree_node_apply_messages_back1 self params node_id_cnt
-          (BetreeListCons (key, new_msg) l) st st1 with
-      | Fail e -> Fail e
-      | Return (st2, ()) -> Return (st2, ())
-      end
+      betree_node_apply_messages_back1 self params node_id_cnt (BetreeListCons
+        (key, new_msg) l) st st1
     end
   end
 
@@ -1923,13 +1781,9 @@ let betree_be_tree_apply_fwd
         st0 with
     | Fail e -> Fail e
     | Return (st1, (_, _)) ->
-      begin match
-        betree_node_apply_back1 self.betree_be_tree_root
-          self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
-          st1 with
-      | Fail e -> Fail e
-      | Return (st2, ()) -> Return (st2, ())
-      end
+      betree_node_apply_back1 self.betree_be_tree_root
+        self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
+        st1
     end
   end
 
@@ -2063,10 +1917,7 @@ let betree_be_tree_lookup_fwd
   (self : betree_be_tree_t) (key : u64) (st : state) :
   result (state & (option u64))
   =
-  begin match betree_node_lookup_fwd self.betree_be_tree_root key st with
-  | Fail e -> Fail e
-  | Return (st0, opt) -> Return (st0, opt)
-  end
+  betree_node_lookup_fwd self.betree_be_tree_root key st
 
 (** [betree_main::betree::BeTree::{6}::lookup] *)
 let betree_be_tree_lookup_back
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index e3ae587f..59c4e125 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -24,11 +24,7 @@ let rec hash_map_allocate_slots_fwd
     | Return slots0 ->
       begin match usize_sub n 1 with
       | Fail e -> Fail e
-      | Return i ->
-        begin match hash_map_allocate_slots_fwd t slots0 i with
-        | Fail e -> Fail e
-        | Return v -> Return v
-        end
+      | Return i -> hash_map_allocate_slots_fwd t slots0 i
       end
     end
 
@@ -55,10 +51,7 @@ let hash_map_new_with_capacity_fwd
 
 (** [hashmap::HashMap::{0}::new] *)
 let hash_map_new_fwd (t : Type0) : result (hash_map_t t) =
-  begin match hash_map_new_with_capacity_fwd t 32 4 5 with
-  | Fail e -> Fail e
-  | Return hm -> Return hm
-  end
+  hash_map_new_with_capacity_fwd t 32 4 5
 
 (** [hashmap::HashMap::{0}::clear_slots] *)
 let rec hash_map_clear_slots_fwd_back
@@ -74,11 +67,7 @@ let rec hash_map_clear_slots_fwd_back
     | Return slots0 ->
       begin match usize_add i 1 with
       | Fail e -> Fail e
-      | Return i1 ->
-        begin match hash_map_clear_slots_fwd_back t slots0 i1 with
-        | Fail e -> Fail e
-        | Return slots1 -> Return slots1
-        end
+      | Return i1 -> hash_map_clear_slots_fwd_back t slots0 i1
       end
     end
   else Return slots
@@ -107,11 +96,7 @@ let rec hash_map_insert_in_list_fwd
   | ListCons ckey cvalue ls0 ->
     if ckey = key
     then Return false
-    else
-      begin match hash_map_insert_in_list_fwd t key value ls0 with
-      | Fail e -> Fail e
-      | Return b -> Return b
-      end
+    else hash_map_insert_in_list_fwd t key value ls0
   | ListNil -> Return true
   end
 
@@ -202,11 +187,7 @@ let rec hash_map_move_elements_from_list_fwd_back
   | ListCons k v tl ->
     begin match hash_map_insert_no_resize_fwd_back t ntable k v with
     | Fail e -> Fail e
-    | Return ntable0 ->
-      begin match hash_map_move_elements_from_list_fwd_back t ntable0 tl with
-      | Fail e -> Fail e
-      | Return ntable1 -> Return ntable1
-      end
+    | Return ntable0 -> hash_map_move_elements_from_list_fwd_back t ntable0 tl
     end
   | ListNil -> Return ntable
   end
@@ -233,12 +214,7 @@ let rec hash_map_move_elements_fwd_back
         | Return slots0 ->
           begin match usize_add i 1 with
           | Fail e -> Fail e
-          | Return i1 ->
-            begin match hash_map_move_elements_fwd_back t ntable0 slots0 i1
-              with
-            | Fail e -> Fail e
-            | Return (ntable1, slots1) -> Return (ntable1, slots1)
-            end
+          | Return i1 -> hash_map_move_elements_fwd_back t ntable0 slots0 i1
           end
         end
       end
@@ -296,11 +272,7 @@ let hash_map_insert_fwd_back
     | Fail e -> Fail e
     | Return i ->
       if i > self0.hash_map_max_load
-      then
-        begin match hash_map_try_resize_fwd_back t self0 with
-        | Fail e -> Fail e
-        | Return self1 -> Return self1
-        end
+      then hash_map_try_resize_fwd_back t self0
       else Return self0
     end
   end
@@ -315,11 +287,7 @@ let rec hash_map_contains_key_in_list_fwd
   | ListCons ckey x ls0 ->
     if ckey = key
     then Return true
-    else
-      begin match hash_map_contains_key_in_list_fwd t key ls0 with
-      | Fail e -> Fail e
-      | Return b -> Return b
-      end
+    else hash_map_contains_key_in_list_fwd t key ls0
   | ListNil -> Return false
   end
 
@@ -335,11 +303,7 @@ let hash_map_contains_key_fwd
     | Return hash_mod ->
       begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with
       | Fail e -> Fail e
-      | Return l ->
-        begin match hash_map_contains_key_in_list_fwd t key l with
-        | Fail e -> Fail e
-        | Return b -> Return b
-        end
+      | Return l -> hash_map_contains_key_in_list_fwd t key l
       end
     end
   end
@@ -351,13 +315,7 @@ let rec hash_map_get_in_list_fwd
   =
   begin match ls with
   | ListCons ckey cvalue ls0 ->
-    if ckey = key
-    then Return cvalue
-    else
-      begin match hash_map_get_in_list_fwd t key ls0 with
-      | Fail e -> Fail e
-      | Return x -> Return x
-      end
+    if ckey = key then Return cvalue else hash_map_get_in_list_fwd t key ls0
   | ListNil -> Fail Failure
   end
 
@@ -373,11 +331,7 @@ let hash_map_get_fwd
     | Return hash_mod ->
       begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with
       | Fail e -> Fail e
-      | Return l ->
-        begin match hash_map_get_in_list_fwd t key l with
-        | Fail e -> Fail e
-        | Return x -> Return x
-        end
+      | Return l -> hash_map_get_in_list_fwd t key l
       end
     end
   end
@@ -391,11 +345,7 @@ let rec hash_map_get_mut_in_list_fwd
   | ListCons ckey cvalue ls0 ->
     if ckey = key
     then Return cvalue
-    else
-      begin match hash_map_get_mut_in_list_fwd t key ls0 with
-      | Fail e -> Fail e
-      | Return x -> Return x
-      end
+    else hash_map_get_mut_in_list_fwd t key ls0
   | ListNil -> Fail Failure
   end
 
@@ -430,11 +380,7 @@ let hash_map_get_mut_fwd
       begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
         with
       | Fail e -> Fail e
-      | Return l ->
-        begin match hash_map_get_mut_in_list_fwd t key l with
-        | Fail e -> Fail e
-        | Return x -> Return x
-        end
+      | Return l -> hash_map_get_mut_in_list_fwd t key l
       end
     end
   end
@@ -485,11 +431,7 @@ let rec hash_map_remove_from_list_fwd
       | ListCons i cvalue tl0 -> Return (Some cvalue)
       | ListNil -> Fail Failure
       end
-    else
-      begin match hash_map_remove_from_list_fwd t key tl with
-      | Fail e -> Fail e
-      | Return opt -> Return opt
-      end
+    else hash_map_remove_from_list_fwd t key tl
   | ListNil -> Return None
   end
 
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index d6da4562..c4f2b039 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -25,11 +25,7 @@ let rec hashmap_hash_map_allocate_slots_fwd
     | Return slots0 ->
       begin match usize_sub n 1 with
       | Fail e -> Fail e
-      | Return i ->
-        begin match hashmap_hash_map_allocate_slots_fwd t slots0 i with
-        | Fail e -> Fail e
-        | Return v -> Return v
-        end
+      | Return i -> hashmap_hash_map_allocate_slots_fwd t slots0 i
       end
     end
 
@@ -57,10 +53,7 @@ let hashmap_hash_map_new_with_capacity_fwd
 
 (** [hashmap_main::hashmap::HashMap::{0}::new] *)
 let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) =
-  begin match hashmap_hash_map_new_with_capacity_fwd t 32 4 5 with
-  | Fail e -> Fail e
-  | Return hm -> Return hm
-  end
+  hashmap_hash_map_new_with_capacity_fwd t 32 4 5
 
 (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
 let rec hashmap_hash_map_clear_slots_fwd_back
@@ -77,11 +70,7 @@ let rec hashmap_hash_map_clear_slots_fwd_back
     | Return slots0 ->
       begin match usize_add i 1 with
       | Fail e -> Fail e
-      | Return i1 ->
-        begin match hashmap_hash_map_clear_slots_fwd_back t slots0 i1 with
-        | Fail e -> Fail e
-        | Return slots1 -> Return slots1
-        end
+      | Return i1 -> hashmap_hash_map_clear_slots_fwd_back t slots0 i1
       end
     end
   else Return slots
@@ -112,11 +101,7 @@ let rec hashmap_hash_map_insert_in_list_fwd
   | HashmapListCons ckey cvalue ls0 ->
     if ckey = key
     then Return false
-    else
-      begin match hashmap_hash_map_insert_in_list_fwd t key value ls0 with
-      | Fail e -> Fail e
-      | Return b -> Return b
-      end
+    else hashmap_hash_map_insert_in_list_fwd t key value ls0
   | HashmapListNil -> Return true
   end
 
@@ -213,11 +198,7 @@ let rec hashmap_hash_map_move_elements_from_list_fwd_back
     begin match hashmap_hash_map_insert_no_resize_fwd_back t ntable k v with
     | Fail e -> Fail e
     | Return ntable0 ->
-      begin match
-        hashmap_hash_map_move_elements_from_list_fwd_back t ntable0 tl with
-      | Fail e -> Fail e
-      | Return ntable1 -> Return ntable1
-      end
+      hashmap_hash_map_move_elements_from_list_fwd_back t ntable0 tl
     end
   | HashmapListNil -> Return ntable
   end
@@ -247,11 +228,7 @@ let rec hashmap_hash_map_move_elements_fwd_back
           begin match usize_add i 1 with
           | Fail e -> Fail e
           | Return i1 ->
-            begin match
-              hashmap_hash_map_move_elements_fwd_back t ntable0 slots0 i1 with
-            | Fail e -> Fail e
-            | Return (ntable1, slots1) -> Return (ntable1, slots1)
-            end
+            hashmap_hash_map_move_elements_fwd_back t ntable0 slots0 i1
           end
         end
       end
@@ -310,11 +287,7 @@ let hashmap_hash_map_insert_fwd_back
     | Fail e -> Fail e
     | Return i ->
       if i > self0.hashmap_hash_map_max_load
-      then
-        begin match hashmap_hash_map_try_resize_fwd_back t self0 with
-        | Fail e -> Fail e
-        | Return self1 -> Return self1
-        end
+      then hashmap_hash_map_try_resize_fwd_back t self0
       else Return self0
     end
   end
@@ -329,11 +302,7 @@ let rec hashmap_hash_map_contains_key_in_list_fwd
   | HashmapListCons ckey x ls0 ->
     if ckey = key
     then Return true
-    else
-      begin match hashmap_hash_map_contains_key_in_list_fwd t key ls0 with
-      | Fail e -> Fail e
-      | Return b -> Return b
-      end
+    else hashmap_hash_map_contains_key_in_list_fwd t key ls0
   | HashmapListNil -> Return false
   end
 
@@ -351,11 +320,7 @@ let hashmap_hash_map_contains_key_fwd
         vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
         with
       | Fail e -> Fail e
-      | Return l ->
-        begin match hashmap_hash_map_contains_key_in_list_fwd t key l with
-        | Fail e -> Fail e
-        | Return b -> Return b
-        end
+      | Return l -> hashmap_hash_map_contains_key_in_list_fwd t key l
       end
     end
   end
@@ -369,11 +334,7 @@ let rec hashmap_hash_map_get_in_list_fwd
   | HashmapListCons ckey cvalue ls0 ->
     if ckey = key
     then Return cvalue
-    else
-      begin match hashmap_hash_map_get_in_list_fwd t key ls0 with
-      | Fail e -> Fail e
-      | Return x -> Return x
-      end
+    else hashmap_hash_map_get_in_list_fwd t key ls0
   | HashmapListNil -> Fail Failure
   end
 
@@ -391,11 +352,7 @@ let hashmap_hash_map_get_fwd
         vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
         with
       | Fail e -> Fail e
-      | Return l ->
-        begin match hashmap_hash_map_get_in_list_fwd t key l with
-        | Fail e -> Fail e
-        | Return x -> Return x
-        end
+      | Return l -> hashmap_hash_map_get_in_list_fwd t key l
       end
     end
   end
@@ -410,11 +367,7 @@ let rec hashmap_hash_map_get_mut_in_list_fwd
   | HashmapListCons ckey cvalue ls0 ->
     if ckey = key
     then Return cvalue
-    else
-      begin match hashmap_hash_map_get_mut_in_list_fwd t key ls0 with
-      | Fail e -> Fail e
-      | Return x -> Return x
-      end
+    else hashmap_hash_map_get_mut_in_list_fwd t key ls0
   | HashmapListNil -> Fail Failure
   end
 
@@ -450,11 +403,7 @@ let hashmap_hash_map_get_mut_fwd
         vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
           hash_mod with
       | Fail e -> Fail e
-      | Return l ->
-        begin match hashmap_hash_map_get_mut_in_list_fwd t key l with
-        | Fail e -> Fail e
-        | Return x -> Return x
-        end
+      | Return l -> hashmap_hash_map_get_mut_in_list_fwd t key l
       end
     end
   end
@@ -510,11 +459,7 @@ let rec hashmap_hash_map_remove_from_list_fwd
       | HashmapListCons i cvalue tl0 -> Return (Some cvalue)
       | HashmapListNil -> Fail Failure
       end
-    else
-      begin match hashmap_hash_map_remove_from_list_fwd t key tl with
-      | Fail e -> Fail e
-      | Return opt -> Return opt
-      end
+    else hashmap_hash_map_remove_from_list_fwd t key tl
   | HashmapListNil -> Return None
   end
 
diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst
index a0658206..9b90e9c7 100644
--- a/tests/fstar/misc/Constants.fst
+++ b/tests/fstar/misc/Constants.fst
@@ -22,12 +22,10 @@ let x2_body : result u32 = Return 3
 let x2_c : u32 = eval_global x2_body
 
 (** [constants::incr] *)
-let incr_fwd (n : u32) : result u32 =
-  begin match u32_add n 1 with | Fail e -> Fail e | Return i -> Return i end
+let incr_fwd (n : u32) : result u32 = u32_add n 1
 
 (** [constants::X3] *)
-let x3_body : result u32 =
-  begin match incr_fwd 32 with | Fail e -> Fail e | Return i -> Return i end
+let x3_body : result u32 = incr_fwd 32
 let x3_c : u32 = eval_global x3_body
 
 (** [constants::mk_pair0] *)
@@ -41,19 +39,11 @@ let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) =
   Return (Mkpair_t x y)
 
 (** [constants::P0] *)
-let p0_body : result (u32 & u32) =
-  begin match mk_pair0_fwd 0 1 with
-  | Fail e -> Fail e
-  | Return p -> Return p
-  end
+let p0_body : result (u32 & u32) = mk_pair0_fwd 0 1
 let p0_c : (u32 & u32) = eval_global p0_body
 
 (** [constants::P1] *)
-let p1_body : result (pair_t u32 u32) =
-  begin match mk_pair1_fwd 0 1 with
-  | Fail e -> Fail e
-  | Return p -> Return p
-  end
+let p1_body : result (pair_t u32 u32) = mk_pair1_fwd 0 1
 let p1_c : pair_t u32 u32 = eval_global p1_body
 
 (** [constants::P2] *)
@@ -72,19 +62,14 @@ let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) =
   Return (Mkwrap_t val0)
 
 (** [constants::Y] *)
-let y_body : result (wrap_t i32) =
-  begin match wrap_new_fwd i32 2 with
-  | Fail e -> Fail e
-  | Return w -> Return w
-  end
+let y_body : result (wrap_t i32) = wrap_new_fwd i32 2
 let y_c : wrap_t i32 = eval_global y_body
 
 (** [constants::unwrap_y] *)
 let unwrap_y_fwd : result i32 = Return y_c.wrap_val
 
 (** [constants::YVAL] *)
-let yval_body : result i32 =
-  begin match unwrap_y_fwd with | Fail e -> Fail e | Return i -> Return i end
+let yval_body : result i32 = unwrap_y_fwd
 let yval_c : i32 = eval_global yval_body
 
 (** [constants::get_z1::Z1] *)
@@ -95,8 +80,7 @@ let get_z1_z1_c : i32 = eval_global get_z1_z1_body
 let get_z1_fwd : result i32 = Return get_z1_z1_c
 
 (** [constants::add] *)
-let add_fwd (a : i32) (b : i32) : result i32 =
-  begin match i32_add a b with | Fail e -> Fail e | Return i -> Return i end
+let add_fwd (a : i32) (b : i32) : result i32 = i32_add a b
 
 (** [constants::Q1] *)
 let q1_body : result i32 = Return 5
@@ -107,8 +91,7 @@ let q2_body : result i32 = Return q1_c
 let q2_c : i32 = eval_global q2_body
 
 (** [constants::Q3] *)
-let q3_body : result i32 =
-  begin match add_fwd q2_c 3 with | Fail e -> Fail e | Return i -> Return i end
+let q3_body : result i32 = add_fwd q2_c 3
 let q3_c : i32 = eval_global q3_body
 
 (** [constants::get_z2] *)
@@ -118,11 +101,7 @@ let get_z2_fwd : result i32 =
   | Return i ->
     begin match add_fwd i q3_c with
     | Fail e -> Fail e
-    | Return i0 ->
-      begin match add_fwd q1_c i0 with
-      | Fail e -> Fail e
-      | Return i1 -> Return i1
-      end
+    | Return i0 -> add_fwd q1_c i0
     end
   end
 
@@ -131,8 +110,7 @@ let s1_body : result u32 = Return 6
 let s1_c : u32 = eval_global s1_body
 
 (** [constants::S2] *)
-let s2_body : result u32 =
-  begin match incr_fwd s1_c with | Fail e -> Fail e | Return i -> Return i end
+let s2_body : result u32 = incr_fwd s1_c
 let s2_c : u32 = eval_global s2_body
 
 (** [constants::S3] *)
@@ -140,10 +118,6 @@ let s3_body : result (pair_t u32 u32) = Return p3_c
 let s3_c : pair_t u32 u32 = eval_global s3_body
 
 (** [constants::S4] *)
-let s4_body : result (pair_t u32 u32) =
-  begin match mk_pair1_fwd 7 8 with
-  | Fail e -> Fail e
-  | Return p -> Return p
-  end
+let s4_body : result (pair_t u32 u32) = mk_pair1_fwd 7 8
 let s4_c : pair_t u32 u32 = eval_global s4_body
 
diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index a57472d4..2529ec33 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -46,12 +46,7 @@ let test_new_non_zero_u32_fwd
   begin match core_num_nonzero_non_zero_u32_new_fwd x st with
   | Fail e -> Fail e
   | Return (st0, opt) ->
-    begin match
-      core_option_option_unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0
-      with
-    | Fail e -> Fail e
-    | Return (st1, nzu) -> Return (st1, nzu)
-    end
+    core_option_option_unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0
   end
 
 (** [external::test_vec] *)
@@ -112,10 +107,7 @@ let test_custom_swap_back
   (x : u32) (y : u32) (st : state) (st0 : state) :
   result (state & (u32 & u32))
   =
-  begin match custom_swap_back u32 x y st 1 st0 with
-  | Fail e -> Fail e
-  | Return (st1, (x0, y0)) -> Return (st1, (x0, y0))
-  end
+  custom_swap_back u32 x y st 1 st0
 
 (** [external::test_swap_non_zero] *)
 let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) =
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index f5339339..870a2159 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -19,21 +19,14 @@ let rec list_nth_mut_loop_loop0_fwd
     else
       begin match u32_sub i 1 with
       | Fail e -> Fail e
-      | Return i0 ->
-        begin match list_nth_mut_loop_loop0_fwd t tl i0 with
-        | Fail e -> Fail e
-        | Return x0 -> Return x0
-        end
+      | Return i0 -> list_nth_mut_loop_loop0_fwd t tl i0
       end
   | ListNil -> Fail Failure
   end
 
 (** [loops::list_nth_mut_loop] *)
 let list_nth_mut_loop_fwd (t : Type0) (ls : list_t t) (i : u32) : result t =
-  begin match list_nth_mut_loop_loop0_fwd t ls i with
-  | Fail e -> Fail e
-  | Return x -> Return x
-  end
+  list_nth_mut_loop_loop0_fwd t ls i
 
 (** [loops::list_nth_mut_loop] *)
 let rec list_nth_mut_loop_loop0_back
@@ -59,8 +52,5 @@ let rec list_nth_mut_loop_loop0_back
 (** [loops::list_nth_mut_loop] *)
 let list_nth_mut_loop_back
   (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) =
-  begin match list_nth_mut_loop_loop0_back t ls i ret with
-  | Fail e -> Fail e
-  | Return l -> Return l
-  end
+  list_nth_mut_loop_loop0_back t ls i ret
 
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index 8424a7cc..f8c63798 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -31,35 +31,25 @@ type sum_t (t1 t2 : Type0) =
 | SumRight : t2 -> sum_t t1 t2
 
 (** [no_nested_borrows::neg_test] *)
-let neg_test_fwd (x : i32) : result i32 =
-  begin match i32_neg x with | Fail e -> Fail e | Return i -> Return i end
+let neg_test_fwd (x : i32) : result i32 = i32_neg x
 
 (** [no_nested_borrows::add_test] *)
-let add_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_add x y with | Fail e -> Fail e | Return i -> Return i end
+let add_test_fwd (x : u32) (y : u32) : result u32 = u32_add x y
 
 (** [no_nested_borrows::subs_test] *)
-let subs_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_sub x y with | Fail e -> Fail e | Return i -> Return i end
+let subs_test_fwd (x : u32) (y : u32) : result u32 = u32_sub x y
 
 (** [no_nested_borrows::div_test] *)
-let div_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_div x y with | Fail e -> Fail e | Return i -> Return i end
+let div_test_fwd (x : u32) (y : u32) : result u32 = u32_div x y
 
 (** [no_nested_borrows::div_test1] *)
-let div_test1_fwd (x : u32) : result u32 =
-  begin match u32_div x 2 with | Fail e -> Fail e | Return i -> Return i end
+let div_test1_fwd (x : u32) : result u32 = u32_div x 2
 
 (** [no_nested_borrows::rem_test] *)
-let rem_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_rem x y with | Fail e -> Fail e | Return i -> Return i end
+let rem_test_fwd (x : u32) (y : u32) : result u32 = u32_rem x y
 
 (** [no_nested_borrows::cast_test] *)
-let cast_test_fwd (x : u32) : result i32 =
-  begin match scalar_cast U32 I32 x with
-  | Fail e -> Fail e
-  | Return i -> Return i
-  end
+let cast_test_fwd (x : u32) : result i32 = scalar_cast U32 I32 x
 
 (** [no_nested_borrows::test2] *)
 let test2_fwd : result unit =
@@ -245,11 +235,7 @@ let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 =
   | ListCons x l1 ->
     begin match list_length_fwd t l1 with
     | Fail e -> Fail e
-    | Return i ->
-      begin match u32_add 1 i with
-      | Fail e -> Fail e
-      | Return i0 -> Return i0
-      end
+    | Return i -> u32_add 1 i
     end
   | ListNil -> Return 0
   end
@@ -263,11 +249,7 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
     else
       begin match u32_sub i 1 with
       | Fail e -> Fail e
-      | Return i0 ->
-        begin match list_nth_shared_fwd t tl i0 with
-        | Fail e -> Fail e
-        | Return x0 -> Return x0
-        end
+      | Return i0 -> list_nth_shared_fwd t tl i0
       end
   | ListNil -> Fail Failure
   end
@@ -281,11 +263,7 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
     else
       begin match u32_sub i 1 with
       | Fail e -> Fail e
-      | Return i0 ->
-        begin match list_nth_mut_fwd t tl i0 with
-        | Fail e -> Fail e
-        | Return x0 -> Return x0
-        end
+      | Return i0 -> list_nth_mut_fwd t tl i0
       end
   | ListNil -> Fail Failure
   end
@@ -313,21 +291,14 @@ let rec list_nth_mut_back
 let rec list_rev_aux_fwd
   (t : Type0) (li : list_t t) (lo : list_t t) : result (list_t t) =
   begin match li with
-  | ListCons hd tl ->
-    begin match list_rev_aux_fwd t tl (ListCons hd lo) with
-    | Fail e -> Fail e
-    | Return l -> Return l
-    end
+  | ListCons hd tl -> list_rev_aux_fwd t tl (ListCons hd lo)
   | ListNil -> Return lo
   end
 
 (** [no_nested_borrows::list_rev] *)
 let list_rev_fwd_back (t : Type0) (l : list_t t) : result (list_t t) =
   let li = mem_replace_fwd (list_t t) l ListNil in
-  begin match list_rev_aux_fwd t li ListNil with
-  | Fail e -> Fail e
-  | Return l0 -> Return l0
-  end
+  list_rev_aux_fwd t li ListNil
 
 (** [no_nested_borrows::test_list_functions] *)
 let test_list_functions_fwd : result unit =
diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index 0f8604d1..199ceb63 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -6,8 +6,7 @@ open Primitives
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [paper::ref_incr] *)
-let ref_incr_fwd_back (x : i32) : result i32 =
-  begin match i32_add x 1 with | Fail e -> Fail e | Return x0 -> Return x0 end
+let ref_incr_fwd_back (x : i32) : result i32 = i32_add x 1
 
 (** [paper::test_incr] *)
 let test_incr_fwd : result unit =
@@ -66,11 +65,7 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
     else
       begin match u32_sub i 1 with
       | Fail e -> Fail e
-      | Return i0 ->
-        begin match list_nth_mut_fwd t tl i0 with
-        | Fail e -> Fail e
-        | Return x0 -> Return x0
-        end
+      | Return i0 -> list_nth_mut_fwd t tl i0
       end
   | ListNil -> Fail Failure
   end
@@ -100,11 +95,7 @@ let rec sum_fwd (l : list_t i32) : result i32 =
   | ListCons x tl ->
     begin match sum_fwd tl with
     | Fail e -> Fail e
-    | Return i ->
-      begin match i32_add x i with
-      | Fail e -> Fail e
-      | Return i0 -> Return i0
-      end
+    | Return i -> i32_add x i
     end
   | ListNil -> Return 0
   end
diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst
index 158a5fc7..12618dbb 100644
--- a/tests/fstar/misc/PoloniusList.fst
+++ b/tests/fstar/misc/PoloniusList.fst
@@ -14,13 +14,7 @@ type list_t (t : Type0) =
 let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) =
   begin match ls with
   | ListCons hd tl ->
-    if hd = x
-    then Return (ListCons hd tl)
-    else
-      begin match get_list_at_x_fwd tl x with
-      | Fail e -> Fail e
-      | Return l -> Return l
-      end
+    if hd = x then Return (ListCons hd tl) else get_list_at_x_fwd tl x
   | ListNil -> Return ListNil
   end