Regenerate the test files and add the fstar-split tests

1 files changed, 245 insertions, 484 deletions

diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 83c249c1..313c2cfd 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -8,90 +8,90 @@ Import ListNotations.
 Local Open Scope Primitives_scope.
 Module Loops.
 
-(** [loops::sum]: loop 0: forward function
+(** [loops::sum]: loop 0:
     Source: 'src/loops.rs', lines 4:0-14:1 *)
 Fixpoint sum_loop (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     if i s< max
-    then (s0 <- u32_add s i; i0 <- u32_add i 1%u32; sum_loop n0 max i0 s0)
+    then (s1 <- u32_add s i; i1 <- u32_add i 1%u32; sum_loop n1 max i1 s1)
     else u32_mul s 2%u32
   end
 .
 
-(** [loops::sum]: forward function
+(** [loops::sum]:
     Source: 'src/loops.rs', lines 4:0-4:27 *)
 Definition sum (n : nat) (max : u32) : result u32 :=
   sum_loop n max 0%u32 0%u32
 .
 
-(** [loops::sum_with_mut_borrows]: loop 0: forward function
+(** [loops::sum_with_mut_borrows]: loop 0:
     Source: 'src/loops.rs', lines 19:0-31:1 *)
 Fixpoint sum_with_mut_borrows_loop
   (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     if mi s< max
     then (
-      ms0 <- u32_add ms mi;
-      mi0 <- u32_add mi 1%u32;
-      sum_with_mut_borrows_loop n0 max mi0 ms0)
+      ms1 <- u32_add ms mi;
+      mi1 <- u32_add mi 1%u32;
+      sum_with_mut_borrows_loop n1 max mi1 ms1)
     else u32_mul ms 2%u32
   end
 .
 
-(** [loops::sum_with_mut_borrows]: forward function
+(** [loops::sum_with_mut_borrows]:
     Source: 'src/loops.rs', lines 19:0-19:44 *)
 Definition sum_with_mut_borrows (n : nat) (max : u32) : result u32 :=
   sum_with_mut_borrows_loop n max 0%u32 0%u32
 .
 
-(** [loops::sum_with_shared_borrows]: loop 0: forward function
+(** [loops::sum_with_shared_borrows]: loop 0:
     Source: 'src/loops.rs', lines 34:0-48:1 *)
 Fixpoint sum_with_shared_borrows_loop
   (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     if i s< max
     then (
-      i0 <- u32_add i 1%u32;
-      s0 <- u32_add s i0;
-      sum_with_shared_borrows_loop n0 max i0 s0)
+      i1 <- u32_add i 1%u32;
+      s1 <- u32_add s i1;
+      sum_with_shared_borrows_loop n1 max i1 s1)
     else u32_mul s 2%u32
   end
 .
 
-(** [loops::sum_with_shared_borrows]: forward function
+(** [loops::sum_with_shared_borrows]:
     Source: 'src/loops.rs', lines 34:0-34:47 *)
 Definition sum_with_shared_borrows (n : nat) (max : u32) : result u32 :=
   sum_with_shared_borrows_loop n max 0%u32 0%u32
 .
 
-(** [loops::clear]: loop 0: merged forward/backward function
-    (there is a single backward function, and the forward function returns ())
+(** [loops::clear]: loop 0:
     Source: 'src/loops.rs', lines 52:0-58:1 *)
 Fixpoint clear_loop
   (n : nat) (v : alloc_vec_Vec u32) (i : usize) : result (alloc_vec_Vec u32) :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
-    let i0 := alloc_vec_Vec_len u32 v in
-    if i s< i0
+  | S n1 =>
+    let i1 := alloc_vec_Vec_len u32 v in
+    if i s< i1
     then (
-      i1 <- usize_add i 1%usize;
-      v0 <-
-        alloc_vec_Vec_index_mut_back u32 usize
-          (core_slice_index_SliceIndexUsizeSliceTInst u32) v i 0%u32;
-      clear_loop n0 v0 i1)
+      p <-
+        alloc_vec_Vec_index_mut u32 usize
+          (core_slice_index_SliceIndexUsizeSliceTInst u32) v i;
+      let (_, index_mut_back) := p in
+      i2 <- usize_add i 1%usize;
+      v1 <- index_mut_back 0%u32;
+      clear_loop n1 v1 i2)
     else Return v
   end
 .
 
-(** [loops::clear]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ())
+(** [loops::clear]:
     Source: 'src/loops.rs', lines 52:0-52:30 *)
 Definition clear
   (n : nat) (v : alloc_vec_Vec u32) : result (alloc_vec_Vec u32) :=
@@ -108,181 +108,146 @@ Inductive List_t (T : Type) :=
 Arguments List_Cons { _ }.
 Arguments List_Nil { _ }.
 
-(** [loops::list_mem]: loop 0: forward function
+(** [loops::list_mem]: loop 0:
     Source: 'src/loops.rs', lines 66:0-75:1 *)
 Fixpoint list_mem_loop (n : nat) (x : u32) (ls : List_t u32) : result bool :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match ls with
-    | List_Cons y tl => if y s= x then Return true else list_mem_loop n0 x tl
+    | List_Cons y tl => if y s= x then Return true else list_mem_loop n1 x tl
     | List_Nil => Return false
     end
   end
 .
 
-(** [loops::list_mem]: forward function
+(** [loops::list_mem]:
     Source: 'src/loops.rs', lines 66:0-66:52 *)
 Definition list_mem (n : nat) (x : u32) (ls : List_t u32) : result bool :=
   list_mem_loop n x ls
 .
 
-(** [loops::list_nth_mut_loop]: loop 0: forward function
+(** [loops::list_nth_mut_loop]: loop 0:
     Source: 'src/loops.rs', lines 78:0-88:1 *)
 Fixpoint list_nth_mut_loop_loop
-  (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | List_Cons x tl =>
-      if i s= 0%u32
-      then Return x
-      else (i0 <- u32_sub i 1%u32; list_nth_mut_loop_loop T n0 tl i0)
-    | List_Nil => Fail_ Failure
-    end
-  end
-.
-
-(** [loops::list_nth_mut_loop]: forward function
-    Source: 'src/loops.rs', lines 78:0-78:71 *)
-Definition list_nth_mut_loop
-  (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
-  list_nth_mut_loop_loop T n ls i
-.
-
-(** [loops::list_nth_mut_loop]: loop 0: backward function 0
-    Source: 'src/loops.rs', lines 78:0-88:1 *)
-Fixpoint list_nth_mut_loop_loop_back
-  (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
-  result (List_t T)
+  (T : Type) (n : nat) (ls : List_t T) (i : u32) :
+  result (T * (T -> result (List_t T)))
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match ls with
     | List_Cons x tl =>
       if i s= 0%u32
-      then Return (List_Cons ret tl)
+      then
+        let back := fun (ret : T) => Return (List_Cons ret tl) in
+        Return (x, back)
       else (
-        i0 <- u32_sub i 1%u32;
-        tl0 <- list_nth_mut_loop_loop_back T n0 tl i0 ret;
-        Return (List_Cons x tl0))
+        i1 <- u32_sub i 1%u32;
+        p <- list_nth_mut_loop_loop T n1 tl i1;
+        let (t, back) := p in
+        let back1 := fun (ret : T) => tl1 <- back ret; Return (List_Cons x tl1)
+          in
+        Return (t, back1))
     | List_Nil => Fail_ Failure
     end
   end
 .
 
-(** [loops::list_nth_mut_loop]: backward function 0
+(** [loops::list_nth_mut_loop]:
     Source: 'src/loops.rs', lines 78:0-78:71 *)
-Definition list_nth_mut_loop_back
-  (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
-  result (List_t T)
+Definition list_nth_mut_loop
+  (T : Type) (n : nat) (ls : List_t T) (i : u32) :
+  result (T * (T -> result (List_t T)))
   :=
-  list_nth_mut_loop_loop_back T n ls i ret
+  p <- list_nth_mut_loop_loop T n ls i;
+  let (t, back) := p in
+  let back1 := fun (ret : T) => back ret in
+  Return (t, back1)
 .
 
-(** [loops::list_nth_shared_loop]: loop 0: forward function
+(** [loops::list_nth_shared_loop]: loop 0:
     Source: 'src/loops.rs', lines 91:0-101:1 *)
 Fixpoint list_nth_shared_loop_loop
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match ls with
     | List_Cons x tl =>
       if i s= 0%u32
       then Return x
-      else (i0 <- u32_sub i 1%u32; list_nth_shared_loop_loop T n0 tl i0)
+      else (i1 <- u32_sub i 1%u32; list_nth_shared_loop_loop T n1 tl i1)
     | List_Nil => Fail_ Failure
     end
   end
 .
 
-(** [loops::list_nth_shared_loop]: forward function
+(** [loops::list_nth_shared_loop]:
     Source: 'src/loops.rs', lines 91:0-91:66 *)
 Definition list_nth_shared_loop
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
   list_nth_shared_loop_loop T n ls i
 .
 
-(** [loops::get_elem_mut]: loop 0: forward function
+(** [loops::get_elem_mut]: loop 0:
     Source: 'src/loops.rs', lines 103:0-117:1 *)
 Fixpoint get_elem_mut_loop
-  (n : nat) (x : usize) (ls : List_t usize) : result usize :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | List_Cons y tl => if y s= x then Return y else get_elem_mut_loop n0 x tl
-    | List_Nil => Fail_ Failure
-    end
-  end
-.
-
-(** [loops::get_elem_mut]: forward function
-    Source: 'src/loops.rs', lines 103:0-103:73 *)
-Definition get_elem_mut
-  (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) :
-  result usize
-  :=
-  l <-
-    alloc_vec_Vec_index_mut (List_t usize) usize
-      (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize;
-  get_elem_mut_loop n x l
-.
-
-(** [loops::get_elem_mut]: loop 0: backward function 0
-    Source: 'src/loops.rs', lines 103:0-117:1 *)
-Fixpoint get_elem_mut_loop_back
-  (n : nat) (x : usize) (ls : List_t usize) (ret : usize) :
-  result (List_t usize)
+  (n : nat) (x : usize) (ls : List_t usize) :
+  result (usize * (usize -> result (List_t usize)))
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match ls with
     | List_Cons y tl =>
       if y s= x
-      then Return (List_Cons ret tl)
+      then
+        let back := fun (ret : usize) => Return (List_Cons ret tl) in
+        Return (y, back)
       else (
-        tl0 <- get_elem_mut_loop_back n0 x tl ret; Return (List_Cons y tl0))
+        p <- get_elem_mut_loop n1 x tl;
+        let (i, back) := p in
+        let back1 :=
+          fun (ret : usize) => tl1 <- back ret; Return (List_Cons y tl1) in
+        Return (i, back1))
     | List_Nil => Fail_ Failure
     end
   end
 .
 
-(** [loops::get_elem_mut]: backward function 0
+(** [loops::get_elem_mut]:
     Source: 'src/loops.rs', lines 103:0-103:73 *)
-Definition get_elem_mut_back
-  (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) (ret : usize) :
-  result (alloc_vec_Vec (List_t usize))
+Definition get_elem_mut
+  (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) :
+  result (usize * (usize -> result (alloc_vec_Vec (List_t usize))))
   :=
-  l <-
+  p <-
     alloc_vec_Vec_index_mut (List_t usize) usize
       (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize;
-  l0 <- get_elem_mut_loop_back n x l ret;
-  alloc_vec_Vec_index_mut_back (List_t usize) usize
-    (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize
-    l0
+  let (l, index_mut_back) := p in
+  p1 <- get_elem_mut_loop n x l;
+  let (i, back) := p1 in
+  let back1 := fun (ret : usize) => l1 <- back ret; index_mut_back l1 in
+  Return (i, back1)
 .
 
-(** [loops::get_elem_shared]: loop 0: forward function
+(** [loops::get_elem_shared]: loop 0:
     Source: 'src/loops.rs', lines 119:0-133:1 *)
 Fixpoint get_elem_shared_loop
   (n : nat) (x : usize) (ls : List_t usize) : result usize :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match ls with
     | List_Cons y tl =>
-      if y s= x then Return y else get_elem_shared_loop n0 x tl
+      if y s= x then Return y else get_elem_shared_loop n1 x tl
     | List_Nil => Fail_ Failure
     end
   end
 .
 
-(** [loops::get_elem_shared]: forward function
+(** [loops::get_elem_shared]:
     Source: 'src/loops.rs', lines 119:0-119:68 *)
 Definition get_elem_shared
   (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) :
@@ -294,123 +259,114 @@ Definition get_elem_shared
   get_elem_shared_loop n x l
 .
 
-(** [loops::id_mut]: forward function
-    Source: 'src/loops.rs', lines 135:0-135:50 *)
-Definition id_mut (T : Type) (ls : List_t T) : result (List_t T) :=
-  Return ls.
-
-(** [loops::id_mut]: backward function 0
+(** [loops::id_mut]:
     Source: 'src/loops.rs', lines 135:0-135:50 *)
-Definition id_mut_back
-  (T : Type) (ls : List_t T) (ret : List_t T) : result (List_t T) :=
-  Return ret
+Definition id_mut
+  (T : Type) (ls : List_t T) :
+  result ((List_t T) * (List_t T -> result (List_t T)))
+  :=
+  let back := fun (ret : List_t T) => Return ret in Return (ls, back)
 .
 
-(** [loops::id_shared]: forward function
+(** [loops::id_shared]:
     Source: 'src/loops.rs', lines 139:0-139:45 *)
 Definition id_shared (T : Type) (ls : List_t T) : result (List_t T) :=
   Return ls
 .
 
-(** [loops::list_nth_mut_loop_with_id]: loop 0: forward function
+(** [loops::list_nth_mut_loop_with_id]: loop 0:
     Source: 'src/loops.rs', lines 144:0-155:1 *)
 Fixpoint list_nth_mut_loop_with_id_loop
-  (T : Type) (n : nat) (i : u32) (ls : List_t T) : result T :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | List_Cons x tl =>
-      if i s= 0%u32
-      then Return x
-      else (i0 <- u32_sub i 1%u32; list_nth_mut_loop_with_id_loop T n0 i0 tl)
-    | List_Nil => Fail_ Failure
-    end
-  end
-.
-
-(** [loops::list_nth_mut_loop_with_id]: forward function
-    Source: 'src/loops.rs', lines 144:0-144:75 *)
-Definition list_nth_mut_loop_with_id
-  (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
-  ls0 <- id_mut T ls; list_nth_mut_loop_with_id_loop T n i ls0
-.
-
-(** [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0
-    Source: 'src/loops.rs', lines 144:0-155:1 *)
-Fixpoint list_nth_mut_loop_with_id_loop_back
-  (T : Type) (n : nat) (i : u32) (ls : List_t T) (ret : T) :
-  result (List_t T)
+  (T : Type) (n : nat) (i : u32) (ls : List_t T) :
+  result (T * (T -> result (List_t T)))
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match ls with
     | List_Cons x tl =>
       if i s= 0%u32
-      then Return (List_Cons ret tl)
+      then
+        let back := fun (ret : T) => Return (List_Cons ret tl) in
+        Return (x, back)
       else (
-        i0 <- u32_sub i 1%u32;
-        tl0 <- list_nth_mut_loop_with_id_loop_back T n0 i0 tl ret;
-        Return (List_Cons x tl0))
+        i1 <- u32_sub i 1%u32;
+        p <- list_nth_mut_loop_with_id_loop T n1 i1 tl;
+        let (t, back) := p in
+        let back1 := fun (ret : T) => tl1 <- back ret; Return (List_Cons x tl1)
+          in
+        Return (t, back1))
     | List_Nil => Fail_ Failure
     end
   end
 .
 
-(** [loops::list_nth_mut_loop_with_id]: backward function 0
+(** [loops::list_nth_mut_loop_with_id]:
     Source: 'src/loops.rs', lines 144:0-144:75 *)
-Definition list_nth_mut_loop_with_id_back
-  (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
-  result (List_t T)
+Definition list_nth_mut_loop_with_id
+  (T : Type) (n : nat) (ls : List_t T) (i : u32) :
+  result (T * (T -> result (List_t T)))
   :=
-  ls0 <- id_mut T ls;
-  l <- list_nth_mut_loop_with_id_loop_back T n i ls0 ret;
-  id_mut_back T ls l
+  p <- id_mut T ls;
+  let (ls1, id_mut_back) := p in
+  p1 <- list_nth_mut_loop_with_id_loop T n i ls1;
+  let (t, back) := p1 in
+  let back1 := fun (ret : T) => l <- back ret; id_mut_back l in
+  Return (t, back1)
 .
 
-(** [loops::list_nth_shared_loop_with_id]: loop 0: forward function
+(** [loops::list_nth_shared_loop_with_id]: loop 0:
     Source: 'src/loops.rs', lines 158:0-169:1 *)
 Fixpoint list_nth_shared_loop_with_id_loop
   (T : Type) (n : nat) (i : u32) (ls : List_t T) : result T :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match ls with
     | List_Cons x tl =>
       if i s= 0%u32
       then Return x
       else (
-        i0 <- u32_sub i 1%u32; list_nth_shared_loop_with_id_loop T n0 i0 tl)
+        i1 <- u32_sub i 1%u32; list_nth_shared_loop_with_id_loop T n1 i1 tl)
     | List_Nil => Fail_ Failure
     end
   end
 .
 
-(** [loops::list_nth_shared_loop_with_id]: forward function
+(** [loops::list_nth_shared_loop_with_id]:
     Source: 'src/loops.rs', lines 158:0-158:70 *)
 Definition list_nth_shared_loop_with_id
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
-  ls0 <- id_shared T ls; list_nth_shared_loop_with_id_loop T n i ls0
+  ls1 <- id_shared T ls; list_nth_shared_loop_with_id_loop T n i ls1
 .
 
-(** [loops::list_nth_mut_loop_pair]: loop 0: forward function
+(** [loops::list_nth_mut_loop_pair]: loop 0:
     Source: 'src/loops.rs', lines 174:0-195:1 *)
 Fixpoint list_nth_mut_loop_pair_loop
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
-  result (T * T)
+  result ((T * T) * (T -> result (List_t T)) * (T -> result (List_t T)))
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match ls0 with
     | List_Cons x0 tl0 =>
       match ls1 with
       | List_Cons x1 tl1 =>
         if i s= 0%u32
-        then Return (x0, x1)
+        then
+          let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in
+          let back_'b := fun (ret : T) => Return (List_Cons ret tl1) in
+          Return ((x0, x1), back_'a, back_'b)
         else (
-          i0 <- u32_sub i 1%u32; list_nth_mut_loop_pair_loop T n0 tl0 tl1 i0)
+          i1 <- u32_sub i 1%u32;
+          t <- list_nth_mut_loop_pair_loop T n1 tl0 tl1 i1;
+          let (p, back_'a, back_'b) := t in
+          let back_'a1 :=
+            fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in
+          let back_'b1 :=
+            fun (ret : T) => tl11 <- back_'b ret; Return (List_Cons x1 tl11) in
+          Return (p, back_'a1, back_'b1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -418,86 +374,20 @@ Fixpoint list_nth_mut_loop_pair_loop
   end
 .
 
-(** [loops::list_nth_mut_loop_pair]: forward function
+(** [loops::list_nth_mut_loop_pair]:
     Source: 'src/loops.rs', lines 174:0-178:27 *)
 Definition list_nth_mut_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
-  result (T * T)
+  result ((T * T) * (T -> result (List_t T)) * (T -> result (List_t T)))
   :=
-  list_nth_mut_loop_pair_loop T n ls0 ls1 i
+  t <- list_nth_mut_loop_pair_loop T n ls0 ls1 i;
+  let (p, back_'a, back_'b) := t in
+  let back_'a1 := fun (ret : T) => back_'a ret in
+  let back_'b1 := fun (ret : T) => back_'b ret in
+  Return (p, back_'a1, back_'b1)
 .
 
-(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 0
-    Source: 'src/loops.rs', lines 174:0-195:1 *)
-Fixpoint list_nth_mut_loop_pair_loop_back'a
-  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
-  result (List_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls0 with
-    | List_Cons x0 tl0 =>
-      match ls1 with
-      | List_Cons x1 tl1 =>
-        if i s= 0%u32
-        then Return (List_Cons ret tl0)
-        else (
-          i0 <- u32_sub i 1%u32;
-          tl00 <- list_nth_mut_loop_pair_loop_back'a T n0 tl0 tl1 i0 ret;
-          Return (List_Cons x0 tl00))
-      | List_Nil => Fail_ Failure
-      end
-    | List_Nil => Fail_ Failure
-    end
-  end
-.
-
-(** [loops::list_nth_mut_loop_pair]: backward function 0
-    Source: 'src/loops.rs', lines 174:0-178:27 *)
-Definition list_nth_mut_loop_pair_back'a
-  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
-  result (List_t T)
-  :=
-  list_nth_mut_loop_pair_loop_back'a T n ls0 ls1 i ret
-.
-
-(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 1
-    Source: 'src/loops.rs', lines 174:0-195:1 *)
-Fixpoint list_nth_mut_loop_pair_loop_back'b
-  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
-  result (List_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls0 with
-    | List_Cons x0 tl0 =>
-      match ls1 with
-      | List_Cons x1 tl1 =>
-        if i s= 0%u32
-        then Return (List_Cons ret tl1)
-        else (
-          i0 <- u32_sub i 1%u32;
-          tl10 <- list_nth_mut_loop_pair_loop_back'b T n0 tl0 tl1 i0 ret;
-          Return (List_Cons x1 tl10))
-      | List_Nil => Fail_ Failure
-      end
-    | List_Nil => Fail_ Failure
-    end
-  end
-.
-
-(** [loops::list_nth_mut_loop_pair]: backward function 1
-    Source: 'src/loops.rs', lines 174:0-178:27 *)
-Definition list_nth_mut_loop_pair_back'b
-  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
-  result (List_t T)
-  :=
-  list_nth_mut_loop_pair_loop_back'b T n ls0 ls1 i ret
-.
-
-(** [loops::list_nth_shared_loop_pair]: loop 0: forward function
+(** [loops::list_nth_shared_loop_pair]: loop 0:
     Source: 'src/loops.rs', lines 198:0-219:1 *)
 Fixpoint list_nth_shared_loop_pair_loop
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
@@ -505,7 +395,7 @@ Fixpoint list_nth_shared_loop_pair_loop
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match ls0 with
     | List_Cons x0 tl0 =>
       match ls1 with
@@ -513,7 +403,7 @@ Fixpoint list_nth_shared_loop_pair_loop
         if i s= 0%u32
         then Return (x0, x1)
         else (
-          i0 <- u32_sub i 1%u32; list_nth_shared_loop_pair_loop T n0 tl0 tl1 i0)
+          i1 <- u32_sub i 1%u32; list_nth_shared_loop_pair_loop T n1 tl0 tl1 i1)
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -521,7 +411,7 @@ Fixpoint list_nth_shared_loop_pair_loop
   end
 .
 
-(** [loops::list_nth_shared_loop_pair]: forward function
+(** [loops::list_nth_shared_loop_pair]:
     Source: 'src/loops.rs', lines 198:0-202:19 *)
 Definition list_nth_shared_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
@@ -530,24 +420,36 @@ Definition list_nth_shared_loop_pair
   list_nth_shared_loop_pair_loop T n ls0 ls1 i
 .
 
-(** [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function
+(** [loops::list_nth_mut_loop_pair_merge]: loop 0:
     Source: 'src/loops.rs', lines 223:0-238:1 *)
 Fixpoint list_nth_mut_loop_pair_merge_loop
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
-  result (T * T)
+  result ((T * T) * ((T * T) -> result ((List_t T) * (List_t T))))
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match ls0 with
     | List_Cons x0 tl0 =>
       match ls1 with
       | List_Cons x1 tl1 =>
         if i s= 0%u32
-        then Return (x0, x1)
+        then
+          let back_'a :=
+            fun (ret : (T * T)) =>
+              let (t, t1) := ret in Return (List_Cons t tl0, List_Cons t1 tl1)
+            in
+          Return ((x0, x1), back_'a)
         else (
-          i0 <- u32_sub i 1%u32;
-          list_nth_mut_loop_pair_merge_loop T n0 tl0 tl1 i0)
+          i1 <- u32_sub i 1%u32;
+          p <- list_nth_mut_loop_pair_merge_loop T n1 tl0 tl1 i1;
+          let (p1, back_'a) := p in
+          let back_'a1 :=
+            fun (ret : (T * T)) =>
+              p2 <- back_'a ret;
+              let (tl01, tl11) := p2 in
+              Return (List_Cons x0 tl01, List_Cons x1 tl11) in
+          Return (p1, back_'a1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -555,54 +457,19 @@ Fixpoint list_nth_mut_loop_pair_merge_loop
   end
 .
 
-(** [loops::list_nth_mut_loop_pair_merge]: forward function
+(** [loops::list_nth_mut_loop_pair_merge]:
     Source: 'src/loops.rs', lines 223:0-227:27 *)
 Definition list_nth_mut_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
-  result (T * T)
+  result ((T * T) * ((T * T) -> result ((List_t T) * (List_t T))))
   :=
-  list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i
+  p <- list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i;
+  let (p1, back_'a) := p in
+  let back_'a1 := fun (ret : (T * T)) => back_'a ret in
+  Return (p1, back_'a1)
 .
 
-(** [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0
-    Source: 'src/loops.rs', lines 223:0-238:1 *)
-Fixpoint list_nth_mut_loop_pair_merge_loop_back
-  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32)
-  (ret : (T * T)) :
-  result ((List_t T) * (List_t T))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls0 with
-    | List_Cons x0 tl0 =>
-      match ls1 with
-      | List_Cons x1 tl1 =>
-        if i s= 0%u32
-        then let (t, t0) := ret in Return (List_Cons t tl0, List_Cons t0 tl1)
-        else (
-          i0 <- u32_sub i 1%u32;
-          p <- list_nth_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
-          let (tl00, tl10) := p in
-          Return (List_Cons x0 tl00, List_Cons x1 tl10))
-      | List_Nil => Fail_ Failure
-      end
-    | List_Nil => Fail_ Failure
-    end
-  end
-.
-
-(** [loops::list_nth_mut_loop_pair_merge]: backward function 0
-    Source: 'src/loops.rs', lines 223:0-227:27 *)
-Definition list_nth_mut_loop_pair_merge_back
-  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32)
-  (ret : (T * T)) :
-  result ((List_t T) * (List_t T))
-  :=
-  list_nth_mut_loop_pair_merge_loop_back T n ls0 ls1 i ret
-.
-
-(** [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function
+(** [loops::list_nth_shared_loop_pair_merge]: loop 0:
     Source: 'src/loops.rs', lines 241:0-256:1 *)
 Fixpoint list_nth_shared_loop_pair_merge_loop
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
@@ -610,7 +477,7 @@ Fixpoint list_nth_shared_loop_pair_merge_loop
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match ls0 with
     | List_Cons x0 tl0 =>
       match ls1 with
@@ -618,8 +485,8 @@ Fixpoint list_nth_shared_loop_pair_merge_loop
         if i s= 0%u32
         then Return (x0, x1)
         else (
-          i0 <- u32_sub i 1%u32;
-          list_nth_shared_loop_pair_merge_loop T n0 tl0 tl1 i0)
+          i1 <- u32_sub i 1%u32;
+          list_nth_shared_loop_pair_merge_loop T n1 tl0 tl1 i1)
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -627,7 +494,7 @@ Fixpoint list_nth_shared_loop_pair_merge_loop
   end
 .
 
-(** [loops::list_nth_shared_loop_pair_merge]: forward function
+(** [loops::list_nth_shared_loop_pair_merge]:
     Source: 'src/loops.rs', lines 241:0-245:19 *)
 Definition list_nth_shared_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
@@ -636,24 +503,30 @@ Definition list_nth_shared_loop_pair_merge
   list_nth_shared_loop_pair_merge_loop T n ls0 ls1 i
 .
 
-(** [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function
+(** [loops::list_nth_mut_shared_loop_pair]: loop 0:
     Source: 'src/loops.rs', lines 259:0-274:1 *)
 Fixpoint list_nth_mut_shared_loop_pair_loop
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
-  result (T * T)
+  result ((T * T) * (T -> result (List_t T)))
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match ls0 with
     | List_Cons x0 tl0 =>
       match ls1 with
       | List_Cons x1 tl1 =>
         if i s= 0%u32
-        then Return (x0, x1)
+        then
+          let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in
+          Return ((x0, x1), back_'a)
         else (
-          i0 <- u32_sub i 1%u32;
-          list_nth_mut_shared_loop_pair_loop T n0 tl0 tl1 i0)
+          i1 <- u32_sub i 1%u32;
+          p <- list_nth_mut_shared_loop_pair_loop T n1 tl0 tl1 i1;
+          let (p1, back_'a) := p in
+          let back_'a1 :=
+            fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in
+          Return (p1, back_'a1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -661,68 +534,42 @@ Fixpoint list_nth_mut_shared_loop_pair_loop
   end
 .
 
-(** [loops::list_nth_mut_shared_loop_pair]: forward function
+(** [loops::list_nth_mut_shared_loop_pair]:
     Source: 'src/loops.rs', lines 259:0-263:23 *)
 Definition list_nth_mut_shared_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
-  result (T * T)
+  result ((T * T) * (T -> result (List_t T)))
   :=
-  list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i
+  p <- list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i;
+  let (p1, back_'a) := p in
+  let back_'a1 := fun (ret : T) => back_'a ret in
+  Return (p1, back_'a1)
 .
 
-(** [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0
-    Source: 'src/loops.rs', lines 259:0-274:1 *)
-Fixpoint list_nth_mut_shared_loop_pair_loop_back
-  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
-  result (List_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls0 with
-    | List_Cons x0 tl0 =>
-      match ls1 with
-      | List_Cons x1 tl1 =>
-        if i s= 0%u32
-        then Return (List_Cons ret tl0)
-        else (
-          i0 <- u32_sub i 1%u32;
-          tl00 <- list_nth_mut_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
-          Return (List_Cons x0 tl00))
-      | List_Nil => Fail_ Failure
-      end
-    | List_Nil => Fail_ Failure
-    end
-  end
-.
-
-(** [loops::list_nth_mut_shared_loop_pair]: backward function 0
-    Source: 'src/loops.rs', lines 259:0-263:23 *)
-Definition list_nth_mut_shared_loop_pair_back
-  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
-  result (List_t T)
-  :=
-  list_nth_mut_shared_loop_pair_loop_back T n ls0 ls1 i ret
-.
-
-(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function
+(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
     Source: 'src/loops.rs', lines 278:0-293:1 *)
 Fixpoint list_nth_mut_shared_loop_pair_merge_loop
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
-  result (T * T)
+  result ((T * T) * (T -> result (List_t T)))
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match ls0 with
     | List_Cons x0 tl0 =>
       match ls1 with
       | List_Cons x1 tl1 =>
         if i s= 0%u32
-        then Return (x0, x1)
+        then
+          let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in
+          Return ((x0, x1), back_'a)
         else (
-          i0 <- u32_sub i 1%u32;
-          list_nth_mut_shared_loop_pair_merge_loop T n0 tl0 tl1 i0)
+          i1 <- u32_sub i 1%u32;
+          p <- list_nth_mut_shared_loop_pair_merge_loop T n1 tl0 tl1 i1;
+          let (p1, back_'a) := p in
+          let back_'a1 :=
+            fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in
+          Return (p1, back_'a1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -730,69 +577,42 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop
   end
 .
 
-(** [loops::list_nth_mut_shared_loop_pair_merge]: forward function
+(** [loops::list_nth_mut_shared_loop_pair_merge]:
     Source: 'src/loops.rs', lines 278:0-282:23 *)
 Definition list_nth_mut_shared_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
-  result (T * T)
-  :=
-  list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i
-.
-
-(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0
-    Source: 'src/loops.rs', lines 278:0-293:1 *)
-Fixpoint list_nth_mut_shared_loop_pair_merge_loop_back
-  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
-  result (List_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls0 with
-    | List_Cons x0 tl0 =>
-      match ls1 with
-      | List_Cons x1 tl1 =>
-        if i s= 0%u32
-        then Return (List_Cons ret tl0)
-        else (
-          i0 <- u32_sub i 1%u32;
-          tl00 <-
-            list_nth_mut_shared_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
-          Return (List_Cons x0 tl00))
-      | List_Nil => Fail_ Failure
-      end
-    | List_Nil => Fail_ Failure
-    end
-  end
-.
-
-(** [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0
-    Source: 'src/loops.rs', lines 278:0-282:23 *)
-Definition list_nth_mut_shared_loop_pair_merge_back
-  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
-  result (List_t T)
+  result ((T * T) * (T -> result (List_t T)))
   :=
-  list_nth_mut_shared_loop_pair_merge_loop_back T n ls0 ls1 i ret
+  p <- list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i;
+  let (p1, back_'a) := p in
+  let back_'a1 := fun (ret : T) => back_'a ret in
+  Return (p1, back_'a1)
 .
 
-(** [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function
+(** [loops::list_nth_shared_mut_loop_pair]: loop 0:
     Source: 'src/loops.rs', lines 297:0-312:1 *)
 Fixpoint list_nth_shared_mut_loop_pair_loop
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
-  result (T * T)
+  result ((T * T) * (T -> result (List_t T)))
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match ls0 with
     | List_Cons x0 tl0 =>
       match ls1 with
       | List_Cons x1 tl1 =>
         if i s= 0%u32
-        then Return (x0, x1)
+        then
+          let back_'b := fun (ret : T) => Return (List_Cons ret tl1) in
+          Return ((x0, x1), back_'b)
         else (
-          i0 <- u32_sub i 1%u32;
-          list_nth_shared_mut_loop_pair_loop T n0 tl0 tl1 i0)
+          i1 <- u32_sub i 1%u32;
+          p <- list_nth_shared_mut_loop_pair_loop T n1 tl0 tl1 i1;
+          let (p1, back_'b) := p in
+          let back_'b1 :=
+            fun (ret : T) => tl11 <- back_'b ret; Return (List_Cons x1 tl11) in
+          Return (p1, back_'b1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -800,68 +620,42 @@ Fixpoint list_nth_shared_mut_loop_pair_loop
   end
 .
 
-(** [loops::list_nth_shared_mut_loop_pair]: forward function
+(** [loops::list_nth_shared_mut_loop_pair]:
     Source: 'src/loops.rs', lines 297:0-301:23 *)
 Definition list_nth_shared_mut_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
-  result (T * T)
+  result ((T * T) * (T -> result (List_t T)))
   :=
-  list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i
-.
-
-(** [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1
-    Source: 'src/loops.rs', lines 297:0-312:1 *)
-Fixpoint list_nth_shared_mut_loop_pair_loop_back
-  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
-  result (List_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls0 with
-    | List_Cons x0 tl0 =>
-      match ls1 with
-      | List_Cons x1 tl1 =>
-        if i s= 0%u32
-        then Return (List_Cons ret tl1)
-        else (
-          i0 <- u32_sub i 1%u32;
-          tl10 <- list_nth_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
-          Return (List_Cons x1 tl10))
-      | List_Nil => Fail_ Failure
-      end
-    | List_Nil => Fail_ Failure
-    end
-  end
+  p <- list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i;
+  let (p1, back_'b) := p in
+  let back_'b1 := fun (ret : T) => back_'b ret in
+  Return (p1, back_'b1)
 .
 
-(** [loops::list_nth_shared_mut_loop_pair]: backward function 1
-    Source: 'src/loops.rs', lines 297:0-301:23 *)
-Definition list_nth_shared_mut_loop_pair_back
-  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
-  result (List_t T)
-  :=
-  list_nth_shared_mut_loop_pair_loop_back T n ls0 ls1 i ret
-.
-
-(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function
+(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
     Source: 'src/loops.rs', lines 316:0-331:1 *)
 Fixpoint list_nth_shared_mut_loop_pair_merge_loop
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
-  result (T * T)
+  result ((T * T) * (T -> result (List_t T)))
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match ls0 with
     | List_Cons x0 tl0 =>
       match ls1 with
       | List_Cons x1 tl1 =>
         if i s= 0%u32
-        then Return (x0, x1)
+        then
+          let back_'a := fun (ret : T) => Return (List_Cons ret tl1) in
+          Return ((x0, x1), back_'a)
         else (
-          i0 <- u32_sub i 1%u32;
-          list_nth_shared_mut_loop_pair_merge_loop T n0 tl0 tl1 i0)
+          i1 <- u32_sub i 1%u32;
+          p <- list_nth_shared_mut_loop_pair_merge_loop T n1 tl0 tl1 i1;
+          let (p1, back_'a) := p in
+          let back_'a1 :=
+            fun (ret : T) => tl11 <- back_'a ret; Return (List_Cons x1 tl11) in
+          Return (p1, back_'a1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -869,49 +663,16 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop
   end
 .
 
-(** [loops::list_nth_shared_mut_loop_pair_merge]: forward function
+(** [loops::list_nth_shared_mut_loop_pair_merge]:
     Source: 'src/loops.rs', lines 316:0-320:23 *)
 Definition list_nth_shared_mut_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
-  result (T * T)
-  :=
-  list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i
-.
-
-(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0
-    Source: 'src/loops.rs', lines 316:0-331:1 *)
-Fixpoint list_nth_shared_mut_loop_pair_merge_loop_back
-  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
-  result (List_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls0 with
-    | List_Cons x0 tl0 =>
-      match ls1 with
-      | List_Cons x1 tl1 =>
-        if i s= 0%u32
-        then Return (List_Cons ret tl1)
-        else (
-          i0 <- u32_sub i 1%u32;
-          tl10 <-
-            list_nth_shared_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
-          Return (List_Cons x1 tl10))
-      | List_Nil => Fail_ Failure
-      end
-    | List_Nil => Fail_ Failure
-    end
-  end
-.
-
-(** [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0
-    Source: 'src/loops.rs', lines 316:0-320:23 *)
-Definition list_nth_shared_mut_loop_pair_merge_back
-  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
-  result (List_t T)
+  result ((T * T) * (T -> result (List_t T)))
   :=
-  list_nth_shared_mut_loop_pair_merge_loop_back T n ls0 ls1 i ret
+  p <- list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i;
+  let (p1, back_'a) := p in
+  let back_'a1 := fun (ret : T) => back_'a ret in
+  Return (p1, back_'a1)
 .
 
 End Loops.