diff --git a/creusot/tests/should_fail/bug/436_0.stderr b/creusot/tests/should_fail/bug/436_0.stderr
index 7f70e70fa4..1ed777cd7b 100644
--- a/creusot/tests/should_fail/bug/436_0.stderr
+++ b/creusot/tests/should_fail/bug/436_0.stderr
@@ -1,7 +1,7 @@
 error: called prophetic logic function `prophecy` in logic context
   --> 436_0.rs:15:23
    |
-15 |     b.g = snapshot! { prophecy(b) + 1i32 };
+15 |     b.g = snapshot! { prophecy(b) + 1 };
    |                       ^^^^^^^^
 
 error: aborting due to 1 previous error
diff --git a/creusot/tests/should_succeed/100doors.coma b/creusot/tests/should_succeed/100doors.coma
index f61a8065d5..b633da86ef 100644
--- a/creusot/tests/should_succeed/100doors.coma
+++ b/creusot/tests/should_succeed/100doors.coma
@@ -26,7 +26,7 @@ module M_100doors__f [#"100doors.rs" 18 0 18 10]
   let%span svec24 = "../../../creusot-contracts/src/std/vec.rs" 154 26 154 57
   let%span svec25 = "../../../creusot-contracts/src/std/vec.rs" 155 26 155 62
   let%span svec26 = "../../../creusot-contracts/src/std/vec.rs" 156 26 156 55
-  let%span sops27 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex27 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span siter28 = "../../../creusot-contracts/src/std/iter.rs" 86 20 86 24
   let%span siter29 = "../../../creusot-contracts/src/std/iter.rs" 92 8 92 19
   let%span srange30 = "../../../creusot-contracts/src/std/iter/range.rs" 33 15 33 24
@@ -90,7 +90,7 @@ module M_100doors__f [#"100doors.rs" 18 0 18 10]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : bool =
-    [%#sops27] Seq.get (view'0 self) ix
+    [%#sindex27] Seq.get (view'0 self) ix
   
   let rec from_elem'0 (elem:bool) (n:usize) (return'  (ret:t_Vec'0))= {[@expl:from_elem 'elem' type invariant] inv'2 elem}
     any
diff --git a/creusot/tests/should_succeed/bug/545.coma b/creusot/tests/should_succeed/bug/545.coma
index 4db4c532b5..b81b30661c 100644
--- a/creusot/tests/should_succeed/bug/545.coma
+++ b/creusot/tests/should_succeed/bug/545.coma
@@ -1,7 +1,5 @@
 module M_545__negative_is_negative [#"545.rs" 4 0 4 29]
-  let%span s5450 = "545.rs" 5 18 5 32
-  
-  use prelude.prelude.Int32
+  let%span s5450 = "545.rs" 5 18 5 26
   
   use prelude.prelude.Int
   
@@ -10,6 +8,6 @@ module M_545__negative_is_negative [#"545.rs" 4 0 4 29]
   meta "compute_max_steps" 1000000
   
   let rec negative_is_negative'0 (_1:()) (return'  (ret:()))= (! bb0
-    [ bb0 = s0 [ s0 = {[@expl:assertion] [%#s5450] (0 : int32) > (-100 : int32)} s1 | s1 = return' {_0} ]  ]
+    [ bb0 = s0 [ s0 = {[@expl:assertion] [%#s5450] 0 > - 100} s1 | s1 = return' {_0} ]  ]
     ) [ & _0 : () = any_l () ]  [ return' (result:())-> (! return' {result}) ] 
 end
diff --git a/creusot/tests/should_succeed/bug/545/why3session.xml b/creusot/tests/should_succeed/bug/545/why3session.xml
index 3da0b4cb10..3cd235676d 100644
--- a/creusot/tests/should_succeed/bug/545/why3session.xml
+++ b/creusot/tests/should_succeed/bug/545/why3session.xml
@@ -6,7 +6,7 @@
 <file format="coma" proved="true">
 <path name=".."/><path name="545.coma"/>
 <theory name="M_545__negative_is_negative" proved="true">
- <goal name="vc_negative_is_negative" proved="true">
+ <goal name="vc_negative_is_negative&#39;0" proved="true">
  <proof prover="0"><result status="valid" time="0.013525" steps="0"/></proof>
  </goal>
 </theory>
diff --git a/creusot/tests/should_succeed/bug/545/why3shapes.gz b/creusot/tests/should_succeed/bug/545/why3shapes.gz
index aa29824d32..0188dc9cb0 100644
Binary files a/creusot/tests/should_succeed/bug/545/why3shapes.gz and b/creusot/tests/should_succeed/bug/545/why3shapes.gz differ
diff --git a/creusot/tests/should_succeed/bug/682.coma b/creusot/tests/should_succeed/bug/682.coma
index 628e011596..890d34a4c5 100644
--- a/creusot/tests/should_succeed/bug/682.coma
+++ b/creusot/tests/should_succeed/bug/682.coma
@@ -1,29 +1,35 @@
 module M_682__add_some [#"682.rs" 6 0 6 24]
   let%span s6820 = "682.rs" 7 10 7 11
-  let%span s6821 = "682.rs" 4 11 4 32
+  let%span s6821 = "682.rs" 4 11 4 35
   let%span s6822 = "682.rs" 5 10 5 17
-  let%span sresolve3 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
+  let%span sarithmetic3 = "../../../../creusot-contracts/src/logic/ops/arithmetic.rs" 92 28 92 42
+  let%span sresolve4 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   
   use prelude.prelude.UInt64
   
   use prelude.prelude.Borrow
   
   predicate resolve'1 (self : borrowed uint64) =
-    [%#sresolve3] self.final = self.current
+    [%#sresolve4] self.final = self.current
   
   predicate resolve'0 (_1 : borrowed uint64) =
     resolve'1 _1
   
   use prelude.prelude.Intrinsic
   
+  use prelude.prelude.UInt64
+  
   constant v_MAX'0 : uint64 = (18446744073709551615 : uint64)
   
   use prelude.prelude.Int
   
+  function div'0 (self : uint64) (other : uint64) : int =
+    [%#sarithmetic3] div (UInt64.to_int self) (UInt64.to_int other)
+  
   meta "compute_max_steps" 1000000
   
-  let rec add_some'0 (a:borrowed uint64) (return'  (ret:()))= {[@expl:add_some requires] [%#s6821] a.current
-    <= div (v_MAX'0 : uint64) (2 : uint64)}
+  let rec add_some'0 (a:borrowed uint64) (return'  (ret:()))= {[@expl:add_some requires] [%#s6821] UInt64.to_int a.current
+    <= div'0 (v_MAX'0 : uint64) (2 : uint64)}
     (! bb0
     [ bb0 = s0
       [ s0 = UInt64.add {a.current} {[%#s6820] (1 : uint64)}
@@ -40,9 +46,10 @@ module M_682__foo [#"682.rs" 12 0 12 23]
   let%span s6821 = "682.rs" 15 18 15 27
   let%span s6822 = "682.rs" 10 11 10 21
   let%span s6823 = "682.rs" 11 10 11 17
-  let%span s6824 = "682.rs" 4 11 4 32
+  let%span s6824 = "682.rs" 4 11 4 35
   let%span s6825 = "682.rs" 5 10 5 17
-  let%span sresolve6 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
+  let%span sarithmetic6 = "../../../../creusot-contracts/src/logic/ops/arithmetic.rs" 92 28 92 42
+  let%span sresolve7 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   
   use prelude.prelude.Borrow
   
@@ -50,16 +57,21 @@ module M_682__foo [#"682.rs" 12 0 12 23]
   
   use prelude.prelude.UInt64
   
+  use prelude.prelude.UInt64
+  
   constant v_MAX'0 : uint64 = (18446744073709551615 : uint64)
   
   use prelude.prelude.Int
   
-  let rec add_some'0 (a:borrowed uint64) (return'  (ret:()))= {[@expl:add_some requires] [%#s6824] a.current
-    <= div (v_MAX'0 : uint64) (2 : uint64)}
+  function div'0 (self : uint64) (other : uint64) : int =
+    [%#sarithmetic6] div (UInt64.to_int self) (UInt64.to_int other)
+  
+  let rec add_some'0 (a:borrowed uint64) (return'  (ret:()))= {[@expl:add_some requires] [%#s6824] UInt64.to_int a.current
+    <= div'0 (v_MAX'0 : uint64) (2 : uint64)}
     any [ return' (result:())-> {[%#s6825] a.final > a.current} (! return' {result}) ] 
   
   predicate resolve'1 (self : borrowed uint64) =
-    [%#sresolve6] self.final = self.current
+    [%#sresolve7] self.final = self.current
   
   predicate resolve'0 (_1 : borrowed uint64) =
     resolve'1 _1
diff --git a/creusot/tests/should_succeed/bug/682/why3session.xml b/creusot/tests/should_succeed/bug/682/why3session.xml
index f21977ed1c..f7e906ff8a 100644
--- a/creusot/tests/should_succeed/bug/682/why3session.xml
+++ b/creusot/tests/should_succeed/bug/682/why3session.xml
@@ -6,13 +6,13 @@
 <file format="coma" proved="true">
 <path name=".."/><path name="682.coma"/>
 <theory name="M_682__add_some" proved="true">
- <goal name="vc_add_some" proved="true">
- <proof prover="0"><result status="valid" time="0.021784" steps="99"/></proof>
+ <goal name="vc_add_some&#39;0" proved="true">
+ <proof prover="0"><result status="valid" time="0.021784" steps="142"/></proof>
  </goal>
 </theory>
 <theory name="M_682__foo" proved="true">
- <goal name="vc_foo" proved="true">
- <proof prover="0"><result status="valid" time="0.026729" steps="120"/></proof>
+ <goal name="vc_foo&#39;0" proved="true">
+ <proof prover="0"><result status="valid" time="0.026729" steps="150"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/creusot/tests/should_succeed/bug/682/why3shapes.gz b/creusot/tests/should_succeed/bug/682/why3shapes.gz
index 2821fcbf16..a2354c5dfc 100644
Binary files a/creusot/tests/should_succeed/bug/682/why3shapes.gz and b/creusot/tests/should_succeed/bug/682/why3shapes.gz differ
diff --git a/creusot/tests/should_succeed/bug/final_borrows.coma b/creusot/tests/should_succeed/bug/final_borrows.coma
index fa8dae297e..4073975abe 100644
--- a/creusot/tests/should_succeed/bug/final_borrows.coma
+++ b/creusot/tests/should_succeed/bug/final_borrows.coma
@@ -1937,7 +1937,7 @@ module M_final_borrows__index_mut_slice [#"final_borrows.rs" 208 0 208 48]
   let%span sfinal_borrows4 = "final_borrows.rs" 208 42 208 48
   let%span sfinal_borrows5 = "final_borrows.rs" 207 10 207 30
   let%span smodel6 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22
-  let%span sops7 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex7 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span sresolve8 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   let%span sslice9 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice10 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
@@ -2031,7 +2031,7 @@ module M_final_borrows__index_mut_slice [#"final_borrows.rs" 208 0 208 48]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 =
-    [%#sops7] Seq.get (view'1 self) ix
+    [%#sindex7] Seq.get (view'1 self) ix
   
   meta "compute_max_steps" 1000000
   
@@ -2100,7 +2100,7 @@ module M_final_borrows__index_mut_array [#"final_borrows.rs" 214 0 214 52]
   let%span sfinal_borrows4 = "final_borrows.rs" 214 46 214 52
   let%span sfinal_borrows5 = "final_borrows.rs" 213 10 213 35
   let%span smodel6 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22
-  let%span sops7 = "../../../../creusot-contracts/src/logic/ops.rs" 77 8 77 32
+  let%span sindex7 = "../../../../creusot-contracts/src/logic/ops/index.rs" 78 8 78 32
   let%span sresolve8 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   let%span sinvariant9 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sarray10 = "../../../../creusot-contracts/src/std/array.rs" 9 20 9 30
@@ -2184,7 +2184,7 @@ module M_final_borrows__index_mut_array [#"final_borrows.rs" 214 0 214 52]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : array t_T'0) (ix : usize) : t_T'0 =
-    [%#sops7] Seq.get (Slice.id self) (UIntSize.to_int ix)
+    [%#sindex7] Seq.get (Slice.id self) (UIntSize.to_int ix)
   
   meta "compute_max_steps" 1000000
   
diff --git a/creusot/tests/should_succeed/bug/two_phase.coma b/creusot/tests/should_succeed/bug/two_phase.coma
index 90d7e22713..b468704eed 100644
--- a/creusot/tests/should_succeed/bug/two_phase.coma
+++ b/creusot/tests/should_succeed/bug/two_phase.coma
@@ -3,7 +3,7 @@ module M_two_phase__test [#"two_phase.rs" 6 0 6 31]
   let%span svec1 = "../../../../creusot-contracts/src/std/vec.rs" 83 26 83 48
   let%span svec2 = "../../../../creusot-contracts/src/std/vec.rs" 87 26 87 56
   let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22
-  let%span sops4 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex4 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span smodel5 = "../../../../creusot-contracts/src/model.rs" 88 8 88 22
   let%span svec6 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span sresolve7 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
@@ -81,7 +81,7 @@ module M_two_phase__test [#"two_phase.rs" 6 0 6 31]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : usize =
-    [%#sops4] Seq.get (view'2 self) ix
+    [%#sindex4] Seq.get (view'2 self) ix
   
   meta "compute_max_steps" 1000000
   
diff --git a/creusot/tests/should_succeed/cell/01.coma b/creusot/tests/should_succeed/cell/01.coma
index 5eb9225304..a31161d15d 100644
--- a/creusot/tests/should_succeed/cell/01.coma
+++ b/creusot/tests/should_succeed/cell/01.coma
@@ -8,7 +8,7 @@ module M_01__adds_two [#"01.rs" 40 0 40 36]
   let%span s016 = "01.rs" 25 16 25 20
   let%span s017 = "01.rs" 25 22 25 23
   let%span s018 = "01.rs" 24 15 24 24
-  let%span s019 = "01.rs" 36 8 36 24
+  let%span s019 = "01.rs" 36 8 36 25
   
   use prelude.prelude.Borrow
   
@@ -31,10 +31,12 @@ module M_01__adds_two [#"01.rs" 40 0 40 36]
   
   axiom inv_axiom'1 [@rewrite] : forall x : uint32 [inv'1 x] . inv'1 x = true
   
+  use prelude.prelude.UInt32
+  
   use prelude.prelude.Int
   
   predicate inv'2 [#"01.rs" 35 4 35 26] (x : uint32) =
-    [%#s019] mod x (2 : uint32) = (0 : uint32)
+    [%#s019] mod (UInt32.to_int x) 2 = 0
   
   let rec get'0 (self:t_Cell'0) (return'  (ret:uint32))= {[@expl:get 'self' type invariant] [%#s013] inv'0 self}
     any [ return' (result:uint32)-> {[%#s014] inv'1 result} {[%#s015] inv'2 result} (! return' {result}) ] 
diff --git a/creusot/tests/should_succeed/cell/01/why3shapes.gz b/creusot/tests/should_succeed/cell/01/why3shapes.gz
index 99b9bee660..6b7e395ebf 100644
Binary files a/creusot/tests/should_succeed/cell/01/why3shapes.gz and b/creusot/tests/should_succeed/cell/01/why3shapes.gz differ
diff --git a/creusot/tests/should_succeed/cell/02.coma b/creusot/tests/should_succeed/cell/02.coma
index 980f8e2b7d..c515e97a4f 100644
--- a/creusot/tests/should_succeed/cell/02.coma
+++ b/creusot/tests/should_succeed/cell/02.coma
@@ -88,7 +88,7 @@ module M_02__fib_memo [#"02.rs" 95 0 95 50]
   let%span sslice30 = "../../../../creusot-contracts/src/std/slice.rs" 122 20 122 37
   let%span sslice31 = "../../../../creusot-contracts/src/std/slice.rs" 129 20 129 37
   let%span s0232 = "02.rs" 72 12 75 13
-  let%span sops33 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex33 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span svec34 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   
   use prelude.prelude.Borrow
@@ -236,7 +236,7 @@ module M_02__fib_memo [#"02.rs" 95 0 95 50]
   use prelude.prelude.Snapshot
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_Cell'0 =
-    [%#sops33] Seq.get (view'1 self) ix
+    [%#sindex33] Seq.get (view'1 self) ix
   
   predicate fib_cell'0 [#"02.rs" 84 0 84 32] (v : t_Vec'0) =
     [%#s0228] forall i : int . UIntSize.to_int ((index_logic'0 v i).t_Cell__ghost_inv'0).t_Fib__ix'0 = i
diff --git a/creusot/tests/should_succeed/filter_positive.coma b/creusot/tests/should_succeed/filter_positive.coma
index 807d00bb9c..1e0a6ba925 100644
--- a/creusot/tests/should_succeed/filter_positive.coma
+++ b/creusot/tests/should_succeed/filter_positive.coma
@@ -160,7 +160,7 @@ module M_filter_positive__m [#"filter_positive.rs" 82 0 82 33]
   let%span smodel39 = "../../../creusot-contracts/src/model.rs" 88 8 88 22
   let%span sslice40 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37
   let%span sslice41 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37
-  let%span sops42 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex42 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span smodel43 = "../../../creusot-contracts/src/model.rs" 106 8 106 22
   let%span sslice44 = "../../../creusot-contracts/src/std/slice.rs" 136 20 136 94
   let%span sresolve45 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
@@ -257,7 +257,7 @@ module M_filter_positive__m [#"filter_positive.rs" 82 0 82 33]
   axiom inv_axiom'4 [@rewrite] : forall x : t_Vec'0 [inv'4 x] . inv'4 x = true
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : int32 =
-    [%#sops42] Seq.get (view'0 self) ix
+    [%#sindex42] Seq.get (view'0 self) ix
   
   let rec from_elem'0 (elem:int32) (n:usize) (return'  (ret:t_Vec'0))= {[@expl:from_elem 'elem' type invariant] inv'3 elem}
     any
diff --git a/creusot/tests/should_succeed/ghost/ghost_vec.coma b/creusot/tests/should_succeed/ghost/ghost_vec.coma
index 71ff1072aa..d7d4f155ed 100644
--- a/creusot/tests/should_succeed/ghost/ghost_vec.coma
+++ b/creusot/tests/should_succeed/ghost/ghost_vec.coma
@@ -43,7 +43,7 @@ module M_ghost_vec__ghost_vec [#"ghost_vec.rs" 4 0 4 18]
   let%span sghost41 = "../../../../creusot-contracts/src/ghost.rs" 68 14 68 35
   let%span sseq42 = "../../../../creusot-contracts/src/logic/seq.rs" 445 22 445 26
   let%span sseq43 = "../../../../creusot-contracts/src/logic/seq.rs" 444 14 444 34
-  let%span sint44 = "../../../../creusot-contracts/src/logic/int.rs" 59 14 59 31
+  let%span sint44 = "../../../../creusot-contracts/src/logic/int.rs" 60 14 60 31
   let%span sghost45 = "../../../../creusot-contracts/src/ghost.rs" 199 22 199 26
   let%span sghost46 = "../../../../creusot-contracts/src/ghost.rs" 199 4 199 32
   let%span sghost47 = "../../../../creusot-contracts/src/ghost.rs" 197 14 197 31
diff --git a/creusot/tests/should_succeed/hashmap.coma b/creusot/tests/should_succeed/hashmap.coma
index 8b56ee3690..cee42e48af 100644
--- a/creusot/tests/should_succeed/hashmap.coma
+++ b/creusot/tests/should_succeed/hashmap.coma
@@ -47,7 +47,7 @@ module M_hashmap__qyi7664122466964245986__new [#"hashmap.rs" 116 4 116 46] (* My
   let%span svec4 = "../../../creusot-contracts/src/std/vec.rs" 181 22 181 76
   let%span shashmap5 = "hashmap.rs" 80 8 80 33
   let%span svec6 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops7 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex7 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span shashmap8 = "hashmap.rs" 86 8 86 53
   let%span shashmap9 = "hashmap.rs" 31 12 34 13
   let%span shashmap10 = "hashmap.rs" 107 12 108 139
@@ -142,7 +142,7 @@ module M_hashmap__qyi7664122466964245986__new [#"hashmap.rs" 116 4 116 46] (* My
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_List'0 =
-    [%#sops7] Seq.get (view'1 self) ix
+    [%#sindex7] Seq.get (view'1 self) ix
   
   let rec from_elem'0 (elem:t_List'0) (n:usize) (return'  (ret:t_Vec'0))= {[@expl:from_elem 'elem' type invariant] inv'1 elem}
     any
@@ -279,7 +279,7 @@ module M_hashmap__qyi7664122466964245986__add [#"hashmap.rs" 122 4 122 41] (* My
   let%span svec37 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sinvariant38 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sboxed39 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
-  let%span sops40 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex40 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span sinvariant41 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
   let%span sseq42 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
   let%span shashmap43 = "hashmap.rs" 107 12 108 139
@@ -548,7 +548,7 @@ module M_hashmap__qyi7664122466964245986__add [#"hashmap.rs" 122 4 122 41] (* My
     resolve'8 _1
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_List'0 =
-    [%#sops40] Seq.get (view'4 self) ix
+    [%#sindex40] Seq.get (view'4 self) ix
   
   predicate invariant'11 [#"hashmap.rs" 105 4 105 30] (self : t_MyHashMap'0) =
     [%#shashmap43] 0 < Seq.length (view'4 self.t_MyHashMap__buckets'0)
@@ -827,7 +827,7 @@ module M_hashmap__qyi7664122466964245986__get [#"hashmap.rs" 154 4 154 43] (* My
   let%span sslice17 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37
   let%span sslice18 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37
   let%span shashmap19 = "hashmap.rs" 91 20 91 66
-  let%span sops20 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex20 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span shashmap21 = "hashmap.rs" 80 8 80 33
   let%span svec22 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span sinvariant23 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
@@ -997,7 +997,7 @@ module M_hashmap__qyi7664122466964245986__get [#"hashmap.rs" 154 4 154 43] (* My
     [%#shashmap19] EuclideanDivision.mod (hash_log'0 k) (Seq.length (view'3 self.t_MyHashMap__buckets'0))
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_List'0 =
-    [%#sops20] Seq.get (view'3 self) ix
+    [%#sindex20] Seq.get (view'3 self) ix
   
   function bucket'0 [#"hashmap.rs" 85 4 85 54] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : t_List'0 =
     [%#shashmap12] index_logic'0 self.t_MyHashMap__buckets'0 (bucket_ix'0 self k)
@@ -1185,7 +1185,7 @@ module M_hashmap__qyi7664122466964245986__resize [#"hashmap.rs" 173 4 173 24] (*
   let%span shashmap24 = "hashmap.rs" 116 31 116 46
   let%span shashmap25 = "hashmap.rs" 115 14 115 62
   let%span svec26 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops27 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex27 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span shashmap28 = "hashmap.rs" 91 20 91 66
   let%span shashmap29 = "hashmap.rs" 80 8 80 33
   let%span ssnapshot30 = "../../../creusot-contracts/src/snapshot.rs" 52 20 52 39
@@ -1323,7 +1323,7 @@ module M_hashmap__qyi7664122466964245986__resize [#"hashmap.rs" 173 4 173 24] (*
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_List'0 =
-    [%#sops27] Seq.get (view'0 self) ix
+    [%#sindex27] Seq.get (view'0 self) ix
   
   type t_DeepModelTy'0
   
@@ -1720,7 +1720,7 @@ module M_hashmap__main [#"hashmap.rs" 213 0 213 13]
   let%span shashmap34 = "hashmap.rs" 31 12 34 13
   let%span shashmap35 = "hashmap.rs" 107 12 108 139
   let%span shashmap36 = "hashmap.rs" 91 20 91 66
-  let%span sops37 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex37 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span sinvariant38 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
   let%span svec39 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span shashmap40 = "hashmap.rs" 97 12 97 91
@@ -1773,7 +1773,7 @@ module M_hashmap__main [#"hashmap.rs" 213 0 213 13]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_List'0 =
-    [%#sops37] Seq.get (view'3 self) ix
+    [%#sindex37] Seq.get (view'3 self) ix
   
   type t_Option'1  =
     | C_None'0
diff --git a/creusot/tests/should_succeed/heapsort_generic.coma b/creusot/tests/should_succeed/heapsort_generic.coma
index 7cd87cf096..241a95d985 100644
--- a/creusot/tests/should_succeed/heapsort_generic.coma
+++ b/creusot/tests/should_succeed/heapsort_generic.coma
@@ -136,7 +136,7 @@ module M_heapsort_generic__sift_down [#"heapsort_generic.rs" 41 0 43 29]
   let%span sheapsort_generic23 = "heapsort_generic.rs" 11 4 11 19
   let%span smodel24 = "../../../creusot-contracts/src/model.rs" 97 8 97 28
   let%span smodel25 = "../../../creusot-contracts/src/model.rs" 106 8 106 22
-  let%span sops26 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex26 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span ssnapshot27 = "../../../creusot-contracts/src/snapshot.rs" 52 20 52 39
   let%span sseq28 = "../../../creusot-contracts/src/logic/seq.rs" 316 8 316 41
   let%span svec29 = "../../../creusot-contracts/src/std/vec.rs" 162 27 162 46
@@ -232,7 +232,7 @@ module M_heapsort_generic__sift_down [#"heapsort_generic.rs" 41 0 43 29]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 =
-    [%#sops26] Seq.get (view'2 self) ix
+    [%#sindex26] Seq.get (view'2 self) ix
   
   function deep_model'3 (self : t_T'0) : t_DeepModelTy'0
   
@@ -668,7 +668,7 @@ module M_heapsort_generic__heap_sort [#"heapsort_generic.rs" 94 0 96 29]
   let%span svec51 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span smodel52 = "../../../creusot-contracts/src/model.rs" 88 8 88 22
   let%span sheapsort_generic53 = "heapsort_generic.rs" 11 4 11 19
-  let%span sops54 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex54 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span sord55 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord56 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord57 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -785,7 +785,7 @@ module M_heapsort_generic__heap_sort [#"heapsort_generic.rs" 94 0 96 29]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 =
-    [%#sops54] Seq.get (view'2 self) ix
+    [%#sindex54] Seq.get (view'2 self) ix
   
   function deep_model'2 (self : t_T'0) : t_DeepModelTy'0
   
diff --git a/creusot/tests/should_succeed/hillel.coma b/creusot/tests/should_succeed/hillel.coma
index 64c06a9fb7..ad80df120c 100644
--- a/creusot/tests/should_succeed/hillel.coma
+++ b/creusot/tests/should_succeed/hillel.coma
@@ -15,7 +15,7 @@ module M_hillel__right_pad [#"hillel.rs" 17 0 17 59]
   let%span shillel13 = "hillel.rs" 16 10 16 73
   let%span ssnapshot14 = "../../../creusot-contracts/src/snapshot.rs" 52 20 52 39
   let%span smodel15 = "../../../creusot-contracts/src/model.rs" 106 8 106 22
-  let%span sops16 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex16 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span svec17 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48
   let%span svec18 = "../../../creusot-contracts/src/std/vec.rs" 87 26 87 56
   let%span svec19 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
@@ -82,7 +82,7 @@ module M_hillel__right_pad [#"hillel.rs" 17 0 17 59]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 =
-    [%#sops16] Seq.get (view'2 self) ix
+    [%#sindex16] Seq.get (view'2 self) ix
   
   use seq.Seq
   
@@ -229,7 +229,7 @@ module M_hillel__left_pad [#"hillel.rs" 34 0 34 58]
   let%span shillel13 = "hillel.rs" 31 10 31 62
   let%span shillel14 = "hillel.rs" 32 10 32 88
   let%span shillel15 = "hillel.rs" 33 10 33 104
-  let%span sops16 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex16 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span smodel17 = "../../../creusot-contracts/src/model.rs" 106 8 106 22
   let%span ssnapshot18 = "../../../creusot-contracts/src/snapshot.rs" 52 20 52 39
   let%span svec19 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48
@@ -292,7 +292,7 @@ module M_hillel__left_pad [#"hillel.rs" 34 0 34 58]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 =
-    [%#sops16] Seq.get (view'2 self) ix
+    [%#sindex16] Seq.get (view'2 self) ix
   
   function view'0 (self : borrowed (t_Vec'0)) : Seq.seq t_T'0 =
     [%#smodel17] view'2 self.current
@@ -505,11 +505,11 @@ module M_hillel__insert_unique [#"hillel.rs" 80 0 80 62]
   let%span svec23 = "../../../creusot-contracts/src/std/vec.rs" 169 26 169 42
   let%span sslice24 = "../../../creusot-contracts/src/std/slice.rs" 245 0 354 1
   let%span siter25 = "../../../creusot-contracts/src/std/iter.rs" 101 0 213 1
-  let%span sops26 = "../../../creusot-contracts/src/logic/ops.rs" 88 8 88 33
+  let%span sindex26 = "../../../creusot-contracts/src/logic/ops/index.rs" 89 8 89 33
   let%span smodel27 = "../../../creusot-contracts/src/model.rs" 79 8 79 28
   let%span sslice28 = "../../../creusot-contracts/src/std/slice.rs" 405 12 405 66
   let%span siter29 = "../../../creusot-contracts/src/std/iter.rs" 107 26 110 17
-  let%span sops30 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex30 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span scmp31 = "../../../creusot-contracts/src/std/cmp.rs" 11 26 11 75
   let%span shillel32 = "hillel.rs" 60 8 60 64
   let%span shillel33 = "hillel.rs" 53 8 53 105
@@ -533,7 +533,7 @@ module M_hillel__insert_unique [#"hillel.rs" 80 0 80 62]
   let%span smodel51 = "../../../creusot-contracts/src/model.rs" 106 8 106 22
   let%span sslice52 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice53 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
-  let%span sops54 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex54 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span sseq55 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
   let%span sinvariant56 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span svec57 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
@@ -604,7 +604,7 @@ module M_hillel__insert_unique [#"hillel.rs" 80 0 80 62]
   use seq.Seq
   
   function index_logic'1 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 =
-    [%#sops30] Seq.get (view'3 self) ix
+    [%#sindex30] Seq.get (view'3 self) ix
   
   function deep_model'1 (self : t_T'0) : t_DeepModelTy'0
   
@@ -724,7 +724,7 @@ module M_hillel__insert_unique [#"hillel.rs" 80 0 80 62]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : Snapshot.snap_ty (Seq.seq t_T'0)) (ix : int) : t_T'0 =
-    [%#sops26] Seq.get (Snapshot.inner self) ix
+    [%#sindex26] Seq.get (Snapshot.inner self) ix
   
   function deep_model'2 (self : t_T'0) : t_DeepModelTy'0 =
     [%#smodel27] deep_model'1 self
@@ -736,7 +736,7 @@ module M_hillel__insert_unique [#"hillel.rs" 80 0 80 62]
   use seq.Seq
   
   function index_logic'2 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 =
-    [%#sops54] Seq.get (view'5 self) ix
+    [%#sindex54] Seq.get (view'5 self) ix
   
   function to_ref_seq'0 (self : slice t_T'0) : Seq.seq t_T'0
   
@@ -1039,7 +1039,7 @@ module M_hillel__unique [#"hillel.rs" 102 0 102 56]
   let%span siter40 = "../../../creusot-contracts/src/std/iter.rs" 92 8 92 19
   let%span sslice41 = "../../../creusot-contracts/src/std/slice.rs" 40 14 40 44
   let%span sslice42 = "../../../creusot-contracts/src/std/slice.rs" 41 14 41 96
-  let%span sops43 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex43 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span shillel44 = "hillel.rs" 60 8 60 64
   let%span srange45 = "../../../creusot-contracts/src/std/iter/range.rs" 33 15 33 24
   let%span srange46 = "../../../creusot-contracts/src/std/iter/range.rs" 34 14 34 45
@@ -1055,7 +1055,7 @@ module M_hillel__unique [#"hillel.rs" 102 0 102 56]
   let%span smodel56 = "../../../creusot-contracts/src/model.rs" 97 8 97 28
   let%span sslice57 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice58 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
-  let%span sops59 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex59 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span svec60 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sinvariant61 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sinvariant62 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
@@ -1201,7 +1201,7 @@ module M_hillel__unique [#"hillel.rs" 102 0 102 56]
   use seq.Seq
   
   function index_logic'1 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 =
-    [%#sops59] Seq.get (view'2 self) ix
+    [%#sindex59] Seq.get (view'2 self) ix
   
   function deep_model'3 (self : t_T'0) : t_DeepModelTy'0
   
@@ -1222,7 +1222,7 @@ module M_hillel__unique [#"hillel.rs" 102 0 102 56]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 =
-    [%#sops43] Seq.get (view'1 self) ix
+    [%#sindex43] Seq.get (view'1 self) ix
   
   function deep_model'1 (self : t_Vec'0) : Seq.seq t_DeepModelTy'0
   
@@ -1595,7 +1595,7 @@ module M_hillel__score [#"hillel.rs" 147 0 147 38]
   let%span shillel9 = "hillel.rs" 148 4 148 41
   let%span shillel10 = "hillel.rs" 121 0 121 8
   let%span shillel11 = "hillel.rs" 138 4 140 5
-  let%span sint12 = "../../../creusot-contracts/src/logic/int.rs" 156 4 156 12
+  let%span sint12 = "../../../creusot-contracts/src/logic/int.rs" 157 4 157 12
   
   use prelude.prelude.Int
   
@@ -1713,7 +1713,7 @@ module M_hillel__fulcrum [#"hillel.rs" 159 0 159 30]
   let%span shillel57 = "hillel.rs" 136 10 136 85
   let%span shillel58 = "hillel.rs" 134 10 134 18
   let%span shillel59 = "hillel.rs" 138 4 140 5
-  let%span sint60 = "../../../creusot-contracts/src/logic/int.rs" 156 4 156 12
+  let%span sint60 = "../../../creusot-contracts/src/logic/int.rs" 157 4 157 12
   let%span srange61 = "../../../creusot-contracts/src/std/iter/range.rs" 33 15 33 24
   let%span srange62 = "../../../creusot-contracts/src/std/iter/range.rs" 34 14 34 45
   let%span srange63 = "../../../creusot-contracts/src/std/iter/range.rs" 39 15 39 21
@@ -1724,7 +1724,7 @@ module M_hillel__fulcrum [#"hillel.rs" 159 0 159 30]
   let%span srange68 = "../../../creusot-contracts/src/std/iter/range.rs" 44 14 44 42
   let%span snum69 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33
   let%span srange70 = "../../../creusot-contracts/src/std/iter/range.rs" 15 12 15 78
-  let%span sops71 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex71 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span smodel72 = "../../../creusot-contracts/src/model.rs" 106 8 106 22
   
   use prelude.prelude.UInt32
@@ -1815,7 +1815,7 @@ module M_hillel__fulcrum [#"hillel.rs" 159 0 159 30]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : slice uint32) (ix : int) : uint32 =
-    [%#sops71] Seq.get (view'1 self) ix
+    [%#sindex71] Seq.get (view'1 self) ix
   
   function to_ref_seq'0 (self : slice uint32) : Seq.seq uint32
   
diff --git a/creusot/tests/should_succeed/index_range.coma b/creusot/tests/should_succeed/index_range.coma
index f70ad1c3f5..ce63fe7fa8 100644
--- a/creusot/tests/should_succeed/index_range.coma
+++ b/creusot/tests/should_succeed/index_range.coma
@@ -9,7 +9,7 @@ module M_index_range__create_arr [#"index_range.rs" 14 0 14 27]
   let%span svec7 = "../../../creusot-contracts/src/std/vec.rs" 74 26 74 44
   let%span svec8 = "../../../creusot-contracts/src/std/vec.rs" 87 26 87 56
   let%span svec9 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops10 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex10 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span smodel11 = "../../../creusot-contracts/src/model.rs" 106 8 106 22
   
   use prelude.prelude.Opaque
@@ -79,7 +79,7 @@ module M_index_range__create_arr [#"index_range.rs" 14 0 14 27]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : int32 =
-    [%#sops10] Seq.get (view'0 self) ix
+    [%#sindex10] Seq.get (view'0 self) ix
   
   use prelude.prelude.Int32
   
@@ -229,7 +229,7 @@ module M_index_range__test_range [#"index_range.rs" 27 0 27 19]
   let%span svec84 = "../../../creusot-contracts/src/std/vec.rs" 156 26 156 55
   let%span svec85 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48
   let%span svec86 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops87 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex87 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span smodel88 = "../../../creusot-contracts/src/model.rs" 88 8 88 22
   let%span sslice89 = "../../../creusot-contracts/src/std/slice.rs" 144 20 144 70
   let%span sslice90 = "../../../creusot-contracts/src/std/slice.rs" 150 20 150 67
@@ -279,7 +279,7 @@ module M_index_range__test_range [#"index_range.rs" 27 0 27 19]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : int32 =
-    [%#sops87] Seq.get (view'0 self) ix
+    [%#sindex87] Seq.get (view'0 self) ix
   
   use prelude.prelude.Int32
   
@@ -861,7 +861,7 @@ module M_index_range__test_range_to [#"index_range.rs" 78 0 78 22]
   let%span svec57 = "../../../creusot-contracts/src/std/vec.rs" 156 26 156 55
   let%span svec58 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48
   let%span svec59 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops60 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex60 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span smodel61 = "../../../creusot-contracts/src/model.rs" 88 8 88 22
   let%span sslice62 = "../../../creusot-contracts/src/std/slice.rs" 167 20 167 42
   let%span sslice63 = "../../../creusot-contracts/src/std/slice.rs" 173 20 173 57
@@ -911,7 +911,7 @@ module M_index_range__test_range_to [#"index_range.rs" 78 0 78 22]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : int32 =
-    [%#sops60] Seq.get (view'0 self) ix
+    [%#sindex60] Seq.get (view'0 self) ix
   
   use prelude.prelude.Int32
   
@@ -1349,7 +1349,7 @@ module M_index_range__test_range_from [#"index_range.rs" 115 0 115 24]
   let%span svec59 = "../../../creusot-contracts/src/std/vec.rs" 156 26 156 55
   let%span svec60 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48
   let%span svec61 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops62 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex62 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span smodel63 = "../../../creusot-contracts/src/model.rs" 88 8 88 22
   let%span sslice64 = "../../../creusot-contracts/src/std/slice.rs" 187 20 187 44
   let%span sslice65 = "../../../creusot-contracts/src/std/slice.rs" 193 20 193 67
@@ -1399,7 +1399,7 @@ module M_index_range__test_range_from [#"index_range.rs" 115 0 115 24]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : int32 =
-    [%#sops62] Seq.get (view'0 self) ix
+    [%#sindex62] Seq.get (view'0 self) ix
   
   use prelude.prelude.Int32
   
@@ -1842,7 +1842,7 @@ module M_index_range__test_range_full [#"index_range.rs" 154 0 154 24]
   let%span svec51 = "../../../creusot-contracts/src/std/vec.rs" 156 26 156 55
   let%span svec52 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48
   let%span svec53 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops54 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex54 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span smodel55 = "../../../creusot-contracts/src/model.rs" 88 8 88 22
   let%span sslice56 = "../../../creusot-contracts/src/std/slice.rs" 209 20 209 24
   let%span sslice57 = "../../../creusot-contracts/src/std/slice.rs" 215 20 215 31
@@ -1892,7 +1892,7 @@ module M_index_range__test_range_full [#"index_range.rs" 154 0 154 24]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : int32 =
-    [%#sops54] Seq.get (view'0 self) ix
+    [%#sindex54] Seq.get (view'0 self) ix
   
   use prelude.prelude.Int32
   
@@ -2300,7 +2300,7 @@ module M_index_range__test_range_to_inclusive [#"index_range.rs" 179 0 179 32]
   let%span svec54 = "../../../creusot-contracts/src/std/vec.rs" 156 26 156 55
   let%span svec55 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48
   let%span svec56 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops57 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex57 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span smodel58 = "../../../creusot-contracts/src/model.rs" 88 8 88 22
   let%span sslice59 = "../../../creusot-contracts/src/std/slice.rs" 229 20 229 41
   let%span sslice60 = "../../../creusot-contracts/src/std/slice.rs" 235 20 235 61
@@ -2350,7 +2350,7 @@ module M_index_range__test_range_to_inclusive [#"index_range.rs" 179 0 179 32]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : int32 =
-    [%#sops57] Seq.get (view'0 self) ix
+    [%#sindex57] Seq.get (view'0 self) ix
   
   use prelude.prelude.Int32
   
diff --git a/creusot/tests/should_succeed/insertion_sort.coma b/creusot/tests/should_succeed/insertion_sort.coma
index 6cf0870e15..fd18bc1ade 100644
--- a/creusot/tests/should_succeed/insertion_sort.coma
+++ b/creusot/tests/should_succeed/insertion_sort.coma
@@ -30,8 +30,8 @@ module M_insertion_sort__insertion_sort [#"insertion_sort.rs" 21 0 21 40]
   let%span sinsertion_sort28 = "insertion_sort.rs" 8 8 8 72
   let%span srange29 = "../../../creusot-contracts/src/std/iter/range.rs" 23 12 27 70
   let%span siter30 = "../../../creusot-contracts/src/std/iter.rs" 107 26 110 17
-  let%span sops31 = "../../../creusot-contracts/src/logic/ops.rs" 55 8 55 32
-  let%span sops32 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex31 = "../../../creusot-contracts/src/logic/ops/index.rs" 56 8 56 32
+  let%span sindex32 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span sslice33 = "../../../creusot-contracts/src/std/slice.rs" 257 19 257 35
   let%span sslice34 = "../../../creusot-contracts/src/std/slice.rs" 258 19 258 35
   let%span sslice35 = "../../../creusot-contracts/src/std/slice.rs" 259 18 259 50
@@ -222,10 +222,10 @@ module M_insertion_sort__insertion_sort [#"insertion_sort.rs" 21 0 21 40]
     
   
   function index_logic'0 [@inline:trivial] (self : slice int32) (ix : usize) : int32 =
-    [%#sops31] Seq.get (view'2 self) (UIntSize.to_int ix)
+    [%#sindex31] Seq.get (view'2 self) (UIntSize.to_int ix)
   
   function index_logic'1 [@inline:trivial] (self : slice int32) (ix : int) : int32 =
-    [%#sops32] Seq.get (view'2 self) ix
+    [%#sindex32] Seq.get (view'2 self) ix
   
   predicate inv'5 (_1 : borrowed (slice int32))
   
diff --git a/creusot/tests/should_succeed/iterators/02_iter_mut.coma b/creusot/tests/should_succeed/iterators/02_iter_mut.coma
index 2b5aadbffb..7439a54975 100644
--- a/creusot/tests/should_succeed/iterators/02_iter_mut.coma
+++ b/creusot/tests/should_succeed/iterators/02_iter_mut.coma
@@ -9,7 +9,7 @@ module M_02_iter_mut__qyi4305820612590367313__produces_refl [#"02_iter_mut.rs" 5
   let%span s02_iter_mut7 = "02_iter_mut.rs" 22 20 22 64
   let%span sslice8 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice9 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
-  let%span sops10 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex10 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span sinvariant11 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sslice12 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
   let%span sseq13 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
@@ -102,7 +102,7 @@ module M_02_iter_mut__qyi4305820612590367313__produces_refl [#"02_iter_mut.rs" 5
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 =
-    [%#sops10] Seq.get (view'1 self) ix
+    [%#sindex10] Seq.get (view'1 self) ix
   
   function to_mut_seq'0 (self : borrowed (slice t_T'0)) : Seq.seq (borrowed t_T'0)
   
@@ -147,7 +147,7 @@ module M_02_iter_mut__qyi4305820612590367313__produces_trans [#"02_iter_mut.rs"
   let%span s02_iter_mut11 = "02_iter_mut.rs" 22 20 22 64
   let%span sslice12 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice13 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
-  let%span sops14 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex14 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span sinvariant15 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sslice16 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
   let%span sseq17 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
@@ -238,7 +238,7 @@ module M_02_iter_mut__qyi4305820612590367313__produces_trans [#"02_iter_mut.rs"
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 =
-    [%#sops14] Seq.get (view'1 self) ix
+    [%#sindex14] Seq.get (view'1 self) ix
   
   function to_mut_seq'0 (self : borrowed (slice t_T'0)) : Seq.seq (borrowed t_T'0)
   
@@ -287,7 +287,7 @@ module M_02_iter_mut__qyi4305820612590367313__next [#"02_iter_mut.rs" 67 4 67 44
   let%span sslice3 = "../../../../creusot-contracts/src/std/slice.rs" 291 18 298 9
   let%span s02_iter_mut4 = "02_iter_mut.rs" 32 8 32 76
   let%span s02_iter_mut5 = "02_iter_mut.rs" 39 12 43 13
-  let%span sops6 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex6 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span sslice7 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice8 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
   let%span sseq9 = "../../../../creusot-contracts/src/logic/seq.rs" 173 8 173 39
@@ -391,7 +391,7 @@ module M_02_iter_mut__qyi4305820612590367313__next [#"02_iter_mut.rs" 67 4 67 44
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 =
-    [%#sops6] Seq.get (view'0 self) ix
+    [%#sindex6] Seq.get (view'0 self) ix
   
   use seq.Seq
   
@@ -869,14 +869,14 @@ module M_02_iter_mut__all_zero [#"02_iter_mut.rs" 88 0 88 35]
   let%span s02_iter_mut14 = "02_iter_mut.rs" 74 17 74 21
   let%span s02_iter_mut15 = "02_iter_mut.rs" 74 26 74 30
   let%span s02_iter_mut16 = "02_iter_mut.rs" 73 14 73 28
-  let%span sops17 = "../../../../creusot-contracts/src/logic/ops.rs" 88 8 88 33
+  let%span sindex17 = "../../../../creusot-contracts/src/logic/ops/index.rs" 89 8 89 33
   let%span s02_iter_mut18 = "02_iter_mut.rs" 39 12 43 13
   let%span s02_iter_mut19 = "02_iter_mut.rs" 67 17 67 21
   let%span s02_iter_mut20 = "02_iter_mut.rs" 67 26 67 44
   let%span s02_iter_mut21 = "02_iter_mut.rs" 63 14 66 5
   let%span svec22 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span smodel23 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22
-  let%span sops24 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex24 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span sslice25 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice26 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
   let%span s02_iter_mut27 = "02_iter_mut.rs" 49 15 49 24
@@ -893,7 +893,7 @@ module M_02_iter_mut__all_zero [#"02_iter_mut.rs" 88 0 88 35]
   let%span sslice38 = "../../../../creusot-contracts/src/std/slice.rs" 88 14 88 84
   let%span s02_iter_mut39 = "02_iter_mut.rs" 32 8 32 76
   let%span sresolve40 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
-  let%span sops41 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex41 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span s02_iter_mut42 = "02_iter_mut.rs" 22 20 22 64
   let%span sinvariant43 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   
@@ -1002,7 +1002,7 @@ module M_02_iter_mut__all_zero [#"02_iter_mut.rs" 88 0 88 35]
   function index_logic'0 [@inline:trivial] (self : Snapshot.snap_ty (Seq.seq (borrowed usize))) (ix : int) : borrowed usize
     
    =
-    [%#sops17] Seq.get (Snapshot.inner self) ix
+    [%#sindex17] Seq.get (Snapshot.inner self) ix
   
   use prelude.prelude.Snapshot
   
@@ -1013,7 +1013,7 @@ module M_02_iter_mut__all_zero [#"02_iter_mut.rs" 88 0 88 35]
   use seq.Seq
   
   function index_logic'2 [@inline:trivial] (self : slice usize) (ix : int) : usize =
-    [%#sops41] Seq.get (view'3 self) ix
+    [%#sindex41] Seq.get (view'3 self) ix
   
   function to_mut_seq'0 (self : borrowed (slice usize)) : Seq.seq (borrowed usize)
   
@@ -1113,7 +1113,7 @@ module M_02_iter_mut__all_zero [#"02_iter_mut.rs" 88 0 88 35]
   use prelude.prelude.Snapshot
   
   function index_logic'1 [@inline:trivial] (self : t_Vec'0) (ix : int) : usize =
-    [%#sops24] Seq.get (view'0 self) ix
+    [%#sindex24] Seq.get (view'0 self) ix
   
   meta "compute_max_steps" 1000000
   
@@ -1191,7 +1191,7 @@ module M_02_iter_mut__qyi4305820612590367313__produces_trans__refines [#"02_iter
   let%span sslice4 = "../../../../creusot-contracts/src/std/slice.rs" 88 14 88 84
   let%span sslice5 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice6 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
-  let%span sops7 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex7 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span s02_iter_mut8 = "02_iter_mut.rs" 22 20 22 64
   let%span sinvariant9 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sslice10 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
@@ -1239,7 +1239,7 @@ module M_02_iter_mut__qyi4305820612590367313__produces_trans__refines [#"02_iter
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 =
-    [%#sops7] Seq.get (view'1 self) ix
+    [%#sindex7] Seq.get (view'1 self) ix
   
   function to_mut_seq'0 (self : borrowed (slice t_T'0)) : Seq.seq (borrowed t_T'0)
   
@@ -1324,7 +1324,7 @@ module M_02_iter_mut__qyi4305820612590367313__next__refines [#"02_iter_mut.rs" 6
   let%span sinvariant7 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sslice8 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice9 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
-  let%span sops10 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex10 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span s02_iter_mut11 = "02_iter_mut.rs" 22 20 22 64
   let%span sslice12 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
   let%span sseq13 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
@@ -1439,7 +1439,7 @@ module M_02_iter_mut__qyi4305820612590367313__next__refines [#"02_iter_mut.rs" 6
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 =
-    [%#sops10] Seq.get (view'1 self) ix
+    [%#sindex10] Seq.get (view'1 self) ix
   
   function to_mut_seq'0 (self : borrowed (slice t_T'0)) : Seq.seq (borrowed t_T'0)
   
@@ -1499,7 +1499,7 @@ module M_02_iter_mut__qyi4305820612590367313__produces_refl__refines [#"02_iter_
   let%span s02_iter_mut5 = "02_iter_mut.rs" 22 20 22 64
   let%span sslice6 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice7 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
-  let%span sops8 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex8 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span sinvariant9 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sslice10 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
   let%span sseq11 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
@@ -1592,7 +1592,7 @@ module M_02_iter_mut__qyi4305820612590367313__produces_refl__refines [#"02_iter_
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 =
-    [%#sops8] Seq.get (view'1 self) ix
+    [%#sindex8] Seq.get (view'1 self) ix
   
   function to_mut_seq'0 (self : borrowed (slice t_T'0)) : Seq.seq (borrowed t_T'0)
   
diff --git a/creusot/tests/should_succeed/iterators/03_std_iterators.coma b/creusot/tests/should_succeed/iterators/03_std_iterators.coma
index ad3506963f..110f27a56c 100644
--- a/creusot/tests/should_succeed/iterators/03_std_iterators.coma
+++ b/creusot/tests/should_succeed/iterators/03_std_iterators.coma
@@ -28,7 +28,7 @@ module M_03_std_iterators__slice_iter [#"03_std_iterators.rs" 6 0 6 42]
   let%span sresolve26 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   let%span sslice27 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice28 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
-  let%span sops29 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex29 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span sseq30 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
   let%span smodel31 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22
   let%span sinvariant32 = "../../../../creusot-contracts/src/invariant.rs" 24 8 24 18
@@ -146,7 +146,7 @@ module M_03_std_iterators__slice_iter [#"03_std_iterators.rs" 6 0 6 42]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 =
-    [%#sops29] Seq.get (view'2 self) ix
+    [%#sindex29] Seq.get (view'2 self) ix
   
   function to_ref_seq'0 (self : slice t_T'0) : Seq.seq t_T'0
   
@@ -339,7 +339,7 @@ module M_03_std_iterators__vec_iter [#"03_std_iterators.rs" 17 0 17 41]
   let%span sslice24 = "../../../../creusot-contracts/src/std/slice.rs" 398 20 398 61
   let%span sresolve25 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   let%span svec26 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops27 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex27 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span sseq28 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
   let%span smodel29 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22
   let%span sslice30 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
@@ -471,7 +471,7 @@ module M_03_std_iterators__vec_iter [#"03_std_iterators.rs" 17 0 17 41]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 =
-    [%#sops27] Seq.get (view'5 self) ix
+    [%#sindex27] Seq.get (view'5 self) ix
   
   function to_ref_seq'0 (self : slice t_T'0) : Seq.seq t_T'0
   
@@ -651,12 +651,12 @@ module M_03_std_iterators__all_zero [#"03_std_iterators.rs" 28 0 28 35]
   let%span svec9 = "../../../../creusot-contracts/src/std/vec.rs" 176 26 176 48
   let%span sslice10 = "../../../../creusot-contracts/src/std/slice.rs" 245 0 354 1
   let%span siter11 = "../../../../creusot-contracts/src/std/iter.rs" 101 0 213 1
-  let%span sops12 = "../../../../creusot-contracts/src/logic/ops.rs" 88 8 88 33
+  let%span sindex12 = "../../../../creusot-contracts/src/logic/ops/index.rs" 89 8 89 33
   let%span sslice13 = "../../../../creusot-contracts/src/std/slice.rs" 459 12 459 66
   let%span siter14 = "../../../../creusot-contracts/src/std/iter.rs" 107 26 110 17
   let%span svec15 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span smodel16 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22
-  let%span sops17 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex17 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span sslice18 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice19 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
   let%span sslice20 = "../../../../creusot-contracts/src/std/slice.rs" 427 14 427 50
@@ -677,7 +677,7 @@ module M_03_std_iterators__all_zero [#"03_std_iterators.rs" 28 0 28 35]
   let%span sslice35 = "../../../../creusot-contracts/src/std/slice.rs" 88 14 88 84
   let%span sslice36 = "../../../../creusot-contracts/src/std/slice.rs" 452 20 452 61
   let%span sslice37 = "../../../../creusot-contracts/src/std/slice.rs" 437 20 437 36
-  let%span sops38 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex38 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   
   use prelude.prelude.Borrow
   
@@ -798,7 +798,7 @@ module M_03_std_iterators__all_zero [#"03_std_iterators.rs" 28 0 28 35]
   function index_logic'0 [@inline:trivial] (self : Snapshot.snap_ty (Seq.seq (borrowed usize))) (ix : int) : borrowed usize
     
    =
-    [%#sops12] Seq.get (Snapshot.inner self) ix
+    [%#sindex12] Seq.get (Snapshot.inner self) ix
   
   use prelude.prelude.Snapshot
   
@@ -809,7 +809,7 @@ module M_03_std_iterators__all_zero [#"03_std_iterators.rs" 28 0 28 35]
   use seq.Seq
   
   function index_logic'2 [@inline:trivial] (self : slice usize) (ix : int) : usize =
-    [%#sops38] Seq.get (view'3 self) ix
+    [%#sindex38] Seq.get (view'3 self) ix
   
   function to_mut_seq'0 (self : borrowed (slice usize)) : Seq.seq (borrowed usize)
   
@@ -906,7 +906,7 @@ module M_03_std_iterators__all_zero [#"03_std_iterators.rs" 28 0 28 35]
   use prelude.prelude.Snapshot
   
   function index_logic'1 [@inline:trivial] (self : t_Vec'0) (ix : int) : usize =
-    [%#sops17] Seq.get (view'0 self) ix
+    [%#sindex17] Seq.get (view'0 self) ix
   
   meta "compute_max_steps" 1000000
   
@@ -1373,7 +1373,7 @@ module M_03_std_iterators__counter [#"03_std_iterators.rs" 41 0 41 27]
   let%span smap_inv51 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 32 15 32 32
   let%span smap_inv52 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 33 15 33 32
   let%span smap_inv53 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 34 14 34 42
-  let%span sops54 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex54 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span smodel55 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22
   let%span sinvariant56 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   
@@ -1553,7 +1553,7 @@ module M_03_std_iterators__counter [#"03_std_iterators.rs" 41 0 41 27]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : slice uint32) (ix : int) : uint32 =
-    [%#sops54] Seq.get (view'4 self) ix
+    [%#sindex54] Seq.get (view'4 self) ix
   
   function to_ref_seq'0 (self : slice uint32) : Seq.seq uint32
   
@@ -2049,7 +2049,7 @@ module M_03_std_iterators__enumerate_range [#"03_std_iterators.rs" 72 0 72 24]
   let%span siter7 = "../../../../creusot-contracts/src/std/iter.rs" 154 27 154 103
   let%span siter8 = "../../../../creusot-contracts/src/std/iter.rs" 155 27 157 54
   let%span siter9 = "../../../../creusot-contracts/src/std/iter.rs" 101 0 213 1
-  let%span sops10 = "../../../../creusot-contracts/src/logic/ops.rs" 88 8 88 33
+  let%span sindex10 = "../../../../creusot-contracts/src/logic/ops/index.rs" 89 8 89 33
   let%span senumerate11 = "../../../../creusot-contracts/src/std/iter/enumerate.rs" 74 12 78 113
   let%span siter12 = "../../../../creusot-contracts/src/std/iter.rs" 107 26 110 17
   let%span srange13 = "../../../../creusot-contracts/src/std/iter/range.rs" 15 12 15 78
@@ -2206,7 +2206,7 @@ module M_03_std_iterators__enumerate_range [#"03_std_iterators.rs" 72 0 72 24]
   function index_logic'0 [@inline:trivial] (self : Snapshot.snap_ty (Seq.seq (usize, usize))) (ix : int) : (usize, usize)
     
    =
-    [%#sops10] Seq.get (Snapshot.inner self) ix
+    [%#sindex10] Seq.get (Snapshot.inner self) ix
   
   use prelude.prelude.Snapshot
   
@@ -2406,8 +2406,8 @@ module M_03_std_iterators__my_reverse [#"03_std_iterators.rs" 94 0 94 37]
   let%span sslice29 = "../../../../creusot-contracts/src/std/slice.rs" 257 19 257 35
   let%span sslice30 = "../../../../creusot-contracts/src/std/slice.rs" 258 19 258 35
   let%span sslice31 = "../../../../creusot-contracts/src/std/slice.rs" 259 18 259 50
-  let%span sops32 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
-  let%span sops33 = "../../../../creusot-contracts/src/logic/ops.rs" 55 8 55 32
+  let%span sindex32 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
+  let%span sindex33 = "../../../../creusot-contracts/src/logic/ops/index.rs" 56 8 56 32
   let%span sslice34 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice35 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
   let%span smodel36 = "../../../../creusot-contracts/src/model.rs" 88 8 88 22
@@ -2755,10 +2755,10 @@ module M_03_std_iterators__my_reverse [#"03_std_iterators.rs" 94 0 94 37]
     
   
   function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 =
-    [%#sops32] Seq.get (view'2 self) ix
+    [%#sindex32] Seq.get (view'2 self) ix
   
   function index_logic'1 [@inline:trivial] (self : slice t_T'0) (ix : usize) : t_T'0 =
-    [%#sops33] Seq.get (view'2 self) (UIntSize.to_int ix)
+    [%#sindex33] Seq.get (view'2 self) (UIntSize.to_int ix)
   
   predicate resolve'3 (self : borrowed (slice t_T'0)) =
     [%#sresolve51] self.final = self.current
diff --git a/creusot/tests/should_succeed/iterators/04_skip.coma b/creusot/tests/should_succeed/iterators/04_skip.coma
index 8217f71449..4b91306088 100644
--- a/creusot/tests/should_succeed/iterators/04_skip.coma
+++ b/creusot/tests/should_succeed/iterators/04_skip.coma
@@ -234,7 +234,7 @@ module M_04_skip__qyi17349041008065389927__next [#"04_skip.rs" 67 4 67 41] (* <S
   let%span s04_skip13 = "04_skip.rs" 63 14 66 5
   let%span smem14 = "../../../../creusot-contracts/src/std/mem.rs" 17 22 17 37
   let%span smem15 = "../../../../creusot-contracts/src/std/mem.rs" 18 22 18 42
-  let%span sops16 = "../../../../creusot-contracts/src/logic/ops.rs" 88 8 88 33
+  let%span sindex16 = "../../../../creusot-contracts/src/logic/ops/index.rs" 89 8 89 33
   let%span scommon17 = "common.rs" 31 17 31 21
   let%span scommon18 = "common.rs" 31 26 31 44
   let%span scommon19 = "common.rs" 27 14 30 5
@@ -331,7 +331,7 @@ module M_04_skip__qyi17349041008065389927__next [#"04_skip.rs" 67 4 67 41] (* <S
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : Snapshot.snap_ty (Seq.seq t_Item'0)) (ix : int) : t_Item'0 =
-    [%#sops16] Seq.get (Snapshot.inner self) ix
+    [%#sindex16] Seq.get (Snapshot.inner self) ix
   
   predicate resolve'1 (_1 : t_Item'0)
   
diff --git a/creusot/tests/should_succeed/iterators/08_collect_extend.coma b/creusot/tests/should_succeed/iterators/08_collect_extend.coma
index 9e5f757d12..277884730a 100644
--- a/creusot/tests/should_succeed/iterators/08_collect_extend.coma
+++ b/creusot/tests/should_succeed/iterators/08_collect_extend.coma
@@ -846,7 +846,7 @@ module M_08_collect_extend__collect_example [#"08_collect_extend.rs" 67 0 67 56]
   let%span s08_collect_extend4 = "08_collect_extend.rs" 46 40 46 52
   let%span s08_collect_extend5 = "08_collect_extend.rs" 42 2 44 49
   let%span svec6 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops7 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex7 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span siter8 = "../../../../creusot-contracts/src/std/iter.rs" 38 15 38 24
   let%span siter9 = "../../../../creusot-contracts/src/std/iter.rs" 39 14 39 45
   let%span siter10 = "../../../../creusot-contracts/src/std/iter.rs" 43 15 43 21
@@ -945,7 +945,7 @@ module M_08_collect_extend__collect_example [#"08_collect_extend.rs" 67 0 67 56]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : uint32 =
-    [%#sops7] Seq.get (view'0 self) ix
+    [%#sindex7] Seq.get (view'0 self) ix
   
   use prelude.prelude.UInt32
   
diff --git a/creusot/tests/should_succeed/iterators/17_filter.coma b/creusot/tests/should_succeed/iterators/17_filter.coma
index 2247cee782..eb47eeface 100644
--- a/creusot/tests/should_succeed/iterators/17_filter.coma
+++ b/creusot/tests/should_succeed/iterators/17_filter.coma
@@ -286,7 +286,7 @@ module M_17_filter__qyi17392541228996028033__next [#"17_filter.rs" 88 4 88 41] (
   let%span s17_filter9 = "17_filter.rs" 83 15 83 24
   let%span s17_filter10 = "17_filter.rs" 88 26 88 41
   let%span s17_filter11 = "17_filter.rs" 84 14 87 5
-  let%span sops12 = "../../../../creusot-contracts/src/logic/ops.rs" 88 8 88 33
+  let%span sindex12 = "../../../../creusot-contracts/src/logic/ops/index.rs" 89 8 89 33
   let%span scommon13 = "common.rs" 31 17 31 21
   let%span scommon14 = "common.rs" 31 26 31 44
   let%span scommon15 = "common.rs" 27 14 30 5
@@ -393,7 +393,7 @@ module M_17_filter__qyi17392541228996028033__next [#"17_filter.rs" 88 4 88 41] (
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : Snapshot.snap_ty (Seq.seq t_Item'0)) (ix : int) : t_Item'0 =
-    [%#sops12] Seq.get (Snapshot.inner self) ix
+    [%#sindex12] Seq.get (Snapshot.inner self) ix
   
   predicate precondition'0 (self : t_F'0) (args : t_Item'0)
   
@@ -787,7 +787,7 @@ module M_17_filter__less_than [#"17_filter.rs" 123 0 123 49]
   let%span siter6 = "../../../../creusot-contracts/src/std/iter.rs" 146 27 146 45
   let%span siter7 = "../../../../creusot-contracts/src/std/iter.rs" 172 26 174 81
   let%span svec8 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops9 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex9 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span sseq10 = "../../../../creusot-contracts/src/logic/seq.rs" 355 20 355 77
   let%span svec11 = "../../../../creusot-contracts/src/std/vec.rs" 191 20 191 24
   let%span svec12 = "../../../../creusot-contracts/src/std/vec.rs" 197 20 197 33
@@ -1122,7 +1122,7 @@ module M_17_filter__less_than [#"17_filter.rs" 123 0 123 49]
     
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : uint32 =
-    [%#sops9] Seq.get (view'0 self) ix
+    [%#sindex9] Seq.get (view'0 self) ix
   
   predicate contains'0 (self : Seq.seq uint32) (x : uint32) =
     [%#sseq10] exists i : int . 0 <= i /\ i < Seq.length self /\ Seq.get self i = x
diff --git a/creusot/tests/should_succeed/knapsack.coma b/creusot/tests/should_succeed/knapsack.coma
index 8a3707d40a..fb5f3e65ad 100644
--- a/creusot/tests/should_succeed/knapsack.coma
+++ b/creusot/tests/should_succeed/knapsack.coma
@@ -120,7 +120,7 @@ module M_knapsack__knapsack01_dyn [#"knapsack.rs" 49 0 49 91]
   let%span svec29 = "../../../creusot-contracts/src/std/vec.rs" 181 22 181 76
   let%span svec30 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48
   let%span smodel31 = "../../../creusot-contracts/src/model.rs" 88 8 88 22
-  let%span sops32 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex32 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span svec33 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span sknapsack34 = "knapsack.rs" 32 11 32 37
   let%span sknapsack35 = "knapsack.rs" 33 11 33 17
@@ -193,7 +193,7 @@ module M_knapsack__knapsack01_dyn [#"knapsack.rs" 49 0 49 91]
   use seq.Seq
   
   function index_logic'2 [@inline:trivial] (self : t_Vec'0) (ix : int) : usize =
-    [%#sops32] Seq.get (view'1 self) ix
+    [%#sindex32] Seq.get (view'1 self) ix
   
   let rec from_elem'0 (elem:usize) (n:usize) (return'  (ret:t_Vec'0))= {[@expl:from_elem 'elem' type invariant] inv'2 elem}
     any
@@ -304,7 +304,7 @@ module M_knapsack__knapsack01_dyn [#"knapsack.rs" 49 0 49 91]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'1) (ix : int) : t_Vec'0 =
-    [%#sops32] Seq.get (view'2 self) ix
+    [%#sindex32] Seq.get (view'2 self) ix
   
   let rec from_elem'1 (elem:t_Vec'0) (n:usize) (return'  (ret:t_Vec'1))= {[@expl:from_elem 'elem' type invariant] inv'3 elem}
     any
@@ -541,7 +541,7 @@ module M_knapsack__knapsack01_dyn [#"knapsack.rs" 49 0 49 91]
   use prelude.prelude.Intrinsic
   
   function index_logic'1 [@inline:trivial] (self : t_Vec'3) (ix : int) : t_Item'0 =
-    [%#sops32] Seq.get (view'3 self) ix
+    [%#sindex32] Seq.get (view'3 self) ix
   
   meta "compute_max_steps" 1000000
   
diff --git a/creusot/tests/should_succeed/knapsack_full.coma b/creusot/tests/should_succeed/knapsack_full.coma
index 6f012467dc..36dcc1c37e 100644
--- a/creusot/tests/should_succeed/knapsack_full.coma
+++ b/creusot/tests/should_succeed/knapsack_full.coma
@@ -347,7 +347,7 @@ module M_knapsack_full__knapsack01_dyn [#"knapsack_full.rs" 86 0 86 91]
   let%span svec42 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48
   let%span siter43 = "../../../creusot-contracts/src/std/iter.rs" 101 0 213 1
   let%span smodel44 = "../../../creusot-contracts/src/model.rs" 88 8 88 22
-  let%span sops45 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex45 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span svec46 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span sknapsack_full47 = "knapsack_full.rs" 61 11 61 37
   let%span sknapsack_full48 = "knapsack_full.rs" 62 11 62 17
@@ -459,7 +459,7 @@ module M_knapsack_full__knapsack01_dyn [#"knapsack_full.rs" 86 0 86 91]
   use seq.Seq
   
   function index_logic'3 [@inline:trivial] (self : t_Vec'0) (ix : int) : usize =
-    [%#sops45] Seq.get (view'1 self) ix
+    [%#sindex45] Seq.get (view'1 self) ix
   
   let rec from_elem'0 (elem:usize) (n:usize) (return'  (ret:t_Vec'0))= {[@expl:from_elem 'elem' type invariant] inv'5 elem}
     any
@@ -570,7 +570,7 @@ module M_knapsack_full__knapsack01_dyn [#"knapsack_full.rs" 86 0 86 91]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'1) (ix : int) : t_Vec'0 =
-    [%#sops45] Seq.get (view'2 self) ix
+    [%#sindex45] Seq.get (view'2 self) ix
   
   let rec from_elem'1 (elem:t_Vec'0) (n:usize) (return'  (ret:t_Vec'1))= {[@expl:from_elem 'elem' type invariant] inv'6 elem}
     any
@@ -1026,7 +1026,7 @@ module M_knapsack_full__knapsack01_dyn [#"knapsack_full.rs" 86 0 86 91]
     
   
   function index_logic'1 [@inline:trivial] (self : t_Vec'2) (ix : int) : t_Item'0 =
-    [%#sops45] Seq.get (view'3 self) ix
+    [%#sindex45] Seq.get (view'3 self) ix
   
   predicate invariant'3 (self : borrowed (t_Vec'2)) =
     [%#sinvariant109] inv'3 self.current /\ inv'3 self.final
@@ -1053,7 +1053,7 @@ module M_knapsack_full__knapsack01_dyn [#"knapsack_full.rs" 86 0 86 91]
   use prelude.prelude.Snapshot
   
   function index_logic'2 [@inline:trivial] (self : t_Vec'3) (ix : int) : t_Item'0 =
-    [%#sops45] Seq.get (view'4 self) ix
+    [%#sindex45] Seq.get (view'4 self) ix
   
   meta "compute_max_steps" 1000000
   
diff --git a/creusot/tests/should_succeed/list_reversal_lasso.coma b/creusot/tests/should_succeed/list_reversal_lasso.coma
index 1333ff6691..4988561f7f 100644
--- a/creusot/tests/should_succeed/list_reversal_lasso.coma
+++ b/creusot/tests/should_succeed/list_reversal_lasso.coma
@@ -9,7 +9,7 @@ module M_list_reversal_lasso__qyi13715866738248475091__index [#"list_reversal_la
   let%span sslice7 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37
   let%span sslice8 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37
   let%span svec9 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops10 = "../../../creusot-contracts/src/logic/ops.rs" 33 8 33 32
+  let%span sindex10 = "../../../creusot-contracts/src/logic/ops/index.rs" 34 8 34 32
   
   use prelude.prelude.Opaque
   
@@ -86,7 +86,7 @@ module M_list_reversal_lasso__qyi13715866738248475091__index [#"list_reversal_la
     /\ UIntSize.to_int i < Seq.length (view'1 self.t_Memory__0'0)
   
   function index_logic'1 [@inline:trivial] (self : t_Vec'0) (ix : usize) : usize =
-    [%#sops10] Seq.get (view'1 self) (UIntSize.to_int ix)
+    [%#sindex10] Seq.get (view'1 self) (UIntSize.to_int ix)
   
   function index_logic'0 [#"list_reversal_lasso.rs" 20 4 20 39] (self : t_Memory'0) (i : usize) : usize =
     [%#slist_reversal_lasso5] index_logic'1 self.t_Memory__0'0 i
@@ -127,7 +127,7 @@ module M_list_reversal_lasso__qyi14823043098042356205__index_mut [#"list_reversa
   let%span sslice15 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37
   let%span sslice16 = "../../../creusot-contracts/src/std/slice.rs" 136 20 136 94
   let%span sresolve17 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
-  let%span sops18 = "../../../creusot-contracts/src/logic/ops.rs" 33 8 33 32
+  let%span sindex18 = "../../../creusot-contracts/src/logic/ops/index.rs" 34 8 34 32
   
   use prelude.prelude.Borrow
   
@@ -225,7 +225,7 @@ module M_list_reversal_lasso__qyi14823043098042356205__index_mut [#"list_reversa
     /\ UIntSize.to_int i < Seq.length (view'0 self.t_Memory__0'0)
   
   function index_logic'1 [@inline:trivial] (self : t_Vec'0) (ix : usize) : usize =
-    [%#sops18] Seq.get (view'0 self) (UIntSize.to_int ix)
+    [%#sindex18] Seq.get (view'0 self) (UIntSize.to_int ix)
   
   function index_logic'0 [#"list_reversal_lasso.rs" 20 4 20 39] (self : t_Memory'0) (i : usize) : usize =
     [%#slist_reversal_lasso11] index_logic'1 self.t_Memory__0'0 i
@@ -296,7 +296,7 @@ module M_list_reversal_lasso__qyi2644757663130641572__list_reversal_safe [#"list
   let%span slist_reversal_lasso17 = "list_reversal_lasso.rs" 21 8 21 31
   let%span svec18 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span sresolve19 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
-  let%span sops20 = "../../../creusot-contracts/src/logic/ops.rs" 33 8 33 32
+  let%span sindex20 = "../../../creusot-contracts/src/logic/ops/index.rs" 34 8 34 32
   
   use prelude.prelude.UIntSize
   
@@ -345,7 +345,7 @@ module M_list_reversal_lasso__qyi2644757663130641572__list_reversal_safe [#"list
   use seq.Seq
   
   function index_logic'1 [@inline:trivial] (self : t_Vec'0) (ix : usize) : usize =
-    [%#sops20] Seq.get (view'0 self) (UIntSize.to_int ix)
+    [%#sindex20] Seq.get (view'0 self) (UIntSize.to_int ix)
   
   function index_logic'0 [#"list_reversal_lasso.rs" 20 4 20 39] (self : t_Memory'0) (i : usize) : usize =
     [%#slist_reversal_lasso17] index_logic'1 self.t_Memory__0'0 i
@@ -470,7 +470,7 @@ module M_list_reversal_lasso__qyi2644757663130641572__list_reversal_list [#"list
   let%span slist_reversal_lasso20 = "list_reversal_lasso.rs" 21 8 21 31
   let%span svec21 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span sresolve22 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
-  let%span sops23 = "../../../creusot-contracts/src/logic/ops.rs" 33 8 33 32
+  let%span sindex23 = "../../../creusot-contracts/src/logic/ops/index.rs" 34 8 34 32
   
   use prelude.prelude.UIntSize
   
@@ -529,7 +529,7 @@ module M_list_reversal_lasso__qyi2644757663130641572__list_reversal_list [#"list
     /\ UIntSize.to_int i < Seq.length (view'0 self.t_Memory__0'0)
   
   function index_logic'1 [@inline:trivial] (self : t_Vec'0) (ix : usize) : usize =
-    [%#sops23] Seq.get (view'0 self) (UIntSize.to_int ix)
+    [%#sindex23] Seq.get (view'0 self) (UIntSize.to_int ix)
   
   function index_logic'0 [#"list_reversal_lasso.rs" 20 4 20 39] (self : t_Memory'0) (i : usize) : usize =
     [%#slist_reversal_lasso20] index_logic'1 self.t_Memory__0'0 i
@@ -695,7 +695,7 @@ module M_list_reversal_lasso__qyi2644757663130641572__list_reversal_loop [#"list
   let%span slist_reversal_lasso12 = "list_reversal_lasso.rs" 124 14 124 89
   let%span slist_reversal_lasso13 = "list_reversal_lasso.rs" 13 0 13 15
   let%span slist_reversal_lasso14 = "list_reversal_lasso.rs" 83 12 85 98
-  let%span sops15 = "../../../creusot-contracts/src/logic/ops.rs" 88 8 88 33
+  let%span sindex15 = "../../../creusot-contracts/src/logic/ops/index.rs" 89 8 89 33
   let%span slist_reversal_lasso16 = "list_reversal_lasso.rs" 50 20 50 70
   let%span slist_reversal_lasso17 = "list_reversal_lasso.rs" 21 8 21 31
   let%span slist_reversal_lasso18 = "list_reversal_lasso.rs" 36 15 36 34
@@ -708,7 +708,7 @@ module M_list_reversal_lasso__qyi2644757663130641572__list_reversal_loop [#"list
   let%span sseq25 = "../../../creusot-contracts/src/logic/seq.rs" 251 8 251 27
   let%span slist_reversal_lasso26 = "list_reversal_lasso.rs" 118 12 118 53
   let%span svec27 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops28 = "../../../creusot-contracts/src/logic/ops.rs" 33 8 33 32
+  let%span sindex28 = "../../../creusot-contracts/src/logic/ops/index.rs" 34 8 34 32
   let%span sresolve29 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   
   use prelude.prelude.UIntSize
@@ -768,7 +768,7 @@ module M_list_reversal_lasso__qyi2644757663130641572__list_reversal_loop [#"list
     /\ UIntSize.to_int i < Seq.length (view'0 self.t_Memory__0'0)
   
   function index_logic'2 [@inline:trivial] (self : t_Vec'0) (ix : usize) : usize =
-    [%#sops28] Seq.get (view'0 self) (UIntSize.to_int ix)
+    [%#sindex28] Seq.get (view'0 self) (UIntSize.to_int ix)
   
   function index_logic'1 [#"list_reversal_lasso.rs" 20 4 20 39] (self : t_Memory'0) (i : usize) : usize =
     [%#slist_reversal_lasso17] index_logic'2 self.t_Memory__0'0 i
@@ -785,7 +785,7 @@ module M_list_reversal_lasso__qyi2644757663130641572__list_reversal_loop [#"list
   use prelude.prelude.Snapshot
   
   function index_logic'0 [@inline:trivial] (self : Snapshot.snap_ty (Seq.seq usize)) (ix : int) : usize =
-    [%#sops15] Seq.get (Snapshot.inner self) ix
+    [%#sindex15] Seq.get (Snapshot.inner self) ix
   
   use prelude.prelude.Snapshot
   
@@ -961,7 +961,7 @@ module M_list_reversal_lasso__qyi2644757663130641572__list_reversal_lasso [#"lis
   let%span slist_reversal_lasso6 = "list_reversal_lasso.rs" 192 16 192 36
   let%span slist_reversal_lasso7 = "list_reversal_lasso.rs" 161 15 161 38
   let%span slist_reversal_lasso8 = "list_reversal_lasso.rs" 162 14 162 54
-  let%span sops9 = "../../../creusot-contracts/src/logic/ops.rs" 88 8 88 33
+  let%span sindex9 = "../../../creusot-contracts/src/logic/ops/index.rs" 89 8 89 33
   let%span slist_reversal_lasso10 = "list_reversal_lasso.rs" 13 0 13 15
   let%span slist_reversal_lasso11 = "list_reversal_lasso.rs" 83 12 85 98
   let%span slist_reversal_lasso12 = "list_reversal_lasso.rs" 36 15 36 34
@@ -976,7 +976,7 @@ module M_list_reversal_lasso__qyi2644757663130641572__list_reversal_lasso [#"lis
   let%span slist_reversal_lasso21 = "list_reversal_lasso.rs" 21 8 21 31
   let%span svec22 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span sresolve23 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
-  let%span sops24 = "../../../creusot-contracts/src/logic/ops.rs" 33 8 33 32
+  let%span sindex24 = "../../../creusot-contracts/src/logic/ops/index.rs" 34 8 34 32
   
   use prelude.prelude.UIntSize
   
@@ -997,7 +997,7 @@ module M_list_reversal_lasso__qyi2644757663130641572__list_reversal_lasso [#"lis
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : Snapshot.snap_ty (Seq.seq usize)) (ix : int) : usize =
-    [%#sops9] Seq.get (Snapshot.inner self) ix
+    [%#sindex9] Seq.get (Snapshot.inner self) ix
   
   use prelude.prelude.Snapshot
   
@@ -1040,7 +1040,7 @@ module M_list_reversal_lasso__qyi2644757663130641572__list_reversal_lasso [#"lis
     /\ UIntSize.to_int i < Seq.length (view'0 self.t_Memory__0'0)
   
   function index_logic'2 [@inline:trivial] (self : t_Vec'0) (ix : usize) : usize =
-    [%#sops24] Seq.get (view'0 self) (UIntSize.to_int ix)
+    [%#sindex24] Seq.get (view'0 self) (UIntSize.to_int ix)
   
   function index_logic'1 [#"list_reversal_lasso.rs" 20 4 20 39] (self : t_Memory'0) (i : usize) : usize =
     [%#slist_reversal_lasso21] index_logic'2 self.t_Memory__0'0 i
@@ -1419,7 +1419,7 @@ module M_list_reversal_lasso__qyi2644757663130641572__find_lasso_aux [#"list_rev
   let%span slist_reversal_lasso22 = "list_reversal_lasso.rs" 205 8 209 9
   let%span slist_reversal_lasso23 = "list_reversal_lasso.rs" 220 8 232 9
   let%span slist_reversal_lasso24 = "list_reversal_lasso.rs" 21 8 21 31
-  let%span sops25 = "../../../creusot-contracts/src/logic/ops.rs" 33 8 33 32
+  let%span sindex25 = "../../../creusot-contracts/src/logic/ops/index.rs" 34 8 34 32
   
   use prelude.prelude.Opaque
   
@@ -1464,7 +1464,7 @@ module M_list_reversal_lasso__qyi2644757663130641572__find_lasso_aux [#"list_rev
   use seq.Seq
   
   function index_logic'1 [@inline:trivial] (self : t_Vec'0) (ix : usize) : usize =
-    [%#sops25] Seq.get (view'0 self) (UIntSize.to_int ix)
+    [%#sindex25] Seq.get (view'0 self) (UIntSize.to_int ix)
   
   function index_logic'0 [#"list_reversal_lasso.rs" 20 4 20 39] (self : t_Memory'0) (i : usize) : usize =
     [%#slist_reversal_lasso24] index_logic'1 self.t_Memory__0'0 i
@@ -1653,7 +1653,7 @@ module M_list_reversal_lasso__qyi2644757663130641572__find_lasso [#"list_reversa
   let%span slist_reversal_lasso26 = "list_reversal_lasso.rs" 199 14 202 5
   let%span slist_reversal_lasso27 = "list_reversal_lasso.rs" 203 14 203 25
   let%span slist_reversal_lasso28 = "list_reversal_lasso.rs" 205 8 209 9
-  let%span sops29 = "../../../creusot-contracts/src/logic/ops.rs" 33 8 33 32
+  let%span sindex29 = "../../../creusot-contracts/src/logic/ops/index.rs" 34 8 34 32
   
   use prelude.prelude.Opaque
   
@@ -1698,7 +1698,7 @@ module M_list_reversal_lasso__qyi2644757663130641572__find_lasso [#"list_reversa
   use seq.Seq
   
   function index_logic'1 [@inline:trivial] (self : t_Vec'0) (ix : usize) : usize =
-    [%#sops29] Seq.get (view'0 self) (UIntSize.to_int ix)
+    [%#sindex29] Seq.get (view'0 self) (UIntSize.to_int ix)
   
   function index_logic'0 [#"list_reversal_lasso.rs" 20 4 20 39] (self : t_Memory'0) (i : usize) : usize =
     [%#slist_reversal_lasso17] index_logic'1 self.t_Memory__0'0 i
diff --git a/creusot/tests/should_succeed/mc91.coma b/creusot/tests/should_succeed/mc91.coma
index 090ca71d25..08e2b4715f 100644
--- a/creusot/tests/should_succeed/mc91.coma
+++ b/creusot/tests/should_succeed/mc91.coma
@@ -2,7 +2,8 @@ module M_mc91__mc91 [#"mc91.rs" 7 0 7 26]
   let%span smc910 = "mc91.rs" 8 11 8 14
   let%span smc911 = "mc91.rs" 9 12 9 14
   let%span smc912 = "mc91.rs" 11 22 11 24
-  let%span smc913 = "mc91.rs" 5 10 6 38
+  let%span smc913 = "mc91.rs" 5 10 6 39
+  let%span sarithmetic4 = "../../../creusot-contracts/src/logic/ops/arithmetic.rs" 72 28 72 42
   
   use prelude.prelude.UInt32
   
@@ -10,6 +11,11 @@ module M_mc91__mc91 [#"mc91.rs" 7 0 7 26]
   
   use prelude.prelude.Int
   
+  use prelude.prelude.UInt32
+  
+  function sub'0 (self : uint32) (other : uint32) : int =
+    [%#sarithmetic4] UInt32.to_int self - UInt32.to_int other
+  
   meta "compute_max_steps" 1000000
   
   let rec mc91'0 (x:uint32) (return'  (ret:uint32))= (! bb0
@@ -36,7 +42,7 @@ module M_mc91__mc91 [#"mc91.rs" 7 0 7 26]
     | & _7 : uint32 = any_l () ]
     
     [ return' (result:uint32)-> {[@expl:mc91 ensures] [%#smc913] x <= (100 : uint32)
-       -> result = (91 : uint32) /\ x > (100 : uint32)  -> result = x - (10 : uint32)}
+       -> result = (91 : uint32) /\ x > (100 : uint32)  -> UInt32.to_int result = sub'0 x (10 : uint32)}
       (! return' {result}) ]
     
 end
diff --git a/creusot/tests/should_succeed/mc91/why3session.xml b/creusot/tests/should_succeed/mc91/why3session.xml
index 8ee1f7511e..08f10d8e5e 100644
--- a/creusot/tests/should_succeed/mc91/why3session.xml
+++ b/creusot/tests/should_succeed/mc91/why3session.xml
@@ -6,8 +6,8 @@
 <file format="coma" proved="true">
 <path name=".."/><path name="mc91.coma"/>
 <theory name="M_mc91__mc91" proved="true">
- <goal name="vc_mc91" proved="true">
- <proof prover="0"><result status="valid" time="0.024631" steps="42"/></proof>
+ <goal name="vc_mc91&#39;0" proved="true">
+ <proof prover="0"><result status="valid" time="0.024631" steps="54"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/creusot/tests/should_succeed/mc91/why3shapes.gz b/creusot/tests/should_succeed/mc91/why3shapes.gz
index 5ea964a99a..03f921796c 100644
Binary files a/creusot/tests/should_succeed/mc91/why3shapes.gz and b/creusot/tests/should_succeed/mc91/why3shapes.gz differ
diff --git a/creusot/tests/should_succeed/mutex.coma b/creusot/tests/should_succeed/mutex.coma
index f54c048d09..981f825a4a 100644
--- a/creusot/tests/should_succeed/mutex.coma
+++ b/creusot/tests/should_succeed/mutex.coma
@@ -8,7 +8,7 @@ module M_mutex__qyi5425553346843331945__call [#"mutex.rs" 100 4 100 23] (* <Adds
   let%span smutex6 = "mutex.rs" 49 4 49 35
   let%span smutex7 = "mutex.rs" 56 22 56 23
   let%span smutex8 = "mutex.rs" 55 4 55 30
-  let%span smutex9 = "mutex.rs" 67 8 67 24
+  let%span smutex9 = "mutex.rs" 67 8 67 25
   
   use prelude.prelude.Borrow
   
@@ -45,10 +45,12 @@ module M_mutex__qyi5425553346843331945__call [#"mutex.rs" 100 4 100 23] (* <Adds
   
   axiom inv_axiom'1 [@rewrite] : forall x : uint32 [inv'1 x] . inv'1 x = true
   
+  use prelude.prelude.UInt32
+  
   use prelude.prelude.Int
   
   predicate inv'2 [#"mutex.rs" 66 4 66 33] (self : ()) (x : uint32) =
-    [%#smutex9] mod x (2 : uint32) = (0 : uint32)
+    [%#smutex9] mod (UInt32.to_int x) 2 = 0
   
   let rec deref'0 (self:t_MutexGuard'0) (return'  (ret:uint32))= any
     [ return' (result:uint32)-> {[%#smutex5] inv'1 result}
@@ -120,7 +122,7 @@ module M_mutex__concurrent [#"mutex.rs" 163 0 163 19]
   let%span smutex9 = "mutex.rs" 130 11 130 27
   let%span smutex10 = "mutex.rs" 121 21 121 34
   let%span smutex11 = "mutex.rs" 117 14 120 5
-  let%span smutex12 = "mutex.rs" 67 8 67 24
+  let%span smutex12 = "mutex.rs" 67 8 67 25
   let%span sresolve13 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   let%span smutex14 = "mutex.rs" 92 8 92 12
   let%span smutex15 = "mutex.rs" 149 4 149 16
@@ -138,10 +140,12 @@ module M_mutex__concurrent [#"mutex.rs" 163 0 163 19]
   
   use prelude.prelude.Borrow
   
+  use prelude.prelude.UInt32
+  
   use prelude.prelude.Int
   
   predicate inv'2 [#"mutex.rs" 66 4 66 33] (self : ()) (x : uint32) =
-    [%#smutex12] mod x (2 : uint32) = (0 : uint32)
+    [%#smutex12] mod (UInt32.to_int x) 2 = 0
   
   type t_MutexInner'0
   
diff --git a/creusot/tests/should_succeed/mutex/why3shapes.gz b/creusot/tests/should_succeed/mutex/why3shapes.gz
index 1a899d0378..c015e86748 100644
Binary files a/creusot/tests/should_succeed/mutex/why3shapes.gz and b/creusot/tests/should_succeed/mutex/why3shapes.gz differ
diff --git a/creusot/tests/should_succeed/selection_sort_generic.coma b/creusot/tests/should_succeed/selection_sort_generic.coma
index 742b2f1c0a..4769680734 100644
--- a/creusot/tests/should_succeed/selection_sort_generic.coma
+++ b/creusot/tests/should_succeed/selection_sort_generic.coma
@@ -73,7 +73,7 @@ module M_selection_sort_generic__selection_sort [#"selection_sort_generic.rs" 30
   let%span smodel71 = "../../../creusot-contracts/src/model.rs" 79 8 79 28
   let%span sslice72 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice73 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
-  let%span sops74 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex74 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span svec75 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sslice76 = "../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
   let%span sinvariant77 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
@@ -196,7 +196,7 @@ module M_selection_sort_generic__selection_sort [#"selection_sort_generic.rs" 30
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 =
-    [%#sops74] Seq.get (view'2 self) ix
+    [%#sindex74] Seq.get (view'2 self) ix
   
   function deep_model'4 (self : t_T'0) : t_DeepModelTy'0
   
diff --git a/creusot/tests/should_succeed/slices/01.coma b/creusot/tests/should_succeed/slices/01.coma
index 566aa07f74..3e1c6156f3 100644
--- a/creusot/tests/should_succeed/slices/01.coma
+++ b/creusot/tests/should_succeed/slices/01.coma
@@ -65,7 +65,7 @@ module M_01__index_mut_slice [#"01.rs" 12 0 12 37]
   let%span s013 = "01.rs" 10 11 10 24
   let%span s014 = "01.rs" 11 10 11 23
   let%span smodel5 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22
-  let%span sops6 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex6 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span sresolve7 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   let%span sslice8 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice9 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
@@ -110,7 +110,7 @@ module M_01__index_mut_slice [#"01.rs" 12 0 12 37]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : slice uint32) (ix : int) : uint32 =
-    [%#sops6] Seq.get (view'1 self) ix
+    [%#sindex6] Seq.get (view'1 self) ix
   
   use prelude.prelude.UInt32
   
@@ -151,7 +151,7 @@ module M_01__slice_first [#"01.rs" 20 0 20 44]
   let%span s014 = "01.rs" 20 34 20 44
   let%span s015 = "01.rs" 16 10 19 1
   let%span sslice6 = "../../../../creusot-contracts/src/std/slice.rs" 245 0 354 1
-  let%span sops7 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex7 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span smodel8 = "../../../../creusot-contracts/src/model.rs" 88 8 88 22
   let%span sslice9 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice10 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
@@ -250,7 +250,7 @@ module M_01__slice_first [#"01.rs" 20 0 20 44]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 =
-    [%#sops7] Seq.get (view'1 self) ix
+    [%#sindex7] Seq.get (view'1 self) ix
   
   meta "compute_max_steps" 1000000
   
diff --git a/creusot/tests/should_succeed/slices/02_std.coma b/creusot/tests/should_succeed/slices/02_std.coma
index 86f5a7a3a5..a8ebbda3ab 100644
--- a/creusot/tests/should_succeed/slices/02_std.coma
+++ b/creusot/tests/should_succeed/slices/02_std.coma
@@ -11,7 +11,7 @@ module M_02_std__binary_search [#"02_std.rs" 8 0 8 40]
   let%span sresult9 = "../../../../creusot-contracts/src/std/result.rs" 53 27 53 53
   let%span sresult10 = "../../../../creusot-contracts/src/std/result.rs" 18 0 135 1
   let%span smodel11 = "../../../../creusot-contracts/src/model.rs" 88 8 88 22
-  let%span sops12 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex12 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span smodel13 = "../../../../creusot-contracts/src/model.rs" 79 8 79 28
   let%span sseq14 = "../../../../creusot-contracts/src/logic/seq.rs" 377 8 377 40
   let%span sslice15 = "../../../../creusot-contracts/src/std/slice.rs" 40 14 40 44
@@ -73,7 +73,7 @@ module M_02_std__binary_search [#"02_std.rs" 8 0 8 40]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : slice uint32) (ix : int) : uint32 =
-    [%#sops12] Seq.get (view'1 self) ix
+    [%#sindex12] Seq.get (view'1 self) ix
   
   use prelude.prelude.UInt32
   
diff --git a/creusot/tests/should_succeed/sparse_array.coma b/creusot/tests/should_succeed/sparse_array.coma
index 7972904278..0c34f1122a 100644
--- a/creusot/tests/should_succeed/sparse_array.coma
+++ b/creusot/tests/should_succeed/sparse_array.coma
@@ -13,7 +13,7 @@ module M_sparse_array__qyi912363311032332466__get [#"sparse_array.rs" 88 4 88 45
   let%span svec11 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span sinvariant12 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
   let%span ssparse_array13 = "sparse_array.rs" 72 20 73 52
-  let%span sops14 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex14 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span ssparse_array15 = "sparse_array.rs" 51 12 59 17
   let%span svec16 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sseq17 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
@@ -177,7 +177,7 @@ module M_sparse_array__qyi912363311032332466__get [#"sparse_array.rs" 88 4 88 45
   use prelude.prelude.Intrinsic
   
   function index_logic'1 [@inline:trivial] (self : t_Vec'0) (ix : int) : usize =
-    [%#sops14] Seq.get (view'4 self) ix
+    [%#sindex14] Seq.get (view'4 self) ix
   
   predicate invariant'3 [#"sparse_array.rs" 49 4 49 30] (self : t_Sparse'0) =
     [%#ssparse_array15] UIntSize.to_int self.t_Sparse__n'0 <= UIntSize.to_int self.t_Sparse__size'0
@@ -218,7 +218,7 @@ module M_sparse_array__qyi912363311032332466__get [#"sparse_array.rs" 88 4 88 45
     = i
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'1) (ix : int) : t_T'0 =
-    [%#sops14] Seq.get (view'5 self) ix
+    [%#sindex14] Seq.get (view'5 self) ix
   
   use prelude.prelude.Mapping
   
@@ -299,7 +299,7 @@ module M_sparse_array__qyi912363311032332466__lemma_permutation [#"sparse_array.
   let%span ssparse_array3 = "sparse_array.rs" 103 14 103 28
   let%span ssparse_array4 = "sparse_array.rs" 99 4 99 12
   let%span ssparse_array5 = "sparse_array.rs" 72 20 73 52
-  let%span sops6 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex6 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span ssparse_array7 = "sparse_array.rs" 51 12 59 17
   let%span svec8 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span svec9 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
@@ -371,7 +371,7 @@ module M_sparse_array__qyi912363311032332466__lemma_permutation [#"sparse_array.
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'1) (ix : int) : usize =
-    [%#sops6] Seq.get (view'0 self) ix
+    [%#sindex6] Seq.get (view'0 self) ix
   
   predicate invariant'0 [#"sparse_array.rs" 49 4 49 30] (self : t_Sparse'0) =
     [%#ssparse_array7] UIntSize.to_int self.t_Sparse__n'0 <= UIntSize.to_int self.t_Sparse__size'0
@@ -466,7 +466,7 @@ module M_sparse_array__qyi912363311032332466__set [#"sparse_array.rs" 112 4 112
   let%span sresolve27 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   let%span smodel28 = "../../../creusot-contracts/src/model.rs" 88 8 88 22
   let%span ssparse_array29 = "sparse_array.rs" 72 20 73 52
-  let%span sops30 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex30 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span svec31 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sinvariant32 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span ssparse_array33 = "sparse_array.rs" 51 12 59 17
@@ -642,7 +642,7 @@ module M_sparse_array__qyi912363311032332466__set [#"sparse_array.rs" 112 4 112
     
   
   function index_logic'1 [@inline:trivial] (self : t_Vec'1) (ix : int) : usize =
-    [%#sops30] Seq.get (view'6 self) ix
+    [%#sindex30] Seq.get (view'6 self) ix
   
   predicate invariant'4 [#"sparse_array.rs" 49 4 49 30] (self : t_Sparse'0) =
     [%#ssparse_array33] UIntSize.to_int self.t_Sparse__n'0 <= UIntSize.to_int self.t_Sparse__size'0
@@ -736,7 +736,7 @@ module M_sparse_array__qyi912363311032332466__set [#"sparse_array.rs" 112 4 112
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 =
-    [%#sops30] Seq.get (view'3 self) ix
+    [%#sindex30] Seq.get (view'3 self) ix
   
   use prelude.prelude.Mapping
   
@@ -883,7 +883,7 @@ module M_sparse_array__create [#"sparse_array.rs" 134 0 134 64]
   let%span svec8 = "../../../creusot-contracts/src/std/vec.rs" 181 22 181 76
   let%span ssparse_array9 = "sparse_array.rs" 40 12 41 82
   let%span svec10 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops11 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex11 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span ssparse_array12 = "sparse_array.rs" 72 20 73 52
   let%span ssparse_array13 = "sparse_array.rs" 51 12 59 17
   let%span svec14 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
@@ -953,7 +953,7 @@ module M_sparse_array__create [#"sparse_array.rs" 134 0 134 64]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 =
-    [%#sops11] Seq.get (view'1 self) ix
+    [%#sindex11] Seq.get (view'1 self) ix
   
   let rec from_elem'0 (elem:t_T'0) (n:usize) (return'  (ret:t_Vec'0))= {[@expl:from_elem 'elem' type invariant] inv'0 elem}
     any
@@ -994,7 +994,7 @@ module M_sparse_array__create [#"sparse_array.rs" 134 0 134 64]
   use seq.Seq
   
   function index_logic'1 [@inline:trivial] (self : t_Vec'1) (ix : int) : usize =
-    [%#sops11] Seq.get (view'2 self) ix
+    [%#sindex11] Seq.get (view'2 self) ix
   
   let rec from_elem'1 (elem:usize) (n:usize) (return'  (ret:t_Vec'1))= {[@expl:from_elem 'elem' type invariant] inv'3 elem}
     any
@@ -1144,7 +1144,7 @@ module M_sparse_array__f [#"sparse_array.rs" 140 0 140 10]
   let%span ssparse_array39 = "sparse_array.rs" 40 12 41 82
   let%span smodel40 = "../../../creusot-contracts/src/model.rs" 106 8 106 22
   let%span ssparse_array41 = "sparse_array.rs" 72 20 73 52
-  let%span sops42 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex42 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span ssparse_array43 = "sparse_array.rs" 51 12 59 17
   let%span svec44 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span sinvariant45 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
@@ -1219,7 +1219,7 @@ module M_sparse_array__f [#"sparse_array.rs" 140 0 140 10]
   use seq.Seq
   
   function index_logic'1 [@inline:trivial] (self : t_Vec'1) (ix : int) : usize =
-    [%#sops42] Seq.get (view'5 self) ix
+    [%#sindex42] Seq.get (view'5 self) ix
   
   predicate invariant'0 [#"sparse_array.rs" 49 4 49 30] (self : t_Sparse'0) =
     [%#ssparse_array43] UIntSize.to_int self.t_Sparse__n'0 <= UIntSize.to_int self.t_Sparse__size'0
@@ -1257,7 +1257,7 @@ module M_sparse_array__f [#"sparse_array.rs" 140 0 140 10]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : int32 =
-    [%#sops42] Seq.get (view'4 self) ix
+    [%#sindex42] Seq.get (view'4 self) ix
   
   use prelude.prelude.Mapping
   
diff --git a/creusot/tests/should_succeed/syntax/11_array_types.coma b/creusot/tests/should_succeed/syntax/11_array_types.coma
index 444a2be334..7d30c2b1a2 100644
--- a/creusot/tests/should_succeed/syntax/11_array_types.coma
+++ b/creusot/tests/should_succeed/syntax/11_array_types.coma
@@ -4,7 +4,7 @@ module M_11_array_types__omg [#"11_array_types.rs" 8 0 8 28]
   let%span s11_array_types2 = "11_array_types.rs" 9 13 9 14
   let%span s11_array_types3 = "11_array_types.rs" 11 20 11 32
   let%span s11_array_types4 = "11_array_types.rs" 7 11 7 53
-  let%span sops5 = "../../../../creusot-contracts/src/logic/ops.rs" 66 8 66 31
+  let%span sindex5 = "../../../../creusot-contracts/src/logic/ops/index.rs" 67 8 67 31
   
   use prelude.prelude.UIntSize
   
@@ -22,7 +22,7 @@ module M_11_array_types__omg [#"11_array_types.rs" 8 0 8 28]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : array int64) (ix : int) : int64 =
-    [%#sops5] Seq.get (Slice.id self) ix
+    [%#sindex5] Seq.get (Slice.id self) ix
   
   use prelude.prelude.Int64
   
diff --git a/creusot/tests/should_succeed/syntax/13_vec_macro.coma b/creusot/tests/should_succeed/syntax/13_vec_macro.coma
index d923ed6ea9..a7008dceab 100644
--- a/creusot/tests/should_succeed/syntax/13_vec_macro.coma
+++ b/creusot/tests/should_succeed/syntax/13_vec_macro.coma
@@ -13,7 +13,7 @@ module M_13_vec_macro__x [#"13_vec_macro.rs" 5 0 5 10]
   let%span svec11 = "../../../../creusot-contracts/src/std/vec.rs" 180 22 180 41
   let%span svec12 = "../../../../creusot-contracts/src/std/vec.rs" 181 22 181 76
   let%span sslice13 = "../../../../creusot-contracts/src/std/slice.rs" 332 18 332 35
-  let%span sops14 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex14 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span sboxed15 = "../../../../creusot-contracts/src/std/boxed.rs" 18 8 18 22
   let%span sslice16 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice17 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
@@ -94,7 +94,7 @@ module M_13_vec_macro__x [#"13_vec_macro.rs" 5 0 5 10]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'1) (ix : int) : int32 =
-    [%#sops14] Seq.get (view'1 self) ix
+    [%#sindex14] Seq.get (view'1 self) ix
   
   let rec from_elem'0 (elem:int32) (n:usize) (return'  (ret:t_Vec'1))= {[@expl:from_elem 'elem' type invariant] inv'1 elem}
     any
diff --git a/creusot/tests/should_succeed/syntax/derive_macros/mixed.coma b/creusot/tests/should_succeed/syntax/derive_macros/mixed.coma
index 056d5c2fc2..a427139c0a 100644
--- a/creusot/tests/should_succeed/syntax/derive_macros/mixed.coma
+++ b/creusot/tests/should_succeed/syntax/derive_macros/mixed.coma
@@ -463,7 +463,7 @@ module M_mixed__qyi9942470069884222103__resolve_coherence [#"mixed.rs" 49 9 49 1
   let%span svec3 = "../../../../../creusot-contracts/src/std/vec.rs" 49 20 49 83
   let%span sresolve4 = "../../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   let%span svec5 = "../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops6 = "../../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex6 = "../../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   
   use prelude.prelude.Borrow
   
@@ -510,7 +510,7 @@ module M_mixed__qyi9942470069884222103__resolve_coherence [#"mixed.rs" 49 9 49 1
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : uint32 =
-    [%#sops6] Seq.get (view'0 self) ix
+    [%#sindex6] Seq.get (view'0 self) ix
   
   predicate resolve'6 (_1 : uint32) =
     true
@@ -779,7 +779,7 @@ module M_mixed__qyi9942470069884222103__resolve_coherence__refines [#"mixed.rs"
   let%span sresolve3 = "../../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   let%span sinvariant4 = "../../../../../creusot-contracts/src/invariant.rs" 24 8 24 18
   let%span svec5 = "../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops6 = "../../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex6 = "../../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span sinvariant7 = "../../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   
   use prelude.prelude.Borrow
@@ -827,7 +827,7 @@ module M_mixed__qyi9942470069884222103__resolve_coherence__refines [#"mixed.rs"
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : uint32 =
-    [%#sops6] Seq.get (view'0 self) ix
+    [%#sindex6] Seq.get (view'0 self) ix
   
   predicate resolve'6 (_1 : uint32) =
     true
diff --git a/creusot/tests/should_succeed/syntax/int_suffix.coma b/creusot/tests/should_succeed/syntax/int_suffix.coma
index 970b9d939e..c5f525b145 100644
--- a/creusot/tests/should_succeed/syntax/int_suffix.coma
+++ b/creusot/tests/should_succeed/syntax/int_suffix.coma
@@ -2,7 +2,7 @@ module M_int_suffix__foo [#"int_suffix.rs" 5 0 5 29]
   let%span sint_suffix0 = "int_suffix.rs" 4 10 4 25
   let%span sint_suffix1 = "int_suffix.rs" 6 11 6 15
   let%span sghost2 = "../../../../creusot-contracts/src/ghost.rs" 217 9 217 15
-  let%span sint3 = "../../../../creusot-contracts/src/logic/int.rs" 59 14 59 31
+  let%span sint3 = "../../../../creusot-contracts/src/logic/int.rs" 60 14 60 31
   let%span sghost4 = "../../../../creusot-contracts/src/ghost.rs" 199 22 199 26
   let%span sghost5 = "../../../../creusot-contracts/src/ghost.rs" 199 4 199 32
   let%span sghost6 = "../../../../creusot-contracts/src/ghost.rs" 197 14 197 31
diff --git a/creusot/tests/should_succeed/take_first_mut.coma b/creusot/tests/should_succeed/take_first_mut.coma
index d95fb3827f..ff4c89567d 100644
--- a/creusot/tests/should_succeed/take_first_mut.coma
+++ b/creusot/tests/should_succeed/take_first_mut.coma
@@ -5,7 +5,7 @@ module M_take_first_mut__take_first_mut [#"take_first_mut.rs" 14 0 14 74]
   let%span smem3 = "../../../creusot-contracts/src/std/mem.rs" 17 22 17 37
   let%span smem4 = "../../../creusot-contracts/src/std/mem.rs" 18 22 18 42
   let%span sslice5 = "../../../creusot-contracts/src/std/slice.rs" 279 18 287 9
-  let%span sops6 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex6 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span sslice7 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice8 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
   let%span sseq9 = "../../../creusot-contracts/src/logic/seq.rs" 173 8 173 39
@@ -125,7 +125,7 @@ module M_take_first_mut__take_first_mut [#"take_first_mut.rs" 14 0 14 74]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 =
-    [%#sops6] Seq.get (view'0 self) ix
+    [%#sindex6] Seq.get (view'0 self) ix
   
   use seq.Seq
   
diff --git a/creusot/tests/should_succeed/trigger2.coma b/creusot/tests/should_succeed/trigger2.coma
index f3c499ccef..ed8568eccb 100644
--- a/creusot/tests/should_succeed/trigger2.coma
+++ b/creusot/tests/should_succeed/trigger2.coma
@@ -3,7 +3,7 @@ module M_trigger2__resolve_seq [#"trigger2.rs" 6 0 6 43]
   let%span svec1 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span strigger22 = "trigger2.rs" 8 8 9 32
   let%span svec3 = "../../../creusot-contracts/src/std/vec.rs" 49 20 49 83
-  let%span sops4 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex4 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span sresolve5 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   
   use prelude.prelude.Borrow
@@ -46,7 +46,7 @@ module M_trigger2__resolve_seq [#"trigger2.rs" 6 0 6 43]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : borrowed t_T'0 =
-    [%#sops4] Seq.get (view'0 self) ix
+    [%#sindex4] Seq.get (view'0 self) ix
   
   predicate resolve'3 (self : borrowed t_T'0) =
     [%#sresolve5] self.final = self.current
@@ -75,7 +75,7 @@ module M_trigger2__resolve_seq2 [#"trigger2.rs" 16 0 16 48]
   let%span strigger23 = "trigger2.rs" 8 8 9 32
   let%span svec4 = "../../../creusot-contracts/src/std/vec.rs" 49 20 49 83
   let%span svec5 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops6 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex6 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span sresolve7 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   
   use prelude.prelude.Borrow
@@ -118,7 +118,7 @@ module M_trigger2__resolve_seq2 [#"trigger2.rs" 16 0 16 48]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : borrowed t_T'0 =
-    [%#sops6] Seq.get (view'0 self) ix
+    [%#sindex6] Seq.get (view'0 self) ix
   
   predicate resolve'3 (self : borrowed t_T'0) =
     [%#sresolve7] self.final = self.current
diff --git a/creusot/tests/should_succeed/type_invariants/vec_inv.coma b/creusot/tests/should_succeed/type_invariants/vec_inv.coma
index ef02df19aa..6f47f35f8e 100644
--- a/creusot/tests/should_succeed/type_invariants/vec_inv.coma
+++ b/creusot/tests/should_succeed/type_invariants/vec_inv.coma
@@ -2,7 +2,7 @@ module M_vec_inv__vec [#"vec_inv.rs" 18 0 18 32]
   let%span svec_inv0 = "vec_inv.rs" 19 20 19 43
   let%span svec_inv1 = "vec_inv.rs" 18 11 18 12
   let%span svec_inv2 = "vec_inv.rs" 17 11 17 23
-  let%span sops3 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex3 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span svec4 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span svec5 = "../../../../creusot-contracts/src/std/vec.rs" 49 20 49 83
   let%span svec6 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
@@ -98,7 +98,7 @@ module M_vec_inv__vec [#"vec_inv.rs" 18 0 18 32]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : borrowed (t_SumTo10'0) =
-    [%#sops3] Seq.get (view'0 self) ix
+    [%#sindex3] Seq.get (view'0 self) ix
   
   predicate resolve'3 (self : borrowed (t_SumTo10'0)) =
     [%#sresolve7] self.final = self.current
diff --git a/creusot/tests/should_succeed/vector/01.coma b/creusot/tests/should_succeed/vector/01.coma
index 3a23ed529a..9eebbb7ee6 100644
--- a/creusot/tests/should_succeed/vector/01.coma
+++ b/creusot/tests/should_succeed/vector/01.coma
@@ -12,7 +12,7 @@ module M_01__all_zero [#"01.rs" 7 0 7 33]
   let%span s0110 = "01.rs" 6 10 6 33
   let%span svec11 = "../../../../creusot-contracts/src/std/vec.rs" 83 26 83 48
   let%span siter12 = "../../../../creusot-contracts/src/std/iter.rs" 101 0 213 1
-  let%span sops13 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex13 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span smodel14 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22
   let%span ssnapshot15 = "../../../../creusot-contracts/src/snapshot.rs" 52 20 52 39
   let%span srange16 = "../../../../creusot-contracts/src/std/iter/range.rs" 23 12 27 70
@@ -124,7 +124,7 @@ module M_01__all_zero [#"01.rs" 7 0 7 33]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : uint32 =
-    [%#sops13] Seq.get (view'2 self) ix
+    [%#sindex13] Seq.get (view'2 self) ix
   
   function view'0 (self : borrowed (t_Vec'0)) : Seq.seq uint32 =
     [%#smodel14] view'2 self.current
diff --git a/creusot/tests/should_succeed/vector/02_gnome.coma b/creusot/tests/should_succeed/vector/02_gnome.coma
index d8db6e3755..652efa0377 100644
--- a/creusot/tests/should_succeed/vector/02_gnome.coma
+++ b/creusot/tests/should_succeed/vector/02_gnome.coma
@@ -36,7 +36,7 @@ module M_02_gnome__gnome_sort [#"02_gnome.rs" 22 0 24 29]
   let%span sslice34 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice35 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
   let%span sresolve36 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
-  let%span sops37 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex37 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span sord38 = "../../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64
   let%span sord39 = "../../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61
   let%span sord40 = "../../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61
@@ -125,7 +125,7 @@ module M_02_gnome__gnome_sort [#"02_gnome.rs" 22 0 24 29]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 =
-    [%#sops37] Seq.get (view'2 self) ix
+    [%#sindex37] Seq.get (view'2 self) ix
   
   function deep_model'3 (self : t_T'0) : t_DeepModelTy'0
   
diff --git a/creusot/tests/should_succeed/vector/04_binary_search.coma b/creusot/tests/should_succeed/vector/04_binary_search.coma
index e75193723f..cc94e53e51 100644
--- a/creusot/tests/should_succeed/vector/04_binary_search.coma
+++ b/creusot/tests/should_succeed/vector/04_binary_search.coma
@@ -16,7 +16,7 @@ module M_04_binary_search__binary_search [#"04_binary_search.rs" 26 0 26 71]
   let%span s04_binary_search14 = "04_binary_search.rs" 24 10 25 63
   let%span svec15 = "../../../../creusot-contracts/src/std/vec.rs" 83 26 83 48
   let%span smodel16 = "../../../../creusot-contracts/src/model.rs" 88 8 88 22
-  let%span sops17 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex17 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span svec18 = "../../../../creusot-contracts/src/std/vec.rs" 162 27 162 46
   let%span svec19 = "../../../../creusot-contracts/src/std/vec.rs" 163 26 163 54
   let%span s04_binary_search20 = "04_binary_search.rs" 16 4 16 31
@@ -81,7 +81,7 @@ module M_04_binary_search__binary_search [#"04_binary_search.rs" 26 0 26 71]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : uint32 =
-    [%#sops17] Seq.get (view'1 self) ix
+    [%#sindex17] Seq.get (view'1 self) ix
   
   predicate inv'1 (_1 : usize)
   
diff --git a/creusot/tests/should_succeed/vector/05_binary_search_generic.coma b/creusot/tests/should_succeed/vector/05_binary_search_generic.coma
index 9314146598..ded10f9d31 100644
--- a/creusot/tests/should_succeed/vector/05_binary_search_generic.coma
+++ b/creusot/tests/should_succeed/vector/05_binary_search_generic.coma
@@ -43,7 +43,7 @@ module M_05_binary_search_generic__binary_search [#"05_binary_search_generic.rs"
   let%span sslice41 = "../../../../creusot-contracts/src/std/slice.rs" 122 20 122 37
   let%span sslice42 = "../../../../creusot-contracts/src/std/slice.rs" 129 20 129 37
   let%span s05_binary_search_generic43 = "05_binary_search_generic.rs" 11 8 11 75
-  let%span sops44 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex44 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span sinvariant45 = "../../../../creusot-contracts/src/invariant.rs" 24 8 24 18
   let%span svec46 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sseq47 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
@@ -145,7 +145,7 @@ module M_05_binary_search_generic__binary_search [#"05_binary_search_generic.rs"
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 =
-    [%#sops44] Seq.get (view'1 self) ix
+    [%#sindex44] Seq.get (view'1 self) ix
   
   function deep_model'2 (self : t_Vec'0) : Seq.seq t_DeepModelTy'0
   
diff --git a/creusot/tests/should_succeed/vector/06_knights_tour.coma b/creusot/tests/should_succeed/vector/06_knights_tour.coma
index 0eef369f77..23cac5463c 100644
--- a/creusot/tests/should_succeed/vector/06_knights_tour.coma
+++ b/creusot/tests/should_succeed/vector/06_knights_tour.coma
@@ -124,7 +124,7 @@ module M_06_knights_tour__qyi4580598960913230815__new [#"06_knights_tour.rs" 40
   let%span smap_inv29 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 15 8 18 9
   let%span smap_inv30 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 41 8 54 9
   let%span svec31 = "../../../../creusot-contracts/src/std/vec.rs" 285 20 285 32
-  let%span sops32 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex32 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span sresolve33 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   let%span sops34 = "../../../../creusot-contracts/src/std/ops.rs" 109 15 109 59
   let%span sops35 = "../../../../creusot-contracts/src/std/ops.rs" 110 14 110 36
@@ -205,7 +205,7 @@ module M_06_knights_tour__qyi4580598960913230815__new [#"06_knights_tour.rs" 40
   use seq.Seq
   
   function index_logic'1 [@inline:trivial] (self : t_Vec'1) (ix : int) : usize =
-    [%#sops32] Seq.get (view'0 self) ix
+    [%#sindex32] Seq.get (view'0 self) ix
   
   let rec from_elem'0 (elem:usize) (n:usize) (return'  (ret:t_Vec'1))= {[@expl:from_elem 'elem' type invariant] inv'2 elem}
     any
@@ -521,7 +521,7 @@ module M_06_knights_tour__qyi4580598960913230815__new [#"06_knights_tour.rs" 40
     { t_Board__size'0: usize; t_Board__field'0: t_Vec'0 }
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_Vec'1 =
-    [%#sops32] Seq.get (view'1 self) ix
+    [%#sindex32] Seq.get (view'1 self) ix
   
   predicate wf'0 [#"06_knights_tour.rs" 30 4 30 23] (self : t_Board'0) =
     [%#s06_knights_tour14] UIntSize.to_int self.t_Board__size'0 <= 1000
@@ -572,7 +572,7 @@ module M_06_knights_tour__qyi4580598960913230815__available [#"06_knights_tour.r
   let%span sslice11 = "../../../../creusot-contracts/src/std/slice.rs" 122 20 122 37
   let%span sslice12 = "../../../../creusot-contracts/src/std/slice.rs" 129 20 129 37
   let%span svec13 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops14 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex14 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   
   use prelude.prelude.IntSize
   
@@ -694,7 +694,7 @@ module M_06_knights_tour__qyi4580598960913230815__available [#"06_knights_tour.r
   use prelude.prelude.Intrinsic
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'1) (ix : int) : t_Vec'0 =
-    [%#sops14] Seq.get (view'2 self) ix
+    [%#sindex14] Seq.get (view'2 self) ix
   
   predicate wf'0 [#"06_knights_tour.rs" 30 4 30 23] (self : t_Board'0) =
     [%#s06_knights_tour8] UIntSize.to_int self.t_Board__size'0 <= 1000
@@ -797,7 +797,7 @@ module M_06_knights_tour__qyi4580598960913230815__count_degree [#"06_knights_tou
   let%span s06_knights_tour23 = "06_knights_tour.rs" 32 12 34 93
   let%span s06_knights_tour24 = "06_knights_tour.rs" 63 12 63 75
   let%span svec25 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops26 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex26 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span svec27 = "../../../../creusot-contracts/src/std/vec.rs" 191 20 191 24
   let%span svec28 = "../../../../creusot-contracts/src/std/vec.rs" 197 20 197 33
   let%span svec29 = "../../../../creusot-contracts/src/std/vec.rs" 270 14 270 45
@@ -848,7 +848,7 @@ module M_06_knights_tour__qyi4580598960913230815__count_degree [#"06_knights_tou
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : (isize, isize) =
-    [%#sops26] Seq.get (view'0 self) ix
+    [%#sindex26] Seq.get (view'0 self) ix
   
   use prelude.prelude.IntSize
   
@@ -1032,7 +1032,7 @@ module M_06_knights_tour__qyi4580598960913230815__count_degree [#"06_knights_tou
   use seq.Seq
   
   function index_logic'1 [@inline:trivial] (self : t_Vec'1) (ix : int) : t_Vec'2 =
-    [%#sops26] Seq.get (view'2 self) ix
+    [%#sindex26] Seq.get (view'2 self) ix
   
   use seq.Seq
   
@@ -1167,7 +1167,7 @@ module M_06_knights_tour__qyi4580598960913230815__set [#"06_knights_tour.rs" 87
   let%span svec14 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span sslice15 = "../../../../creusot-contracts/src/std/slice.rs" 136 20 136 94
   let%span sresolve16 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
-  let%span sops17 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex17 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   
   use prelude.prelude.Borrow
   
@@ -1323,7 +1323,7 @@ module M_06_knights_tour__qyi4580598960913230815__set [#"06_knights_tour.rs" 87
   use prelude.prelude.Intrinsic
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_Vec'1 =
-    [%#sops17] Seq.get (view'1 self) ix
+    [%#sindex17] Seq.get (view'1 self) ix
   
   predicate wf'0 [#"06_knights_tour.rs" 30 4 30 23] (self : t_Board'0) =
     [%#s06_knights_tour9] UIntSize.to_int self.t_Board__size'0 <= 1000
@@ -1393,7 +1393,7 @@ module M_06_knights_tour__min [#"06_knights_tour.rs" 110 0 110 58]
   let%span s06_knights_tour5 = "06_knights_tour.rs" 108 10 109 60
   let%span siter6 = "../../../../creusot-contracts/src/std/iter.rs" 101 0 213 1
   let%span smodel7 = "../../../../creusot-contracts/src/model.rs" 88 8 88 22
-  let%span sops8 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex8 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span sslice9 = "../../../../creusot-contracts/src/std/slice.rs" 405 12 405 66
   let%span siter10 = "../../../../creusot-contracts/src/std/iter.rs" 107 26 110 17
   let%span svec11 = "../../../../creusot-contracts/src/std/vec.rs" 205 20 205 24
@@ -1409,7 +1409,7 @@ module M_06_knights_tour__min [#"06_knights_tour.rs" 110 0 110 58]
   let%span sslice21 = "../../../../creusot-contracts/src/std/slice.rs" 97 14 97 80
   let%span sslice22 = "../../../../creusot-contracts/src/std/slice.rs" 398 20 398 61
   let%span sresolve23 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
-  let%span sops24 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31
+  let%span sindex24 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span smodel25 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22
   let%span sslice26 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41
   let%span sslice27 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
@@ -1504,7 +1504,7 @@ module M_06_knights_tour__min [#"06_knights_tour.rs" 110 0 110 58]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : (usize, t_Point'0) =
-    [%#sops8] Seq.get (view'1 self) ix
+    [%#sindex8] Seq.get (view'1 self) ix
   
   use prelude.prelude.Snapshot
   
@@ -1517,7 +1517,7 @@ module M_06_knights_tour__min [#"06_knights_tour.rs" 110 0 110 58]
   use seq.Seq
   
   function index_logic'1 [@inline:trivial] (self : slice (usize, t_Point'0)) (ix : int) : (usize, t_Point'0) =
-    [%#sops24] Seq.get (view'5 self) ix
+    [%#sindex24] Seq.get (view'5 self) ix
   
   function to_ref_seq'0 (self : slice (usize, t_Point'0)) : Seq.seq (usize, t_Point'0)
   
@@ -1740,7 +1740,7 @@ module M_06_knights_tour__knights_tour [#"06_knights_tour.rs" 135 0 135 69]
   let%span s06_knights_tour37 = "06_knights_tour.rs" 93 10 93 28
   let%span s06_knights_tour38 = "06_knights_tour.rs" 94 10 94 128
   let%span svec39 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops40 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex40 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span svec41 = "../../../../creusot-contracts/src/std/vec.rs" 264 12 264 41
   let%span s06_knights_tour42 = "06_knights_tour.rs" 12 15 12 52
   let%span s06_knights_tour43 = "06_knights_tour.rs" 13 15 13 52
@@ -1830,7 +1830,7 @@ module M_06_knights_tour__knights_tour [#"06_knights_tour.rs" 135 0 135 69]
   use seq.Seq
   
   function index_logic'1 [@inline:trivial] (self : t_Vec'2) (ix : int) : t_Vec'3 =
-    [%#sops40] Seq.get (view'1 self) ix
+    [%#sindex40] Seq.get (view'1 self) ix
   
   use seq.Seq
   
@@ -2036,7 +2036,7 @@ module M_06_knights_tour__knights_tour [#"06_knights_tour.rs" 135 0 135 69]
   use seq.Seq
   
   function index_logic'2 [@inline:trivial] (self : t_Vec'1) (ix : int) : (isize, isize) =
-    [%#sops40] Seq.get (view'3 self) ix
+    [%#sindex40] Seq.get (view'3 self) ix
   
   let rec moves'0 (_1:()) (return'  (ret:t_Vec'1))= any
     [ return' (result:t_Vec'1)-> {[%#s06_knights_tour37] Seq.length (view'3 result) = 8}
@@ -2090,7 +2090,7 @@ module M_06_knights_tour__knights_tour [#"06_knights_tour.rs" 135 0 135 69]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : (usize, t_Point'0) =
-    [%#sops40] Seq.get (view'0 self) ix
+    [%#sindex40] Seq.get (view'0 self) ix
   
   use prelude.prelude.Snapshot
   
diff --git a/creusot/tests/should_succeed/vector/08_haystack.coma b/creusot/tests/should_succeed/vector/08_haystack.coma
index ee95b672bf..35eb99cc29 100644
--- a/creusot/tests/should_succeed/vector/08_haystack.coma
+++ b/creusot/tests/should_succeed/vector/08_haystack.coma
@@ -32,7 +32,7 @@ module M_08_haystack__search [#"08_haystack.rs" 21 0 21 60]
   let%span siter30 = "../../../../creusot-contracts/src/std/iter.rs" 86 20 86 24
   let%span siter31 = "../../../../creusot-contracts/src/std/iter.rs" 92 8 92 19
   let%span svec32 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sops33 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex33 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span srange34 = "../../../../creusot-contracts/src/std/iter/range.rs" 81 14 81 45
   let%span srange35 = "../../../../creusot-contracts/src/std/iter/range.rs" 79 4 79 10
   let%span srange36 = "../../../../creusot-contracts/src/std/iter/range.rs" 86 15 86 32
@@ -166,7 +166,7 @@ module M_08_haystack__search [#"08_haystack.rs" 21 0 21 60]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : uint8 =
-    [%#sops33] Seq.get (view'1 self) ix
+    [%#sindex33] Seq.get (view'1 self) ix
   
   predicate match_at'0 [#"08_haystack.rs" 7 0 7 77] (needle : t_Vec'0) (haystack : t_Vec'0) (pos : int) (len : int) =
     [%#s08_haystack22] len <= Seq.length (view'0 needle)
diff --git a/creusot/tests/should_succeed/vector/09_capacity.coma b/creusot/tests/should_succeed/vector/09_capacity.coma
index 8e64155fb1..280ba8d6c1 100644
--- a/creusot/tests/should_succeed/vector/09_capacity.coma
+++ b/creusot/tests/should_succeed/vector/09_capacity.coma
@@ -11,7 +11,7 @@ module M_09_capacity__change_capacity [#"09_capacity.rs" 6 0 6 41]
   let%span svec9 = "../../../../creusot-contracts/src/std/vec.rs" 130 26 130 43
   let%span svec10 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span smodel11 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22
-  let%span sops12 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31
+  let%span sindex12 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span sresolve13 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   let%span svec14 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sinvariant15 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
@@ -113,7 +113,7 @@ module M_09_capacity__change_capacity [#"09_capacity.rs" 6 0 6 41]
   use seq.Seq
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 =
-    [%#sops12] Seq.get (view'0 self) ix
+    [%#sindex12] Seq.get (view'0 self) ix
   
   meta "compute_max_steps" 1000000