Improve formatting of the termination_by clauses

3 files changed, 52 insertions, 84 deletions

diff --git a/tests/lean/hashmap/Hashmap/Funs.lean b/tests/lean/hashmap/Hashmap/Funs.lean
index 030b335a..1b03b7a2 100644
--- a/tests/lean/hashmap/Hashmap/Funs.lean
+++ b/tests/lean/hashmap/Hashmap/Funs.lean
@@ -20,8 +20,7 @@ def hash_map_allocate_slots_loop_fwd
       hash_map_allocate_slots_loop_fwd T slots0 n0
   else result.ret slots
 termination_by hash_map_allocate_slots_loop_fwd slots n =>
-                                                          hash_map_allocate_slots_loop_terminates
-                                                          T slots n
+  hash_map_allocate_slots_loop_terminates T slots n
 decreasing_by hash_map_allocate_slots_loop_decreases slots n
 
 /- [hashmap::HashMap::{0}::allocate_slots] -/
@@ -67,8 +66,7 @@ def hash_map_clear_loop_fwd_back
       hash_map_clear_loop_fwd_back T slots0 i1
   else result.ret slots
 termination_by hash_map_clear_loop_fwd_back slots i =>
-                                                      hash_map_clear_loop_terminates
-                                                      T slots i
+  hash_map_clear_loop_terminates T slots i
 decreasing_by hash_map_clear_loop_decreases slots i
 
 /- [hashmap::HashMap::{0}::clear] -/
@@ -101,8 +99,7 @@ def hash_map_insert_in_list_loop_fwd
   | list_t.ListNil => result.ret true
   
 termination_by hash_map_insert_in_list_loop_fwd key value ls =>
-                                                               hash_map_insert_in_list_loop_terminates
-                                                               T key value ls
+  hash_map_insert_in_list_loop_terminates T key value ls
 decreasing_by hash_map_insert_in_list_loop_decreases key value ls
 
 /- [hashmap::HashMap::{0}::insert_in_list] -/
@@ -125,8 +122,7 @@ def hash_map_insert_in_list_loop_back
     let l := list_t.ListNil result.ret (list_t.ListCons key value l)
   
 termination_by hash_map_insert_in_list_loop_back key value ls =>
-                                                                hash_map_insert_in_list_loop_terminates
-                                                                T key value ls
+  hash_map_insert_in_list_loop_terminates T key value ls
 decreasing_by hash_map_insert_in_list_loop_decreases key value ls
 
 /- [hashmap::HashMap::{0}::insert_in_list] -/
@@ -189,7 +185,7 @@ def hash_map_move_elements_from_list_loop_fwd_back
   | list_t.ListNil => result.ret ntable
   
 termination_by hash_map_move_elements_from_list_loop_fwd_back ntable ls =>
-   hash_map_move_elements_from_list_loop_terminates T ntable ls
+  hash_map_move_elements_from_list_loop_terminates T ntable ls
 decreasing_by hash_map_move_elements_from_list_loop_decreases ntable ls
 
 /- [hashmap::HashMap::{0}::move_elements_from_list] -/
@@ -215,7 +211,7 @@ def hash_map_move_elements_loop_fwd_back
       hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1
   else result.ret (ntable, slots)
 termination_by hash_map_move_elements_loop_fwd_back ntable slots i =>
-   hash_map_move_elements_loop_terminates T ntable slots i
+  hash_map_move_elements_loop_terminates T ntable slots i
 decreasing_by hash_map_move_elements_loop_decreases ntable slots i
 
 /- [hashmap::HashMap::{0}::move_elements] -/
@@ -281,8 +277,7 @@ def hash_map_contains_key_in_list_loop_fwd
   | list_t.ListNil => result.ret false
   
 termination_by hash_map_contains_key_in_list_loop_fwd key ls =>
-                                                               hash_map_contains_key_in_list_loop_terminates
-                                                               T key ls
+  hash_map_contains_key_in_list_loop_terminates T key ls
 decreasing_by hash_map_contains_key_in_list_loop_decreases key ls
 
 /- [hashmap::HashMap::{0}::contains_key_in_list] -/
@@ -311,8 +306,7 @@ def hash_map_get_in_list_loop_fwd
   | list_t.ListNil => result.fail error.panic
   
 termination_by hash_map_get_in_list_loop_fwd key ls =>
-                                                      hash_map_get_in_list_loop_terminates
-                                                      T key ls
+  hash_map_get_in_list_loop_terminates T key ls
 decreasing_by hash_map_get_in_list_loop_decreases key ls
 
 /- [hashmap::HashMap::{0}::get_in_list] -/
@@ -341,8 +335,7 @@ def hash_map_get_mut_in_list_loop_fwd
   | list_t.ListNil => result.fail error.panic
   
 termination_by hash_map_get_mut_in_list_loop_fwd ls key =>
-                                                          hash_map_get_mut_in_list_loop_terminates
-                                                          T ls key
+  hash_map_get_mut_in_list_loop_terminates T ls key
 decreasing_by hash_map_get_mut_in_list_loop_decreases ls key
 
 /- [hashmap::HashMap::{0}::get_mut_in_list] -/
@@ -364,8 +357,7 @@ def hash_map_get_mut_in_list_loop_back
   | list_t.ListNil => result.fail error.panic
   
 termination_by hash_map_get_mut_in_list_loop_back ls key ret0 =>
-                                                                hash_map_get_mut_in_list_loop_terminates
-                                                                T ls key
+  hash_map_get_mut_in_list_loop_terminates T ls key
 decreasing_by hash_map_get_mut_in_list_loop_decreases ls key
 
 /- [hashmap::HashMap::{0}::get_mut_in_list] -/
@@ -420,8 +412,7 @@ def hash_map_remove_from_list_loop_fwd
   | list_t.ListNil => result.ret Option.none
   
 termination_by hash_map_remove_from_list_loop_fwd key ls =>
-                                                           hash_map_remove_from_list_loop_terminates
-                                                           T key ls
+  hash_map_remove_from_list_loop_terminates T key ls
 decreasing_by hash_map_remove_from_list_loop_decreases key ls
 
 /- [hashmap::HashMap::{0}::remove_from_list] -/
@@ -449,8 +440,7 @@ def hash_map_remove_from_list_loop_back
   | list_t.ListNil => result.ret list_t.ListNil
   
 termination_by hash_map_remove_from_list_loop_back key ls =>
-                                                            hash_map_remove_from_list_loop_terminates
-                                                            T key ls
+  hash_map_remove_from_list_loop_terminates T key ls
 decreasing_by hash_map_remove_from_list_loop_decreases key ls
 
 /- [hashmap::HashMap::{0}::remove_from_list] -/
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
index 5134f483..2795ecfa 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
@@ -24,8 +24,7 @@ def hashmap_hash_map_allocate_slots_loop_fwd
       hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0
   else result.ret slots
 termination_by hashmap_hash_map_allocate_slots_loop_fwd slots n =>
-                                                                  hashmap_hash_map_allocate_slots_loop_terminates
-                                                                  T slots n
+  hashmap_hash_map_allocate_slots_loop_terminates T slots n
 decreasing_by hashmap_hash_map_allocate_slots_loop_decreases slots n
 
 /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/
@@ -76,8 +75,7 @@ def hashmap_hash_map_clear_loop_fwd_back
       hashmap_hash_map_clear_loop_fwd_back T slots0 i1
   else result.ret slots
 termination_by hashmap_hash_map_clear_loop_fwd_back slots i =>
-                                                              hashmap_hash_map_clear_loop_terminates
-                                                              T slots i
+  hashmap_hash_map_clear_loop_terminates T slots i
 decreasing_by hashmap_hash_map_clear_loop_decreases slots i
 
 /- [hashmap_main::hashmap::HashMap::{0}::clear] -/
@@ -113,7 +111,7 @@ def hashmap_hash_map_insert_in_list_loop_fwd
   | hashmap_list_t.HashmapListNil => result.ret true
   
 termination_by hashmap_hash_map_insert_in_list_loop_fwd key value ls =>
-   hashmap_hash_map_insert_in_list_loop_terminates T key value ls
+  hashmap_hash_map_insert_in_list_loop_terminates T key value ls
 decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls
 
 /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/
@@ -139,7 +137,7 @@ def hashmap_hash_map_insert_in_list_loop_back
     result.ret (hashmap_list_t.HashmapListCons key value l)
   
 termination_by hashmap_hash_map_insert_in_list_loop_back key value ls =>
-   hashmap_hash_map_insert_in_list_loop_terminates T key value ls
+  hashmap_hash_map_insert_in_list_loop_terminates T key value ls
 decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls
 
 /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/
@@ -209,8 +207,8 @@ def hashmap_hash_map_move_elements_from_list_loop_fwd_back
   | hashmap_list_t.HashmapListNil => result.ret ntable
   
 termination_by hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable ls
-              => hashmap_hash_map_move_elements_from_list_loop_terminates T
-                ntable ls
+  =>
+  hashmap_hash_map_move_elements_from_list_loop_terminates T ntable ls
 decreasing_by hashmap_hash_map_move_elements_from_list_loop_decreases ntable ls
 
 /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/
@@ -242,7 +240,7 @@ def hashmap_hash_map_move_elements_loop_fwd_back
       hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1
   else result.ret (ntable, slots)
 termination_by hashmap_hash_map_move_elements_loop_fwd_back ntable slots i =>
-   hashmap_hash_map_move_elements_loop_terminates T ntable slots i
+  hashmap_hash_map_move_elements_loop_terminates T ntable slots i
 decreasing_by hashmap_hash_map_move_elements_loop_decreases ntable slots i
 
 /- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/
@@ -309,7 +307,7 @@ def hashmap_hash_map_contains_key_in_list_loop_fwd
   | hashmap_list_t.HashmapListNil => result.ret false
   
 termination_by hashmap_hash_map_contains_key_in_list_loop_fwd key ls =>
-   hashmap_hash_map_contains_key_in_list_loop_terminates T key ls
+  hashmap_hash_map_contains_key_in_list_loop_terminates T key ls
 decreasing_by hashmap_hash_map_contains_key_in_list_loop_decreases key ls
 
 /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/
@@ -339,8 +337,7 @@ def hashmap_hash_map_get_in_list_loop_fwd
   | hashmap_list_t.HashmapListNil => result.fail error.panic
   
 termination_by hashmap_hash_map_get_in_list_loop_fwd key ls =>
-                                                              hashmap_hash_map_get_in_list_loop_terminates
-                                                              T key ls
+  hashmap_hash_map_get_in_list_loop_terminates T key ls
 decreasing_by hashmap_hash_map_get_in_list_loop_decreases key ls
 
 /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/
@@ -370,8 +367,7 @@ def hashmap_hash_map_get_mut_in_list_loop_fwd
   | hashmap_list_t.HashmapListNil => result.fail error.panic
   
 termination_by hashmap_hash_map_get_mut_in_list_loop_fwd ls key =>
-                                                                  hashmap_hash_map_get_mut_in_list_loop_terminates
-                                                                  T ls key
+  hashmap_hash_map_get_mut_in_list_loop_terminates T ls key
 decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key
 
 /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/
@@ -395,7 +391,7 @@ def hashmap_hash_map_get_mut_in_list_loop_back
   | hashmap_list_t.HashmapListNil => result.fail error.panic
   
 termination_by hashmap_hash_map_get_mut_in_list_loop_back ls key ret0 =>
-   hashmap_hash_map_get_mut_in_list_loop_terminates T ls key
+  hashmap_hash_map_get_mut_in_list_loop_terminates T ls key
 decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key
 
 /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/
@@ -458,8 +454,7 @@ def hashmap_hash_map_remove_from_list_loop_fwd
   | hashmap_list_t.HashmapListNil => result.ret Option.none
   
 termination_by hashmap_hash_map_remove_from_list_loop_fwd key ls =>
-                                                                   hashmap_hash_map_remove_from_list_loop_terminates
-                                                                   T key ls
+  hashmap_hash_map_remove_from_list_loop_terminates T key ls
 decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls
 
 /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/
@@ -490,8 +485,7 @@ def hashmap_hash_map_remove_from_list_loop_back
   | hashmap_list_t.HashmapListNil => result.ret hashmap_list_t.HashmapListNil
   
 termination_by hashmap_hash_map_remove_from_list_loop_back key ls =>
-                                                                    hashmap_hash_map_remove_from_list_loop_terminates
-                                                                    T key ls
+  hashmap_hash_map_remove_from_list_loop_terminates T key ls
 decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls
 
 /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/
diff --git a/tests/lean/misc/loops/Loops/Funs.lean b/tests/lean/misc/loops/Loops/Funs.lean
index 5fe5b4ff..33a3a881 100644
--- a/tests/lean/misc/loops/Loops/Funs.lean
+++ b/tests/lean/misc/loops/Loops/Funs.lean
@@ -32,8 +32,7 @@ def sum_with_mut_borrows_loop_fwd
       sum_with_mut_borrows_loop_fwd max mi0 ms0
   else UInt32.checked_mul ms (UInt32.ofNatCore 2 (by intlit))
 termination_by sum_with_mut_borrows_loop_fwd max mi ms =>
-                                                         sum_with_mut_borrows_loop_terminates
-                                                         max mi ms
+  sum_with_mut_borrows_loop_terminates max mi ms
 decreasing_by sum_with_mut_borrows_loop_decreases max mi ms
 
 /- [loops::sum_with_mut_borrows] -/
@@ -52,8 +51,7 @@ def sum_with_shared_borrows_loop_fwd
       sum_with_shared_borrows_loop_fwd max i0 s0
   else UInt32.checked_mul s (UInt32.ofNatCore 2 (by intlit))
 termination_by sum_with_shared_borrows_loop_fwd max i s =>
-                                                          sum_with_shared_borrows_loop_terminates
-                                                          max i s
+  sum_with_shared_borrows_loop_terminates max i s
 decreasing_by sum_with_shared_borrows_loop_decreases max i s
 
 /- [loops::sum_with_shared_borrows] -/
@@ -106,8 +104,7 @@ def list_nth_mut_loop_loop_fwd
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_mut_loop_loop_fwd ls i =>
-                                                 list_nth_mut_loop_loop_terminates
-                                                 T ls i
+  list_nth_mut_loop_loop_terminates T ls i
 decreasing_by list_nth_mut_loop_loop_decreases ls i
 
 /- [loops::list_nth_mut_loop] -/
@@ -129,8 +126,7 @@ def list_nth_mut_loop_loop_back
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_mut_loop_loop_back ls i ret0 =>
-                                                       list_nth_mut_loop_loop_terminates
-                                                       T ls i
+  list_nth_mut_loop_loop_terminates T ls i
 decreasing_by list_nth_mut_loop_loop_decreases ls i
 
 /- [loops::list_nth_mut_loop] -/
@@ -152,8 +148,7 @@ def list_nth_shared_loop_loop_fwd
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_shared_loop_loop_fwd ls i =>
-                                                    list_nth_shared_loop_loop_terminates
-                                                    T ls i
+  list_nth_shared_loop_loop_terminates T ls i
 decreasing_by list_nth_shared_loop_loop_decreases ls i
 
 /- [loops::list_nth_shared_loop] -/
@@ -191,8 +186,8 @@ def get_elem_mut_loop_back
         result.ret (list_t.ListCons y tl0)
   | list_t.ListNil => result.fail error.panic
   
-termination_by get_elem_mut_loop_back x ls ret0 => get_elem_mut_loop_terminates
-                                                  x ls
+termination_by get_elem_mut_loop_back x ls ret0 =>
+  get_elem_mut_loop_terminates x ls
 decreasing_by get_elem_mut_loop_decreases x ls
 
 /- [loops::get_elem_mut] -/
@@ -214,8 +209,8 @@ def get_elem_shared_loop_fwd
     if y = x then result.ret y else get_elem_shared_loop_fwd x tl
   | list_t.ListNil => result.fail error.panic
   
-termination_by get_elem_shared_loop_fwd x ls => get_elem_shared_loop_terminates
-                                               x ls
+termination_by get_elem_shared_loop_fwd x ls =>
+  get_elem_shared_loop_terminates x ls
 decreasing_by get_elem_shared_loop_decreases x ls
 
 /- [loops::get_elem_shared] -/
@@ -251,8 +246,7 @@ def list_nth_mut_loop_with_id_loop_fwd
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_mut_loop_with_id_loop_fwd i ls =>
-                                                         list_nth_mut_loop_with_id_loop_terminates
-                                                         T i ls
+  list_nth_mut_loop_with_id_loop_terminates T i ls
 decreasing_by list_nth_mut_loop_with_id_loop_decreases i ls
 
 /- [loops::list_nth_mut_loop_with_id] -/
@@ -277,8 +271,7 @@ def list_nth_mut_loop_with_id_loop_back
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_mut_loop_with_id_loop_back i ls ret0 =>
-                                                               list_nth_mut_loop_with_id_loop_terminates
-                                                               T i ls
+  list_nth_mut_loop_with_id_loop_terminates T i ls
 decreasing_by list_nth_mut_loop_with_id_loop_decreases i ls
 
 /- [loops::list_nth_mut_loop_with_id] -/
@@ -303,8 +296,7 @@ def list_nth_shared_loop_with_id_loop_fwd
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_shared_loop_with_id_loop_fwd i ls =>
-                                                            list_nth_shared_loop_with_id_loop_terminates
-                                                            T i ls
+  list_nth_shared_loop_with_id_loop_terminates T i ls
 decreasing_by list_nth_shared_loop_with_id_loop_decreases i ls
 
 /- [loops::list_nth_shared_loop_with_id] -/
@@ -334,8 +326,7 @@ def list_nth_mut_loop_pair_loop_fwd
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_mut_loop_pair_loop_fwd ls0 ls1 i =>
-                                                           list_nth_mut_loop_pair_loop_terminates
-                                                           T ls0 ls1 i
+  list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i
 
 /- [loops::list_nth_mut_loop_pair] -/
@@ -366,8 +357,7 @@ def list_nth_mut_loop_pair_loop_back'a
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_mut_loop_pair_loop_back'a ls0 ls1 i ret0 =>
-                                                                   list_nth_mut_loop_pair_loop_terminates
-                                                                   T ls0 ls1 i
+  list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i
 
 /- [loops::list_nth_mut_loop_pair] -/
@@ -398,8 +388,7 @@ def list_nth_mut_loop_pair_loop_back'b
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_mut_loop_pair_loop_back'b ls0 ls1 i ret0 =>
-                                                                   list_nth_mut_loop_pair_loop_terminates
-                                                                   T ls0 ls1 i
+  list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i
 
 /- [loops::list_nth_mut_loop_pair] -/
@@ -429,8 +418,7 @@ def list_nth_shared_loop_pair_loop_fwd
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_shared_loop_pair_loop_fwd ls0 ls1 i =>
-                                                              list_nth_shared_loop_pair_loop_terminates
-                                                              T ls0 ls1 i
+  list_nth_shared_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_loop_pair_loop_decreases ls0 ls1 i
 
 /- [loops::list_nth_shared_loop_pair] -/
@@ -460,8 +448,7 @@ def list_nth_mut_loop_pair_merge_loop_fwd
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_mut_loop_pair_merge_loop_fwd ls0 ls1 i =>
-                                                                 list_nth_mut_loop_pair_merge_loop_terminates
-                                                                 T ls0 ls1 i
+  list_nth_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_merge_loop_decreases ls0 ls1 i
 
 /- [loops::list_nth_mut_loop_pair_merge] -/
@@ -495,7 +482,7 @@ def list_nth_mut_loop_pair_merge_loop_back
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_mut_loop_pair_merge_loop_back ls0 ls1 i ret0 =>
-   list_nth_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
+  list_nth_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_merge_loop_decreases ls0 ls1 i
 
 /- [loops::list_nth_mut_loop_pair_merge] -/
@@ -525,8 +512,7 @@ def list_nth_shared_loop_pair_merge_loop_fwd
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_shared_loop_pair_merge_loop_fwd ls0 ls1 i =>
-                                                                    list_nth_shared_loop_pair_merge_loop_terminates
-                                                                    T ls0 ls1 i
+  list_nth_shared_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_loop_pair_merge_loop_decreases ls0 ls1 i
 
 /- [loops::list_nth_shared_loop_pair_merge] -/
@@ -556,8 +542,7 @@ def list_nth_mut_shared_loop_pair_loop_fwd
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_mut_shared_loop_pair_loop_fwd ls0 ls1 i =>
-                                                                  list_nth_mut_shared_loop_pair_loop_terminates
-                                                                  T ls0 ls1 i
+  list_nth_mut_shared_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_shared_loop_pair_loop_decreases ls0 ls1 i
 
 /- [loops::list_nth_mut_shared_loop_pair] -/
@@ -588,7 +573,7 @@ def list_nth_mut_shared_loop_pair_loop_back
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_mut_shared_loop_pair_loop_back ls0 ls1 i ret0 =>
-   list_nth_mut_shared_loop_pair_loop_terminates T ls0 ls1 i
+  list_nth_mut_shared_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_shared_loop_pair_loop_decreases ls0 ls1 i
 
 /- [loops::list_nth_mut_shared_loop_pair] -/
@@ -618,7 +603,7 @@ def list_nth_mut_shared_loop_pair_merge_loop_fwd
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_mut_shared_loop_pair_merge_loop_fwd ls0 ls1 i =>
-   list_nth_mut_shared_loop_pair_merge_loop_terminates T ls0 ls1 i
+  list_nth_mut_shared_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_shared_loop_pair_merge_loop_decreases ls0 ls1 i
 
 /- [loops::list_nth_mut_shared_loop_pair_merge] -/
@@ -650,7 +635,7 @@ def list_nth_mut_shared_loop_pair_merge_loop_back
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_mut_shared_loop_pair_merge_loop_back ls0 ls1 i ret0 =>
-   list_nth_mut_shared_loop_pair_merge_loop_terminates T ls0 ls1 i
+  list_nth_mut_shared_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_shared_loop_pair_merge_loop_decreases ls0 ls1 i
 
 /- [loops::list_nth_mut_shared_loop_pair_merge] -/
@@ -680,8 +665,7 @@ def list_nth_shared_mut_loop_pair_loop_fwd
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_shared_mut_loop_pair_loop_fwd ls0 ls1 i =>
-                                                                  list_nth_shared_mut_loop_pair_loop_terminates
-                                                                  T ls0 ls1 i
+  list_nth_shared_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_mut_loop_pair_loop_decreases ls0 ls1 i
 
 /- [loops::list_nth_shared_mut_loop_pair] -/
@@ -712,7 +696,7 @@ def list_nth_shared_mut_loop_pair_loop_back
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_shared_mut_loop_pair_loop_back ls0 ls1 i ret0 =>
-   list_nth_shared_mut_loop_pair_loop_terminates T ls0 ls1 i
+  list_nth_shared_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_mut_loop_pair_loop_decreases ls0 ls1 i
 
 /- [loops::list_nth_shared_mut_loop_pair] -/
@@ -742,7 +726,7 @@ def list_nth_shared_mut_loop_pair_merge_loop_fwd
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_shared_mut_loop_pair_merge_loop_fwd ls0 ls1 i =>
-   list_nth_shared_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
+  list_nth_shared_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_mut_loop_pair_merge_loop_decreases ls0 ls1 i
 
 /- [loops::list_nth_shared_mut_loop_pair_merge] -/
@@ -774,7 +758,7 @@ def list_nth_shared_mut_loop_pair_merge_loop_back
   | list_t.ListNil => result.fail error.panic
   
 termination_by list_nth_shared_mut_loop_pair_merge_loop_back ls0 ls1 i ret0 =>
-   list_nth_shared_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
+  list_nth_shared_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_mut_loop_pair_merge_loop_decreases ls0 ls1 i
 
 /- [loops::list_nth_shared_mut_loop_pair_merge] -/