diff --git a/creusot-contracts/src/logic/fmap.rs b/creusot-contracts/src/logic/fmap.rs
index d66e12ed1..f93d5aa53 100644
--- a/creusot-contracts/src/logic/fmap.rs
+++ b/creusot-contracts/src/logic/fmap.rs
@@ -430,3 +430,25 @@ impl<K, V: ?Sized> FMap<K, V> {
         panic!()
     }
 }
+
+impl<K: Clone + Copy, V: Clone + Copy> Clone for FMap<K, V> {
+    #[pure]
+    #[ensures(result == *self)]
+    #[trusted]
+    fn clone(&self) -> Self {
+        *self
+    }
+}
+
+// Having `Copy` guarantees that the operation is pure, even if we decide to change the definition of `Clone`.
+impl<K: Clone + Copy, V: Clone + Copy> Copy for FMap<K, V> {}
+
+impl<K, V: ?Sized> Invariant for FMap<K, V> {
+    #[predicate(prophetic)]
+    #[open]
+    #[creusot::trusted_ignore_structural_inv]
+    #[creusot::trusted_is_tyinv_trivial_if_param_trivial]
+    fn invariant(self) -> bool {
+        pearlite! { forall<k: K> self.contains(k) ==> inv(k) && inv(self.lookup_unsized(k)) }
+    }
+}
diff --git a/creusot-contracts/src/logic/fset.rs b/creusot-contracts/src/logic/fset.rs
index 3ad96d2b4..9ebd35b76 100644
--- a/creusot-contracts/src/logic/fset.rs
+++ b/creusot-contracts/src/logic/fset.rs
@@ -304,3 +304,25 @@ impl<T: ?Sized> FSet<T> {
         panic!()
     }
 }
+
+impl<T: Clone + Copy> Clone for FSet<T> {
+    #[pure]
+    #[ensures(result == *self)]
+    #[trusted]
+    fn clone(&self) -> Self {
+        *self
+    }
+}
+
+// Having `Copy` guarantees that the operation is pure, even if we decide to change the definition of `Clone`.
+impl<T: Clone + Copy> Copy for FSet<T> {}
+
+impl<T: ?Sized> Invariant for FSet<T> {
+    #[predicate(prophetic)]
+    #[open]
+    #[creusot::trusted_ignore_structural_inv]
+    #[creusot::trusted_is_tyinv_trivial_if_param_trivial]
+    fn invariant(self) -> bool {
+        pearlite! { forall<x: &T> self.contains(*x) ==> inv(*x) }
+    }
+}
diff --git a/creusot-contracts/src/logic/seq.rs b/creusot-contracts/src/logic/seq.rs
index 89cd2c57a..d28a4a84b 100644
--- a/creusot-contracts/src/logic/seq.rs
+++ b/creusot-contracts/src/logic/seq.rs
@@ -602,6 +602,18 @@ impl<T> Seq<T> {
     }
 }
 
+// Having `Copy` guarantees that the operation is pure, even if we decide to change the definition of `Clone`.
+impl<T: Clone + Copy> Clone for Seq<T> {
+    #[pure]
+    #[ensures(result == *self)]
+    #[trusted]
+    fn clone(&self) -> Self {
+        *self
+    }
+}
+
+impl<T: Clone + Copy> Copy for Seq<T> {}
+
 impl<T: ?Sized> Invariant for Seq<T> {
     #[predicate(prophetic)]
     #[open]
diff --git a/creusot/tests/creusot-contracts/creusot-contracts.coma b/creusot/tests/creusot-contracts/creusot-contracts.coma
index 342dc19e7..61c652f2d 100644
--- a/creusot/tests/creusot-contracts/creusot-contracts.coma
+++ b/creusot/tests/creusot-contracts/creusot-contracts.coma
@@ -8778,58 +8778,32 @@ module M_creusot_contracts__logic__fmap__qyi9892930999379617882__ext_eq [#"../..
   && ([%#sfmap1] (forall k : t_K'0 . get_unsized'0 self k = get_unsized'0 other k)  -> result))
 end
 module M_creusot_contracts__logic__fmap__qyi9892930999379617882__contains_ghost [#"../../../creusot-contracts/src/logic/fmap.rs" 285 4 285 49] (* logic::fmap::FMap<K, V> *)
-  let%span sfmap0 = "../../../creusot-contracts/src/logic/fmap.rs" 285 33 285 36
-  let%span sfmap1 = "../../../creusot-contracts/src/logic/fmap.rs" 284 14 284 43
-  let%span sfmap2 = "../../../creusot-contracts/src/logic/fmap.rs" 314 28 314 31
-  let%span sfmap3 = "../../../creusot-contracts/src/logic/fmap.rs" 314 40 314 50
-  let%span sfmap4 = "../../../creusot-contracts/src/logic/fmap.rs" 306 4 313 11
-  let%span soption5 = "../../../creusot-contracts/src/std/option.rs" 36 26 36 51
-  let%span sfmap6 = "../../../creusot-contracts/src/logic/fmap.rs" 132 8 132 35
-  let%span sfmap7 = "../../../creusot-contracts/src/logic/fmap.rs" 124 8 124 35
-  let%span sfmap8 = "../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26
-  let%span sutil9 = "../../../creusot-contracts/src/util.rs" 43 11 43 21
-  let%span sutil10 = "../../../creusot-contracts/src/util.rs" 44 10 44 28
-  let%span sinvariant11 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
-  let%span sfmap12 = "../../../creusot-contracts/src/logic/fmap.rs" 58 14 58 86
+  let%span sfmap0 = "../../../creusot-contracts/src/logic/fmap.rs" 285 27 285 31
+  let%span sfmap1 = "../../../creusot-contracts/src/logic/fmap.rs" 285 33 285 36
+  let%span sfmap2 = "../../../creusot-contracts/src/logic/fmap.rs" 284 14 284 43
+  let%span sfmap3 = "../../../creusot-contracts/src/logic/fmap.rs" 314 22 314 26
+  let%span sfmap4 = "../../../creusot-contracts/src/logic/fmap.rs" 314 28 314 31
+  let%span sfmap5 = "../../../creusot-contracts/src/logic/fmap.rs" 314 40 314 50
+  let%span sfmap6 = "../../../creusot-contracts/src/logic/fmap.rs" 306 4 313 11
+  let%span soption7 = "../../../creusot-contracts/src/std/option.rs" 36 26 36 51
+  let%span sfmap8 = "../../../creusot-contracts/src/logic/fmap.rs" 132 8 132 35
+  let%span sfmap9 = "../../../creusot-contracts/src/logic/fmap.rs" 124 8 124 35
+  let%span sfmap10 = "../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26
+  let%span sutil11 = "../../../creusot-contracts/src/util.rs" 43 11 43 21
+  let%span sutil12 = "../../../creusot-contracts/src/util.rs" 44 10 44 28
+  let%span sinvariant13 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
+  let%span sfmap14 = "../../../creusot-contracts/src/logic/fmap.rs" 58 14 58 86
+  let%span sfmap15 = "../../../creusot-contracts/src/logic/fmap.rs" 452 20 452 91
+  let%span sboxed16 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
   
-  type t_K'0
-  
-  predicate inv'4 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_K'0)
-  
-  predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_K'0) =
-    [%#sinvariant11] inv'4 self
-  
-  predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_K'0)
+  type t_FMap'0
   
-  axiom inv_axiom'0 [@rewrite] : forall x : t_K'0 [inv'0 x] . inv'0 x = invariant'0 x
+  type t_K'0
   
   type t_V'0
   
-  type t_Option'0  =
-    | C_None'0
-    | C_Some'0 t_V'0
-  
-  predicate inv'5 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_V'0)
-  
-  predicate invariant'2 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_V'0) =
-    [%#sinvariant11] inv'5 self
-  
-  predicate inv'3 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_V'0)
-  
-  axiom inv_axiom'3 [@rewrite] : forall x : t_V'0 [inv'3 x] . inv'3 x = invariant'2 x
-  
-  predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Option'0)
-  
-  axiom inv_axiom'1 [@rewrite] : forall x : t_Option'0 [inv'1 x] . inv'1 x
-  = match x with
-    | C_None'0 -> true
-    | C_Some'0 a_0 -> inv'3 a_0
-    end
-  
-  type t_FMap'0
-  
   type t_Option'1  =
     | C_None'1
     | C_Some'1 t_V'0
@@ -8839,7 +8813,7 @@ module M_creusot_contracts__logic__fmap__qyi9892930999379617882__contains_ghost
   function view'0 [#"../../../creusot-contracts/src/logic/fmap.rs" 59 4 59 35] (self : t_FMap'0) : Map.map t_K'0 (t_Option'1)
     
   
-  axiom view'0_spec : forall self : t_FMap'0 . [%#sfmap12] forall m1 : t_FMap'0, m2 : t_FMap'0 . m1 <> m2
+  axiom view'0_spec : forall self : t_FMap'0 . [%#sfmap14] forall m1 : t_FMap'0, m2 : t_FMap'0 . m1 <> m2
    -> view'0 m1 <> view'0 m2
   
   use map.Map
@@ -8847,27 +8821,79 @@ module M_creusot_contracts__logic__fmap__qyi9892930999379617882__contains_ghost
   function get_unsized'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/fmap.rs" 102 4 102 55] (self : t_FMap'0) (k : t_K'0) : t_Option'1
     
    =
-    [%#sfmap8] Map.get (view'0 self) k
+    [%#sfmap10] Map.get (view'0 self) k
   
   function contains'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/fmap.rs" 131 4 131 39] (self : t_FMap'0) (k : t_K'0) : bool
     
    =
-    [%#sfmap6] get_unsized'0 self k <> C_None'1
+    [%#sfmap8] get_unsized'0 self k <> C_None'1
+  
+  predicate inv'6 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_K'0)
   
   function unwrap'0 [#"../../../creusot-contracts/src/util.rs" 45 0 45 36] (op : t_Option'1) : t_V'0
   
-  axiom unwrap'0_spec : forall op : t_Option'1 . ([%#sutil9] op <> C_None'1)
-   -> ([%#sutil10] C_Some'1 (unwrap'0 op) = op)
+  axiom unwrap'0_spec : forall op : t_Option'1 . ([%#sutil11] op <> C_None'1)
+   -> ([%#sutil12] C_Some'1 (unwrap'0 op) = op)
   
   function lookup_unsized'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/fmap.rs" 123 4 123 50] (self : t_FMap'0) (k : t_K'0) : t_V'0
     
    =
-    [%#sfmap7] unwrap'0 (get_unsized'0 self k)
+    [%#sfmap9] unwrap'0 (get_unsized'0 self k)
+  
+  predicate inv'7 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_V'0)
+  
+  predicate invariant'5 [#"../../../creusot-contracts/src/std/boxed.rs" 27 4 27 30] (self : t_V'0) =
+    [%#sboxed16] inv'7 self
+  
+  predicate inv'8 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_V'0)
+  
+  axiom inv_axiom'6 [@rewrite] : forall x : t_V'0 [inv'8 x] . inv'8 x = invariant'5 x
   
-  let rec get_ghost'0 (self:t_FMap'0) (key:t_K'0) (return'  (ret:t_Option'0))= {[@expl:get_ghost 'key' type invariant] [%#sfmap2] inv'0 key}
+  predicate invariant'4 [#"../../../creusot-contracts/src/logic/fmap.rs" 451 4 451 30] (self : t_FMap'0) =
+    [%#sfmap15] forall k : t_K'0 . contains'0 self k  -> inv'6 k /\ inv'8 (lookup_unsized'0 self k)
+  
+  predicate inv'5 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_FMap'0)
+  
+  axiom inv_axiom'5 [@rewrite] : forall x : t_FMap'0 [inv'5 x] . inv'5 x = invariant'4 x
+  
+  predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_FMap'0) =
+    [%#sinvariant13] inv'5 self
+  
+  predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_FMap'0)
+  
+  axiom inv_axiom'0 [@rewrite] : forall x : t_FMap'0 [inv'0 x] . inv'0 x = invariant'0 x
+  
+  predicate invariant'1 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_K'0) =
+    [%#sinvariant13] inv'6 self
+  
+  predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_K'0)
+  
+  axiom inv_axiom'1 [@rewrite] : forall x : t_K'0 [inv'1 x] . inv'1 x = invariant'1 x
+  
+  type t_Option'0  =
+    | C_None'0
+    | C_Some'0 t_V'0
+  
+  predicate invariant'3 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_V'0) =
+    [%#sinvariant13] inv'7 self
+  
+  predicate inv'4 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_V'0)
+  
+  axiom inv_axiom'4 [@rewrite] : forall x : t_V'0 [inv'4 x] . inv'4 x = invariant'3 x
+  
+  predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Option'0)
+  
+  axiom inv_axiom'2 [@rewrite] : forall x : t_Option'0 [inv'2 x] . inv'2 x
+  = match x with
+    | C_None'0 -> true
+    | C_Some'0 a_0 -> inv'4 a_0
+    end
+  
+  let rec get_ghost'0 (self:t_FMap'0) (key:t_K'0) (return'  (ret:t_Option'0))= {[@expl:get_ghost 'self' type invariant] [%#sfmap3] inv'0 self}
+    {[@expl:get_ghost 'key' type invariant] [%#sfmap4] inv'1 key}
     any
-    [ return' (result:t_Option'0)-> {[%#sfmap3] inv'1 result}
-      {[%#sfmap4] if contains'0 self key then
+    [ return' (result:t_Option'0)-> {[%#sfmap5] inv'2 result}
+      {[%#sfmap6] if contains'0 self key then
         match result with
           | C_None'0 -> false
           | C_Some'0 r -> lookup_unsized'0 self key = r
@@ -8878,27 +8904,28 @@ module M_creusot_contracts__logic__fmap__qyi9892930999379617882__contains_ghost
       (! return' {result}) ]
     
   
-  predicate invariant'1 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Option'0) =
-    [%#sinvariant11] inv'1 self
+  predicate invariant'2 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_Option'0) =
+    [%#sinvariant13] inv'2 self
   
-  predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Option'0)
+  predicate inv'3 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_Option'0)
   
-  axiom inv_axiom'2 [@rewrite] : forall x : t_Option'0 [inv'2 x] . inv'2 x = invariant'1 x
+  axiom inv_axiom'3 [@rewrite] : forall x : t_Option'0 [inv'3 x] . inv'3 x = invariant'2 x
   
-  let rec is_some'0 (self:t_Option'0) (return'  (ret:bool))= {[@expl:is_some 'self' type invariant] inv'2 self}
-    any [ return' (result:bool)-> {[%#soption5] result = (self <> C_None'0)} (! return' {result}) ] 
+  let rec is_some'0 (self:t_Option'0) (return'  (ret:bool))= {[@expl:is_some 'self' type invariant] inv'3 self}
+    any [ return' (result:bool)-> {[%#soption7] result = (self <> C_None'0)} (! return' {result}) ] 
   
   use prelude.prelude.Intrinsic
   
   meta "compute_max_steps" 1000000
   
-  let rec contains_ghost'0 (self:t_FMap'0) (key:t_K'0) (return'  (ret:bool))= {[@expl:contains_ghost 'key' type invariant] [%#sfmap0] inv'0 key}
+  let rec contains_ghost'0 (self:t_FMap'0) (key:t_K'0) (return'  (ret:bool))= {[@expl:contains_ghost 'self' type invariant] [%#sfmap0] inv'0 self}
+    {[@expl:contains_ghost 'key' type invariant] [%#sfmap1] inv'1 key}
     (! bb0
     [ bb0 = s0 [ s0 = get_ghost'0 {self} {key} (fun (_ret':t_Option'0) ->  [ &_5 <- _ret' ] s1) | s1 = bb1 ] 
     | bb1 = s0 [ s0 = is_some'0 {_5} (fun (_ret':bool) ->  [ &_0 <- _ret' ] s1) | s1 = bb2 ] 
     | bb2 = return' {_0} ]
     ) [ & _0 : bool = any_l () | & self : t_FMap'0 = self | & key : t_K'0 = key | & _5 : t_Option'0 = any_l () ] 
-    [ return' (result:bool)-> {[@expl:contains_ghost ensures] [%#sfmap1] result = contains'0 self key}
+    [ return' (result:bool)-> {[@expl:contains_ghost ensures] [%#sfmap2] result = contains'0 self key}
       (! return' {result}) ]
     
 end
@@ -20506,7 +20533,7 @@ module M_creusot_contracts__stdqy35z1__vec__qyi6844585276173866460__resolve_cohe
   let%span sindex3 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span sinvariant4 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
   let%span svec5 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
-  let%span sseq6 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq6 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed7 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
@@ -20570,7 +20597,7 @@ module M_creusot_contracts__stdqy35z1__vec__qyi6844585276173866460__resolve_cohe
   
   axiom inv_axiom'3 [@rewrite] : forall x : t_T'0 [inv'3 x] . inv'3 x = invariant'3 x
   
-  predicate invariant'2 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_T'0) =
+  predicate invariant'2 [#"../../../creusot-contracts/src/logic/seq.rs" 622 4 622 30] (self : Seq.seq t_T'0) =
     [%#sseq6] forall i : int . 0 <= i /\ i < Seq.length self  -> inv'3 (Seq.get self i)
   
   predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_T'0)
@@ -24646,6 +24673,126 @@ module M_creusot_contracts__ghost__qyi17645547594388049322__clone__refines [#"..
   goal refines : [%#sghost0] forall self : t_GhostBox'0 . inv'0 self
    -> inv'0 self /\ (forall result : t_GhostBox'0 . result = self /\ inv'1 result  -> result = self /\ inv'1 result)
 end
+module M_creusot_contracts__logic__fmap__qyi4648834920430559677__clone__refines [#"../../../creusot-contracts/src/logic/fmap.rs" 438 4 438 27] (* <logic::fmap::FMap<K, V> as std::clone::Clone> *)
+  let%span sfmap0 = "../../../creusot-contracts/src/logic/fmap.rs" 438 4 438 27
+  let%span sinvariant1 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
+  let%span sfmap2 = "../../../creusot-contracts/src/logic/fmap.rs" 452 20 452 91
+  let%span sfmap3 = "../../../creusot-contracts/src/logic/fmap.rs" 132 8 132 35
+  let%span sfmap4 = "../../../creusot-contracts/src/logic/fmap.rs" 124 8 124 35
+  let%span sfmap5 = "../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26
+  let%span sutil6 = "../../../creusot-contracts/src/util.rs" 43 11 43 21
+  let%span sutil7 = "../../../creusot-contracts/src/util.rs" 44 10 44 28
+  let%span sfmap8 = "../../../creusot-contracts/src/logic/fmap.rs" 58 14 58 86
+  let%span sboxed9 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
+  
+  use prelude.prelude.Borrow
+  
+  type t_FMap'0
+  
+  type t_K'0
+  
+  type t_V'0
+  
+  type t_Option'0  =
+    | C_None'0
+    | C_Some'0 t_V'0
+  
+  use map.Map
+  
+  function view'0 [#"../../../creusot-contracts/src/logic/fmap.rs" 59 4 59 35] (self : t_FMap'0) : Map.map t_K'0 (t_Option'0)
+    
+  
+  axiom view'0_spec : forall self : t_FMap'0 . [%#sfmap8] forall m1 : t_FMap'0, m2 : t_FMap'0 . m1 <> m2
+   -> view'0 m1 <> view'0 m2
+  
+  use map.Map
+  
+  function get_unsized'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/fmap.rs" 102 4 102 55] (self : t_FMap'0) (k : t_K'0) : t_Option'0
+    
+   =
+    [%#sfmap5] Map.get (view'0 self) k
+  
+  function contains'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/fmap.rs" 131 4 131 39] (self : t_FMap'0) (k : t_K'0) : bool
+    
+   =
+    [%#sfmap3] get_unsized'0 self k <> C_None'0
+  
+  predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_K'0)
+  
+  function unwrap'0 [#"../../../creusot-contracts/src/util.rs" 45 0 45 36] (op : t_Option'0) : t_V'0
+  
+  axiom unwrap'0_spec : forall op : t_Option'0 . ([%#sutil6] op <> C_None'0)
+   -> ([%#sutil7] C_Some'0 (unwrap'0 op) = op)
+  
+  function lookup_unsized'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/fmap.rs" 123 4 123 50] (self : t_FMap'0) (k : t_K'0) : t_V'0
+    
+   =
+    [%#sfmap4] unwrap'0 (get_unsized'0 self k)
+  
+  predicate inv'4 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_V'0)
+  
+  predicate invariant'2 [#"../../../creusot-contracts/src/std/boxed.rs" 27 4 27 30] (self : t_V'0) =
+    [%#sboxed9] inv'4 self
+  
+  predicate inv'3 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_V'0)
+  
+  axiom inv_axiom'2 [@rewrite] : forall x : t_V'0 [inv'3 x] . inv'3 x = invariant'2 x
+  
+  predicate invariant'1 [#"../../../creusot-contracts/src/logic/fmap.rs" 451 4 451 30] (self : t_FMap'0) =
+    [%#sfmap2] forall k : t_K'0 . contains'0 self k  -> inv'2 k /\ inv'3 (lookup_unsized'0 self k)
+  
+  predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_FMap'0)
+  
+  axiom inv_axiom'1 [@rewrite] : forall x : t_FMap'0 [inv'1 x] . inv'1 x = invariant'1 x
+  
+  predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : t_FMap'0) =
+    [%#sinvariant1] inv'1 self
+  
+  predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_FMap'0)
+  
+  axiom inv_axiom'0 [@rewrite] : forall x : t_FMap'0 [inv'0 x] . inv'0 x = invariant'0 x
+  
+  goal refines : [%#sfmap0] forall self : t_FMap'0 . inv'0 self
+   -> inv'0 self /\ (forall result : t_FMap'0 . result = self /\ inv'1 result  -> result = self /\ inv'1 result)
+end
+module M_creusot_contracts__logic__fset__qyi11096226875104347554__clone__refines [#"../../../creusot-contracts/src/logic/fset.rs" 312 4 312 27] (* <logic::fset::FSet<T> as std::clone::Clone> *)
+  let%span sfset0 = "../../../creusot-contracts/src/logic/fset.rs" 312 4 312 27
+  let%span sinvariant1 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
+  let%span sfset2 = "../../../creusot-contracts/src/logic/fset.rs" 326 20 326 63
+  let%span sfset3 = "../../../creusot-contracts/src/logic/fset.rs" 46 8 46 26
+  
+  use prelude.prelude.Borrow
+  
+  type t_T'0
+  
+  use set.Fset
+  
+  use set.Fset
+  
+  predicate contains'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/fset.rs" 45 4 45 39] (self : Fset.fset t_T'0) (e : t_T'0)
+    
+   =
+    [%#sfset3] Fset.mem e self
+  
+  predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_T'0)
+  
+  predicate invariant'1 [#"../../../creusot-contracts/src/logic/fset.rs" 325 4 325 30] (self : Fset.fset t_T'0) =
+    [%#sfset2] forall x : t_T'0 . contains'0 self x  -> inv'2 x
+  
+  predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Fset.fset t_T'0)
+  
+  axiom inv_axiom'1 [@rewrite] : forall x : Fset.fset t_T'0 [inv'1 x] . inv'1 x = invariant'1 x
+  
+  predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : Fset.fset t_T'0) =
+    [%#sinvariant1] inv'1 self
+  
+  predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Fset.fset t_T'0)
+  
+  axiom inv_axiom'0 [@rewrite] : forall x : Fset.fset t_T'0 [inv'0 x] . inv'0 x = invariant'0 x
+  
+  goal refines : [%#sfset0] forall self : Fset.fset t_T'0 . inv'0 self
+   -> inv'0 self /\ (forall result : Fset.fset t_T'0 . result = self /\ inv'1 result  -> result = self /\ inv'1 result)
+end
 module M_creusot_contracts__logic__int__qyi3540547019284611154__clone__refines [#"../../../creusot-contracts/src/logic/int.rs" 37 4 37 27] (* <logic::int::Int as std::clone::Clone> *)
   let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 37 4 37 27
   
@@ -24664,6 +24811,50 @@ module M_creusot_contracts__logic__int__qyi3540547019284611154__clone__refines [
   goal refines : [%#sint0] forall self : int . inv'0 self
    -> (forall result : int . result = self  -> result = self /\ inv'1 result)
 end
+module M_creusot_contracts__logic__seq__qyi8239750555979287100__clone__refines [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 27] (* <logic::seq::Seq<T> as std::clone::Clone> *)
+  let%span sseq0 = "../../../creusot-contracts/src/logic/seq.rs" 610 4 610 27
+  let%span sinvariant1 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
+  let%span sseq2 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
+  let%span sboxed3 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
+  
+  use prelude.prelude.Borrow
+  
+  type t_T'0
+  
+  use seq.Seq
+  
+  use prelude.prelude.Int
+  
+  use seq.Seq
+  
+  use seq.Seq
+  
+  predicate inv'3 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_T'0)
+  
+  predicate invariant'2 [#"../../../creusot-contracts/src/std/boxed.rs" 27 4 27 30] (self : t_T'0) =
+    [%#sboxed3] inv'3 self
+  
+  predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_T'0)
+  
+  axiom inv_axiom'2 [@rewrite] : forall x : t_T'0 [inv'2 x] . inv'2 x = invariant'2 x
+  
+  predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 622 4 622 30] (self : Seq.seq t_T'0) =
+    [%#sseq2] forall i : int . 0 <= i /\ i < Seq.length self  -> inv'2 (Seq.get self i)
+  
+  predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_T'0)
+  
+  axiom inv_axiom'1 [@rewrite] : forall x : Seq.seq t_T'0 [inv'1 x] . inv'1 x = invariant'1 x
+  
+  predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : Seq.seq t_T'0) =
+    [%#sinvariant1] inv'1 self
+  
+  predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_T'0)
+  
+  axiom inv_axiom'0 [@rewrite] : forall x : Seq.seq t_T'0 [inv'0 x] . inv'0 x = invariant'0 x
+  
+  goal refines : [%#sseq0] forall self : Seq.seq t_T'0 . inv'0 self
+   -> inv'0 self /\ (forall result : Seq.seq t_T'0 . result = self /\ inv'1 result  -> result = self /\ inv'1 result)
+end
 module M_creusot_contracts__snapshot__qyi5567339964777190687__clone__refines [#"../../../creusot-contracts/src/snapshot.rs" 59 4 59 27] (* <snapshot::Snapshot<T> as std::clone::Clone> *)
   let%span ssnapshot0 = "../../../creusot-contracts/src/snapshot.rs" 59 4 59 27
   
diff --git a/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml b/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml
index 8ba632708..5b920d707 100644
--- a/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml
+++ b/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml
@@ -1761,12 +1761,12 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__copied__qyi4622684907952448174__resolve_coherence__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.018852" steps="2"/></proof>
+ <proof prover="3"><result status="valid" time="0.018852" steps="2"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__copied__qyi18224474876607687026__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.020719" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.020719" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__copied__qyi18224474876607687026__produces_refl" proved="true">
@@ -1776,7 +1776,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__copied__qyi18224474876607687026__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="2"><result status="valid" time="0.034597" steps="1186"/></proof>
+ <proof prover="3"><result status="valid" time="0.011306" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__copied__qyi18224474876607687026__produces_trans" proved="true">
@@ -1786,7 +1786,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__empty__qyi10605201058978801838__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.021676" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.021676" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__empty__qyi10605201058978801838__produces_refl" proved="true">
@@ -1796,26 +1796,26 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__empty__qyi10605201058978801838__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="2"><result status="valid" time="0.033459" steps="102"/></proof>
+ <proof prover="3"><result status="valid" time="0.014647" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__empty__qyi10605201058978801838__produces_trans" proved="true">
  <goal name="vc_produces_trans&#39;0" proved="true">
  <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
   <goal name="vc_produces_trans&#39;0.0" proved="true">
-  <proof prover="0"><result status="valid" time="0.022672" steps="19905"/></proof>
+  <proof prover="3"><result status="valid" time="0.010971" steps="38"/></proof>
   </goal>
  </transf>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__enumerate__qyi2208779330486735413__resolve_coherence__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="1"><result status="valid" time="0.018266" steps="506"/></proof>
+ <proof prover="3"><result status="valid" time="0.008419" steps="2"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__enumerate__qyi2718914205750388896__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.020348" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.020348" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__enumerate__qyi2718914205750388896__produces_refl" proved="true">
@@ -1825,7 +1825,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__enumerate__qyi2718914205750388896__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.020912" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.020912" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__enumerate__qyi2718914205750388896__produces_trans" proved="true">
@@ -1835,7 +1835,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__filter__qyi9573749579793237160__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.025514" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.025514" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__filter__qyi9573749579793237160__produces_refl" proved="true">
@@ -1860,7 +1860,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__filter__qyi9573749579793237160__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.023223" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.023223" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__filter__qyi9573749579793237160__produces_trans" proved="true">
@@ -1869,17 +1869,17 @@
   <goal name="vc_produces_trans&#39;0.0" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="vc_produces_trans&#39;0.0.0" proved="true">
-   <proof prover="3" timelimit="5"><result status="valid" time="0.018270" steps="28"/></proof>
+   <proof prover="3"><result status="valid" time="0.018270" steps="28"/></proof>
    </goal>
    <goal name="vc_produces_trans&#39;0.0.1" proved="true">
    <transf name="destruct_rec" proved="true" arg1="H3">
     <goal name="vc_produces_trans&#39;0.0.1.0" expl="destruct premise" proved="true">
-    <proof prover="3" timelimit="5"><result status="valid" time="0.036253" steps="8"/></proof>
+    <proof prover="3"><result status="valid" time="0.036253" steps="8"/></proof>
     </goal>
     <goal name="vc_produces_trans&#39;0.0.1.1" proved="true">
     <transf name="destruct_rec" proved="true" arg1="H1">
      <goal name="vc_produces_trans&#39;0.0.1.1.0" expl="destruct premise" proved="true">
-     <proof prover="2"><result status="valid" time="0.042374" steps="3264"/></proof>
+     <proof prover="3"><result status="valid" time="0.014631" steps="6"/></proof>
      </goal>
      <goal name="vc_produces_trans&#39;0.0.1.1.1" proved="true">
      <transf name="exists" proved="true" arg1="(s++s1)">
@@ -1888,37 +1888,37 @@
        <goal name="vc_produces_trans&#39;0.0.1.1.1.0.0" proved="true">
        <transf name="split_vc" proved="true" >
         <goal name="vc_produces_trans&#39;0.0.1.1.1.0.0.0" proved="true">
-        <proof prover="0"><result status="valid" time="0.052579" steps="24512"/></proof>
+        <proof prover="3"><result status="valid" time="0.011349" steps="11"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.1.1.0.0.1" proved="true">
-        <proof prover="2"><result status="valid" time="0.070246" steps="5786"/></proof>
+        <proof prover="3"><result status="valid" time="0.364186" steps="1950"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.1.1.0.0.2" proved="true">
-        <proof prover="2"><result status="valid" time="0.152303" steps="7619"/></proof>
+        <proof prover="3"><result status="valid" time="0.232402" steps="2445"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.1.1.0.0.3" proved="true">
-        <proof prover="0"><result status="valid" time="0.047466" steps="28034"/></proof>
+        <proof prover="3"><result status="valid" time="0.442625" steps="2591"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.1.1.0.0.4" proved="true">
-        <proof prover="1"><result status="valid" time="0.126306" steps="10144"/></proof>
+        <proof prover="2" timelimit="1"><result status="valid" time="0.057569" steps="9418"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.1.1.0.0.5" proved="true">
-        <proof prover="2"><result status="valid" time="0.173384" steps="8897"/></proof>
+        <proof prover="2" timelimit="1"><result status="valid" time="0.056024" steps="8897"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.1.1.0.0.6" proved="true">
         <transf name="case" proved="true" arg1="(i&lt;length s)">
          <goal name="vc_produces_trans&#39;0.0.1.1.1.0.0.6.0" expl="true case" proved="true">
-         <proof prover="3" timelimit="5"><result status="valid" time="0.062073" steps="112"/></proof>
+         <proof prover="3"><result status="valid" time="0.062073" steps="112"/></proof>
          </goal>
          <goal name="vc_produces_trans&#39;0.0.1.1.1.0.0.6.1" expl="false case" proved="true">
          <transf name="instantiate" proved="true" arg1="H9" arg2="(i-length s)">
           <goal name="vc_produces_trans&#39;0.0.1.1.1.0.0.6.1.0" expl="false case" proved="true">
           <transf name="replace" proved="true" arg1="(func&#39;0 b)" arg2="(func&#39;0 a)" arg3="in" arg4="Hinst">
            <goal name="vc_produces_trans&#39;0.0.1.1.1.0.0.6.1.0.0" expl="false case" proved="true">
-           <proof prover="3" timelimit="5"><result status="valid" time="0.160334" steps="482"/></proof>
+           <proof prover="3"><result status="valid" time="0.160334" steps="482"/></proof>
            </goal>
            <goal name="vc_produces_trans&#39;0.0.1.1.1.0.0.6.1.0.1" expl="equality hypothesis" proved="true">
-           <proof prover="2"><result status="valid" time="0.090160" steps="4412"/></proof>
+           <proof prover="2" timelimit="1"><result status="valid" time="0.090160" steps="4412"/></proof>
            </goal>
           </transf>
           </goal>
@@ -1943,37 +1943,37 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__ops__qyi14194840286170235833__postcondition_mut_unnest__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="1"><result status="valid" time="0.021900" steps="20"/></proof>
+ <proof prover="3"><result status="valid" time="0.018670" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__ops__qyi14194840286170235833__unnest_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.016176" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.016176" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__ops__qyi14194840286170235833__unnest_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="2"><result status="valid" time="0.021904" steps="27"/></proof>
+ <proof prover="3"><result status="valid" time="0.019200" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__ops__qyi14194840286170235833__fn_mut_once__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="1"><result status="valid" time="0.019826" steps="20"/></proof>
+ <proof prover="3"><result status="valid" time="0.017896" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__ops__qyi10441027020636586103__fn_mut__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.019464" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.019464" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__ops__qyi10441027020636586103__fn_once__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="2"><result status="valid" time="0.017081" steps="27"/></proof>
+ <proof prover="3"><result status="valid" time="0.016216" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__resolve__qyi4855891653524509355__resolve_coherence__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.019076" steps="2"/></proof>
+ <proof prover="3"><result status="valid" time="0.019076" steps="2"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__resolve__qyi4855891653524509355__resolve_coherence" proved="true">
@@ -1983,7 +1983,7 @@
 </theory>
 <theory name="M_creusot_contracts__resolve__qyi6740873903368268328__resolve_coherence__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="0"><result status="valid" time="0.023505" steps="4135"/></proof>
+ <proof prover="3"><result status="valid" time="0.022889" steps="2"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__resolve__qyi6740873903368268328__resolve_coherence" proved="true">
@@ -1993,7 +1993,7 @@
 </theory>
 <theory name="M_creusot_contracts__resolve__qyi10830812895881240411__resolve_coherence__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="1"><result status="valid" time="0.022812" steps="147"/></proof>
+ <proof prover="3"><result status="valid" time="0.017216" steps="2"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__resolve__qyi10830812895881240411__resolve_coherence" proved="true">
@@ -2003,7 +2003,7 @@
 </theory>
 <theory name="M_creusot_contracts__resolve__qyi12875730110607858017__resolve_coherence__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="0"><result status="valid" time="0.019203" steps="869"/></proof>
+ <proof prover="3"><result status="valid" time="0.014800" steps="4"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__resolve__qyi12875730110607858017__resolve_coherence" proved="true">
@@ -2013,7 +2013,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__fuse__qyi10730559947553418603__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.024500" steps="2"/></proof>
+ <proof prover="3"><result status="valid" time="0.024500" steps="2"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__fuse__qyi10730559947553418603__produces_refl" proved="true">
@@ -2023,7 +2023,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__fuse__qyi10730559947553418603__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="2"><result status="valid" time="0.028578" steps="1359"/></proof>
+ <proof prover="3"><result status="valid" time="0.016743" steps="2"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__fuse__qyi10730559947553418603__produces_trans" proved="true">
@@ -2040,10 +2040,10 @@
     <proof prover="3"><result status="valid" time="0.033521" steps="23"/></proof>
     </goal>
     <goal name="vc_produces_trans&#39;0.0.0.2" proved="true">
-    <proof prover="2" timelimit="1"><result status="valid" time="0.070752" steps="4223"/></proof>
+    <proof prover="3"><result status="valid" time="0.031056" steps="228"/></proof>
     </goal>
     <goal name="vc_produces_trans&#39;0.0.0.3" proved="true">
-    <proof prover="2" timelimit="1"><result status="valid" time="0.051050" steps="3207"/></proof>
+    <proof prover="3"><result status="valid" time="0.037782" steps="114"/></proof>
     </goal>
    </transf>
    </goal>
@@ -2054,22 +2054,22 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__fuse__qyi7691061398646472980__is_fused__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.014983" steps="2"/></proof>
+ <proof prover="3"><result status="valid" time="0.014983" steps="2"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__fuse__qyi7691061398646472980__is_fused" proved="true">
  <goal name="vc_is_fused&#39;0" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.024051" steps="23"/></proof>
+ <proof prover="3"><result status="valid" time="0.024051" steps="23"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__map__qyi13484997498660514945__resolve_coherence__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.017610" steps="2"/></proof>
+ <proof prover="3"><result status="valid" time="0.017610" steps="2"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.022410" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.022410" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produces_refl" proved="true">
@@ -2079,7 +2079,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="0"><result status="valid" time="0.020505" steps="849"/></proof>
+ <proof prover="3"><result status="valid" time="0.021756" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produces_trans" proved="true">
@@ -2088,19 +2088,19 @@
   <goal name="vc_produces_trans&#39;0.0" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="vc_produces_trans&#39;0.0.0" proved="true">
-   <proof prover="0"><result status="valid" time="0.021589" steps="37006"/></proof>
+   <proof prover="3"><result status="valid" time="0.027633" steps="41"/></proof>
    </goal>
    <goal name="vc_produces_trans&#39;0.0.1" proved="true">
    <transf name="exists" proved="true" arg1="(fs++fs1)">
     <goal name="vc_produces_trans&#39;0.0.1.0" proved="true">
     <transf name="split_vc" proved="true" >
      <goal name="vc_produces_trans&#39;0.0.1.0.0" proved="true">
-     <proof prover="0"><result status="valid" time="0.031588" steps="38896"/></proof>
+     <proof prover="3"><result status="valid" time="0.023861" steps="32"/></proof>
      </goal>
      <goal name="vc_produces_trans&#39;0.0.1.0.1" proved="true">
      <transf name="exists" proved="true" arg1="(s++s1)">
       <goal name="vc_produces_trans&#39;0.0.1.0.1.0" proved="true">
-      <proof prover="3" timelimit="5"><result status="valid" time="0.355761" steps="2012"/></proof>
+      <proof prover="3"><result status="valid" time="0.355761" steps="2012"/></proof>
       </goal>
      </transf>
      </goal>
@@ -2115,21 +2115,21 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__map_inv__qyi9026772487048432788__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="2"><result status="valid" time="0.042267" steps="1669"/></proof>
+ <proof prover="3"><result status="valid" time="0.021713" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__map_inv__qyi9026772487048432788__produces_refl" proved="true">
  <goal name="vc_produces_refl&#39;0" proved="true">
  <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
   <goal name="vc_produces_refl&#39;0.0" proved="true">
-  <proof prover="0"><result status="valid" time="0.154900" steps="66687"/></proof>
+  <proof prover="2" timelimit="1"><result status="valid" time="0.040877" steps="11651"/></proof>
   </goal>
  </transf>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__map_inv__qyi9026772487048432788__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.029388" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.029388" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__map_inv__qyi9026772487048432788__produces_trans" proved="true">
@@ -2138,14 +2138,14 @@
   <goal name="vc_produces_trans&#39;0.0" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="vc_produces_trans&#39;0.0.0" proved="true">
-   <proof prover="3" timelimit="5"><result status="valid" time="0.018330" steps="49"/></proof>
+   <proof prover="3"><result status="valid" time="0.018330" steps="49"/></proof>
    </goal>
    <goal name="vc_produces_trans&#39;0.0.1" proved="true">
    <transf name="exists" proved="true" arg1="(fs++fs1)">
     <goal name="vc_produces_trans&#39;0.0.1.0" proved="true">
     <transf name="split_vc" proved="true" >
      <goal name="vc_produces_trans&#39;0.0.1.0.0" proved="true">
-     <proof prover="3" timelimit="5"><result status="valid" time="0.019916" steps="39"/></proof>
+     <proof prover="3"><result status="valid" time="0.019916" steps="39"/></proof>
      </goal>
      <goal name="vc_produces_trans&#39;0.0.1.0.1" proved="true">
      <transf name="exists" proved="true" arg1="(s++s1)">
@@ -2154,35 +2154,35 @@
        <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0" proved="true">
        <transf name="split_vc" proved="true" >
         <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.0" proved="true">
-        <proof prover="3" timelimit="5"><result status="valid" time="0.017775" steps="45"/></proof>
+        <proof prover="3"><result status="valid" time="0.017775" steps="45"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.1" proved="true">
-        <proof prover="2"><result status="valid" time="0.100243" steps="10715"/></proof>
+        <proof prover="3"><result status="valid" time="0.017017" steps="39"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.2" proved="true">
-        <proof prover="3" timelimit="5"><result status="valid" time="0.018146" steps="250"/></proof>
+        <proof prover="3"><result status="valid" time="0.018146" steps="250"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.3" proved="true">
-        <proof prover="3" timelimit="5"><result status="valid" time="0.044450" steps="392"/></proof>
+        <proof prover="3"><result status="valid" time="0.044450" steps="392"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.4" proved="true">
-        <proof prover="0"><result status="valid" time="0.034965" steps="76192"/></proof>
+        <proof prover="3"><result status="valid" time="0.033185" steps="71"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.5" proved="true">
-        <proof prover="3" timelimit="5"><result status="valid" time="0.027243" steps="166"/></proof>
+        <proof prover="3"><result status="valid" time="0.027243" steps="166"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.6" proved="true">
-        <proof prover="3" timelimit="5"><result status="valid" time="0.021964" steps="204"/></proof>
+        <proof prover="3"><result status="valid" time="0.021964" steps="204"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.7" proved="true">
-        <proof prover="3" timelimit="5"><result status="valid" time="0.185671" steps="722"/></proof>
+        <proof prover="3"><result status="valid" time="0.185671" steps="722"/></proof>
         </goal>
         <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.8" proved="true">
         <transf name="instantiate" proved="true" arg1="H2" arg2="i">
          <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.8.0" proved="true">
          <transf name="instantiate" proved="true" arg1="H10" arg2="(i-length ab)">
           <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.8.0.0" proved="true">
-          <proof prover="3" timelimit="5"><result status="valid" time="0.705553" steps="3543"/></proof>
+          <proof prover="3"><result status="valid" time="0.295329" steps="3543"/></proof>
           </goal>
          </transf>
          </goal>
@@ -2193,7 +2193,7 @@
          <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.9.0" proved="true">
          <transf name="instantiate" proved="true" arg1="H10" arg2="(i-length ab)">
           <goal name="vc_produces_trans&#39;0.0.1.0.1.0.0.9.0.0" proved="true">
-          <proof prover="3" timelimit="5"><result status="valid" time="0.704234" steps="3575"/></proof>
+          <proof prover="3"><result status="valid" time="0.492531" steps="3575"/></proof>
           </goal>
          </transf>
          </goal>
@@ -2216,29 +2216,29 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__map_inv__qyi5691635635396426195__resolve_coherence__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.022845" steps="2"/></proof>
+ <proof prover="3"><result status="valid" time="0.022845" steps="2"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__map_inv__qyi5691635635396426195__resolve_coherence" proved="true">
  <goal name="vc_resolve_coherence&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.040191" steps="658"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.040191" steps="658"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__map_inv__qyi4413682431414748756__next__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="2"><result status="valid" time="0.175872" steps="20623"/></proof>
+ <proof prover="3"><result status="valid" time="0.120551" steps="984"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__map_inv__qyi4413682431414748756__next" proved="true">
  <goal name="vc_next&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.319669" steps="32188"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.108892" steps="32188"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__map_inv__qyi4899712594723907874__preservation_inv" proved="true">
  <goal name="vc_preservation_inv&#39;0" proved="true">
  <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
   <goal name="vc_preservation_inv&#39;0.0" proved="true">
-  <proof prover="2"><result status="valid" time="0.220252" steps="15320"/></proof>
+  <proof prover="2" timelimit="1"><result status="valid" time="0.051887" steps="15320"/></proof>
   </goal>
  </transf>
  </goal>
@@ -2251,54 +2251,54 @@
    <goal name="vc_produces_one&#39;0.0.0" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="vc_produces_one&#39;0.0.0.0" proved="true">
-    <proof prover="3" timelimit="5"><result status="valid" time="0.016697" steps="16"/></proof>
+    <proof prover="3"><result status="valid" time="0.016697" steps="16"/></proof>
     </goal>
     <goal name="vc_produces_one&#39;0.0.0.1" proved="true">
     <transf name="exists" proved="true" arg1="(singleton f)">
      <goal name="vc_produces_one&#39;0.0.0.1.0" proved="true">
      <transf name="split_vc" proved="true" >
       <goal name="vc_produces_one&#39;0.0.0.1.0.0" proved="true">
-      <proof prover="3" timelimit="5"><result status="valid" time="0.018782" steps="19"/></proof>
+      <proof prover="3"><result status="valid" time="0.018782" steps="19"/></proof>
       </goal>
       <goal name="vc_produces_one&#39;0.0.0.1.0.1" proved="true">
       <transf name="exists" proved="true" arg1="(singleton e)">
        <goal name="vc_produces_one&#39;0.0.0.1.0.1.0" proved="true">
        <transf name="split_vc" proved="true" >
         <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.0" proved="true">
-        <proof prover="3" timelimit="5"><result status="valid" time="0.019230" steps="19"/></proof>
+        <proof prover="3"><result status="valid" time="0.019230" steps="19"/></proof>
         </goal>
         <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.1" proved="true">
-        <proof prover="2"><result status="valid" time="0.026157" steps="7537"/></proof>
+        <proof prover="3"><result status="valid" time="0.016468" steps="12"/></proof>
         </goal>
         <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.2" proved="true">
-        <proof prover="2"><result status="valid" time="0.106338" steps="15998"/></proof>
+        <proof prover="3"><result status="valid" time="0.045945" steps="248"/></proof>
         </goal>
         <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.3" proved="true">
-        <proof prover="3" timelimit="5"><result status="valid" time="0.019323" steps="24"/></proof>
+        <proof prover="3"><result status="valid" time="0.019323" steps="24"/></proof>
         </goal>
         <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.4" proved="true">
-        <proof prover="0"><result status="valid" time="0.024676" steps="59798"/></proof>
+        <proof prover="3"><result status="valid" time="0.029714" steps="18"/></proof>
         </goal>
         <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.5" proved="true">
-        <proof prover="3" timelimit="5"><result status="valid" time="0.018616" steps="17"/></proof>
+        <proof prover="3"><result status="valid" time="0.018616" steps="17"/></proof>
         </goal>
         <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.6" proved="true">
-        <proof prover="3" timelimit="5"><result status="valid" time="0.017070" steps="21"/></proof>
+        <proof prover="3"><result status="valid" time="0.017070" steps="21"/></proof>
         </goal>
         <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.7" proved="true">
-        <proof prover="3" timelimit="5"><result status="valid" time="0.025921" steps="30"/></proof>
+        <proof prover="3"><result status="valid" time="0.025921" steps="30"/></proof>
         </goal>
         <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.8" proved="true">
         <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
          <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.8.0" proved="true">
-         <proof prover="3" timelimit="5"><result status="valid" time="0.056708" steps="349"/></proof>
+         <proof prover="3"><result status="valid" time="0.056708" steps="349"/></proof>
          </goal>
         </transf>
         </goal>
         <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.9" proved="true">
         <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
          <goal name="vc_produces_one&#39;0.0.0.1.0.1.0.9.0" proved="true">
-         <proof prover="3" timelimit="5"><result status="valid" time="0.088230" steps="352"/></proof>
+         <proof prover="3"><result status="valid" time="0.088230" steps="352"/></proof>
          </goal>
         </transf>
         </goal>
@@ -2317,7 +2317,7 @@
   <goal name="vc_produces_one&#39;0.1" proved="true">
   <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
    <goal name="vc_produces_one&#39;0.1.0" proved="true">
-   <proof prover="0"><result status="valid" time="0.124858" steps="256688"/></proof>
+   <proof prover="2" timelimit="1"><result status="valid" time="0.701793" steps="251521"/></proof>
    </goal>
   </transf>
   </goal>
@@ -2326,7 +2326,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__once__qyi8116812009287608646__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="2"><result status="valid" time="0.035276" steps="102"/></proof>
+ <proof prover="3"><result status="valid" time="0.012797" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__once__qyi8116812009287608646__produces_refl" proved="true">
@@ -2336,7 +2336,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__once__qyi8116812009287608646__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="0"><result status="valid" time="0.019876" steps="70"/></proof>
+ <proof prover="3"><result status="valid" time="0.011484" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__once__qyi8116812009287608646__produces_trans" proved="true">
@@ -2349,12 +2349,12 @@
     <goal name="vc_produces_trans&#39;0.0.0.0" proved="true">
     <transf name="inline_goal" proved="true" >
      <goal name="vc_produces_trans&#39;0.0.0.0.0" proved="true">
-     <proof prover="0" timelimit="30" memlimit="4000"><result status="valid" time="0.047345" steps="44505"/></proof>
+     <proof prover="3"><result status="valid" time="0.042530" steps="409"/></proof>
      </goal>
     </transf>
     </goal>
     <goal name="vc_produces_trans&#39;0.0.0.1" proved="true">
-    <proof prover="3" timelimit="5"><result status="valid" time="0.060052" steps="184"/></proof>
+    <proof prover="3"><result status="valid" time="0.060052" steps="184"/></proof>
     </goal>
    </transf>
    </goal>
@@ -2365,7 +2365,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__range__qyi16860283617022118777__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="0"><result status="valid" time="0.018597" steps="70"/></proof>
+ <proof prover="3"><result status="valid" time="0.011734" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__range__qyi16860283617022118777__produces_refl" proved="true">
@@ -2375,7 +2375,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__range__qyi16860283617022118777__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="1"><result status="valid" time="0.033451" steps="163"/></proof>
+ <proof prover="3"><result status="valid" time="0.010255" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__range__qyi16860283617022118777__produces_trans" proved="true">
@@ -2390,7 +2390,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__range__qyi11108913944999844411__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.023012" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.023012" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__range__qyi11108913944999844411__produces_refl" proved="true">
@@ -2400,7 +2400,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__range__qyi11108913944999844411__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="2"><result status="valid" time="0.037411" steps="256"/></proof>
+ <proof prover="3"><result status="valid" time="0.013419" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__range__qyi11108913944999844411__produces_trans" proved="true">
@@ -2410,7 +2410,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__repeat__qyi8658929399712466629__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="2"><result status="valid" time="0.036280" steps="102"/></proof>
+ <proof prover="3"><result status="valid" time="0.008767" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__repeat__qyi8658929399712466629__produces_refl" proved="true">
@@ -2420,7 +2420,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__repeat__qyi8658929399712466629__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.023084" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.023084" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__repeat__qyi8658929399712466629__produces_trans" proved="true">
@@ -2430,12 +2430,12 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__skip__qyi14372835745621067113__resolve_coherence__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="1"><result status="valid" time="0.020249" steps="504"/></proof>
+ <proof prover="3"><result status="valid" time="0.018458" steps="2"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__skip__qyi3195031491774060502__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.021646" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.021646" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__skip__qyi3195031491774060502__produces_refl" proved="true">
@@ -2445,26 +2445,26 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__skip__qyi3195031491774060502__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="0"><result status="valid" time="0.018824" steps="837"/></proof>
+ <proof prover="3"><result status="valid" time="0.019698" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__skip__qyi3195031491774060502__produces_trans" proved="true">
  <goal name="vc_produces_trans&#39;0" proved="true">
  <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
   <goal name="vc_produces_trans&#39;0.0" proved="true">
-  <proof prover="1"><result status="valid" time="0.041057" steps="9739"/></proof>
+  <proof prover="2" timelimit="1"><result status="valid" time="0.037964" steps="10141"/></proof>
   </goal>
  </transf>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__take__qyi11550387566643656565__resolve_coherence__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.018550" steps="2"/></proof>
+ <proof prover="3"><result status="valid" time="0.018550" steps="2"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__take__qyi12344256497067751022__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="2"><result status="valid" time="0.038854" steps="1409"/></proof>
+ <proof prover="3"><result status="valid" time="0.013894" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__take__qyi12344256497067751022__produces_refl" proved="true">
@@ -2474,7 +2474,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__take__qyi12344256497067751022__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.021970" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.021970" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__take__qyi12344256497067751022__produces_trans" proved="true">
@@ -2484,17 +2484,17 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__zip__qyi2281060687216883844__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.022810" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.022810" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__zip__qyi2281060687216883844__produces_refl" proved="true">
  <goal name="vc_produces_refl&#39;0" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.042157" steps="27"/></proof>
+ <proof prover="3"><result status="valid" time="0.042157" steps="27"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__zip__qyi2281060687216883844__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="2"><result status="valid" time="0.041177" steps="1573"/></proof>
+ <proof prover="3"><result status="valid" time="0.014558" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__iter__zip__qyi2281060687216883844__produces_trans" proved="true">
@@ -2507,7 +2507,7 @@
     <goal name="vc_produces_trans&#39;0.0.0.0" proved="true">
     <transf name="exists" proved="true" arg1="(p2++p21)">
      <goal name="vc_produces_trans&#39;0.0.0.0.0" proved="true">
-     <proof prover="3" timelimit="5"><result status="valid" time="0.053930" steps="170"/></proof>
+     <proof prover="3"><result status="valid" time="0.053930" steps="170"/></proof>
      </goal>
     </transf>
     </goal>
@@ -2575,7 +2575,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__option__qyi15354566128244900690__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.009756" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.009756" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__option__qyi15354566128244900690__produces_refl" proved="true">
@@ -2585,7 +2585,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__option__qyi15354566128244900690__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="2"><result status="valid" time="0.017861" steps="102"/></proof>
+ <proof prover="3"><result status="valid" time="0.017253" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__option__qyi15354566128244900690__produces_trans" proved="true">
@@ -2596,10 +2596,10 @@
    <goal name="vc_produces_trans&#39;0.0.0" proved="true">
    <transf name="split_all_full" proved="true" >
     <goal name="vc_produces_trans&#39;0.0.0.0" proved="true">
-    <proof prover="2" memlimit="2000"><result status="valid" time="4.062279" steps="319009"/></proof>
+    <proof prover="3"><result status="valid" time="0.024062" steps="258"/></proof>
     </goal>
     <goal name="vc_produces_trans&#39;0.0.0.1" proved="true">
-    <proof prover="2"><result status="valid" time="0.385603" steps="45579"/></proof>
+    <proof prover="3"><result status="valid" time="0.040039" steps="183"/></proof>
     </goal>
    </transf>
    </goal>
@@ -2610,7 +2610,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__option__qyi15411423289202690388__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="2"><result status="valid" time="0.015801" steps="102"/></proof>
+ <proof prover="3"><result status="valid" time="0.018383" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__option__qyi15411423289202690388__produces_refl" proved="true">
@@ -2620,7 +2620,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__option__qyi15411423289202690388__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="0"><result status="valid" time="0.013024" steps="70"/></proof>
+ <proof prover="3"><result status="valid" time="0.020059" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__option__qyi15411423289202690388__produces_trans" proved="true">
@@ -2631,10 +2631,10 @@
    <goal name="vc_produces_trans&#39;0.0.0" proved="true">
    <transf name="split_all_full" proved="true" >
     <goal name="vc_produces_trans&#39;0.0.0.0" proved="true">
-    <proof prover="2" memlimit="2000"><result status="valid" time="3.985917" steps="319009"/></proof>
+    <proof prover="3"><result status="valid" time="0.034844" steps="258"/></proof>
     </goal>
     <goal name="vc_produces_trans&#39;0.0.0.1" proved="true">
-    <proof prover="2"><result status="valid" time="0.401688" steps="45579"/></proof>
+    <proof prover="3"><result status="valid" time="0.018784" steps="183"/></proof>
     </goal>
    </transf>
    </goal>
@@ -2645,7 +2645,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__option__qyi6601631924869095363__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="2"><result status="valid" time="0.032794" steps="102"/></proof>
+ <proof prover="3"><result status="valid" time="0.015995" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__option__qyi6601631924869095363__produces_refl" proved="true">
@@ -2655,7 +2655,7 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__option__qyi6601631924869095363__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="2"><result status="valid" time="0.036545" steps="102"/></proof>
+ <proof prover="3"><result status="valid" time="0.015185" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__option__qyi6601631924869095363__produces_trans" proved="true">
@@ -2666,10 +2666,10 @@
    <goal name="vc_produces_trans&#39;0.0.0" proved="true">
    <transf name="split_all_full" proved="true" >
     <goal name="vc_produces_trans&#39;0.0.0.0" proved="true">
-    <proof prover="2" memlimit="2000"><result status="valid" time="3.906816" steps="317192"/></proof>
+    <proof prover="3"><result status="valid" time="0.029006" steps="259"/></proof>
     </goal>
     <goal name="vc_produces_trans&#39;0.0.0.1" proved="true">
-    <proof prover="2"><result status="valid" time="0.401865" steps="48925"/></proof>
+    <proof prover="3"><result status="valid" time="0.032958" steps="183"/></proof>
     </goal>
    </transf>
    </goal>
@@ -2700,17 +2700,17 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__vec__qyi6844585276173866460__resolve_coherence__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.019625" steps="2"/></proof>
+ <proof prover="3"><result status="valid" time="0.019625" steps="2"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__vec__qyi8594830193745006303__resolve_coherence__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="2"><result status="valid" time="0.036074" steps="481"/></proof>
+ <proof prover="3"><result status="valid" time="0.009926" steps="2"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__vec__qyi12862303518309667396__produces_refl__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.023053" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.023053" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__vec__qyi12862303518309667396__produces_refl" proved="true">
@@ -2719,7 +2719,7 @@
   <goal name="vc_produces_refl&#39;0.0" proved="true">
   <transf name="split_all_full" proved="true" >
    <goal name="vc_produces_refl&#39;0.0.0" proved="true">
-   <proof prover="2" memlimit="2000"><result status="valid" time="0.066793" steps="5102"/></proof>
+   <proof prover="3"><result status="valid" time="0.025656" steps="29"/></proof>
    </goal>
   </transf>
   </goal>
@@ -2728,21 +2728,21 @@
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__vec__qyi12862303518309667396__produces_trans__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="0"><result status="valid" time="0.027023" steps="154"/></proof>
+ <proof prover="3"><result status="valid" time="0.013981" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__stdqy35z1__vec__qyi12862303518309667396__produces_trans" proved="true">
  <goal name="vc_produces_trans&#39;0" proved="true">
  <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
   <goal name="vc_produces_trans&#39;0.0" proved="true">
-  <proof prover="2"><result status="valid" time="0.033460" steps="5643"/></proof>
+  <proof prover="3"><result status="valid" time="0.028354" steps="24"/></proof>
   </goal>
  </transf>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__ghost__qyi17645547594388049322__clone__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="1"><result status="valid" time="0.020011" steps="190"/></proof>
+ <proof prover="3"><result status="valid" time="0.022235" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__ghost__qyi17645547594388049322__clone" proved="true">
@@ -2752,7 +2752,7 @@
 </theory>
 <theory name="M_creusot_contracts__ghost__qyi1862168959261460300__deref__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.020731" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.020731" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__ghost__qyi1862168959261460300__deref" proved="true">
@@ -2762,7 +2762,7 @@
 </theory>
 <theory name="M_creusot_contracts__ghost__qyi17214052996668775070__deref_mut__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="1"><result status="valid" time="0.024494" steps="2168"/></proof>
+ <proof prover="3"><result status="valid" time="0.013831" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__ghost__qyi17214052996668775070__deref_mut" proved="true">
@@ -2772,7 +2772,7 @@
 </theory>
 <theory name="M_creusot_contracts__ghost__qyi2241556416362616690__resolve_coherence__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.020834" steps="0"/></proof>
+ <proof prover="3"><result status="valid" time="0.020834" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__ghost__qyi2175792468772189056__borrow" proved="true">
@@ -2807,7 +2807,12 @@
 </theory>
 <theory name="M_creusot_contracts__logic__fmap__qyi9892930999379617882__contains_ghost" proved="true">
  <goal name="vc_contains_ghost&#39;0" proved="true">
- <proof prover="3"><result status="valid" time="0.011990" steps="35"/></proof>
+ <proof prover="3"><result status="valid" time="0.011990" steps="40"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__logic__fmap__qyi4648834920430559677__clone__refines" proved="true">
+ <goal name="refines" proved="true">
+ <proof prover="3"><result status="valid" time="0.026100" steps="2"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__util__unwrap" proved="true">
@@ -2827,12 +2832,22 @@
 </theory>
 <theory name="M_creusot_contracts__snapshot__qyi5567339964777190687__clone__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="1"><result status="valid" time="0.023986" steps="524"/></proof>
+ <proof prover="3"><result status="valid" time="0.018112" steps="6"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__logic__seq__qyi8239750555979287100__clone__refines" proved="true">
+ <goal name="refines" proved="true">
+ <proof prover="3"><result status="valid" time="0.028328" steps="0"/></proof>
+ </goal>
+</theory>
+<theory name="M_creusot_contracts__logic__fset__qyi11096226875104347554__clone__refines" proved="true">
+ <goal name="refines" proved="true">
+ <proof prover="3"><result status="valid" time="0.032160" steps="0"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__logic__int__qyi3540547019284611154__clone__refines" proved="true">
  <goal name="refines" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.019936" steps="6"/></proof>
+ <proof prover="3"><result status="valid" time="0.019936" steps="6"/></proof>
  </goal>
 </theory>
 <theory name="M_creusot_contracts__logic__int__qyi8495612394334423323__eq__refines" proved="true">
diff --git a/creusot/tests/creusot-contracts/creusot-contracts/why3shapes.gz b/creusot/tests/creusot-contracts/creusot-contracts/why3shapes.gz
index dc51f2921..18053c4de 100644
Binary files a/creusot/tests/creusot-contracts/creusot-contracts/why3shapes.gz and b/creusot/tests/creusot-contracts/creusot-contracts/why3shapes.gz differ
diff --git a/creusot/tests/should_fail/bug/878.coma b/creusot/tests/should_fail/bug/878.coma
index c1fae20a9..eba933955 100644
--- a/creusot/tests/should_fail/bug/878.coma
+++ b/creusot/tests/should_fail/bug/878.coma
@@ -112,7 +112,7 @@ module M_878__test2 [#"878.rs" 19 0 19 14]
   let%span sboxed7 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   let%span svec8 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sslice9 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
-  let%span sseq10 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq10 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span s87811 = "878.rs" 15 8 15 22
   
   use prelude.prelude.UInt32
@@ -254,7 +254,7 @@ module M_878__test3 [#"878.rs" 25 0 25 14]
   let%span sboxed7 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   let%span svec8 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sslice9 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
-  let%span sseq10 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq10 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span s87811 = "878.rs" 15 8 15 22
   
   use prelude.prelude.UInt32
diff --git a/creusot/tests/should_fail/bug/specialize.coma b/creusot/tests/should_fail/bug/specialize.coma
index ab52d8f60..d6c798deb 100644
--- a/creusot/tests/should_fail/bug/specialize.coma
+++ b/creusot/tests/should_fail/bug/specialize.coma
@@ -43,7 +43,7 @@ module M_specialize__g [#"specialize.rs" 27 0 27 18]
   let%span sspecialize2 = "specialize.rs" 6 9 6 13
   let%span svec3 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span svec4 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sseq5 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq5 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed6 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Opaque
@@ -169,7 +169,7 @@ module M_specialize__qyi2463200954251793265__x__refines [#"specialize.rs" 12 4 1
   let%span sspecialize0 = "specialize.rs" 12 4 12 22
   let%span svec1 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span svec2 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sseq3 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq3 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed4 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Opaque
diff --git a/creusot/tests/should_succeed/bug/final_borrows.coma b/creusot/tests/should_succeed/bug/final_borrows.coma
index 4073975ab..b58b79456 100644
--- a/creusot/tests/should_succeed/bug/final_borrows.coma
+++ b/creusot/tests/should_succeed/bug/final_borrows.coma
@@ -1943,7 +1943,7 @@ module M_final_borrows__index_mut_slice [#"final_borrows.rs" 208 0 208 48]
   let%span sslice10 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
   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
+  let%span sseq13 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed14 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.UIntSize
@@ -2104,7 +2104,7 @@ module M_final_borrows__index_mut_array [#"final_borrows.rs" 214 0 214 52]
   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
-  let%span sseq11 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq11 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed12 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.UIntSize
diff --git a/creusot/tests/should_succeed/ghost/ghost_map.coma b/creusot/tests/should_succeed/ghost/ghost_map.coma
index ec4d8ae07..2570c6600 100644
--- a/creusot/tests/should_succeed/ghost/ghost_map.coma
+++ b/creusot/tests/should_succeed/ghost/ghost_map.coma
@@ -1,101 +1,112 @@
 module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18]
   let%span sghost_map0 = "ghost_map.rs" 5 18 5 41
-  let%span sfmap1 = "../../../../creusot-contracts/src/logic/fmap.rs" 237 14 237 31
-  let%span sghost_map2 = "ghost_map.rs" 7 22 7 53
-  let%span sghost_map3 = "ghost_map.rs" 8 25 8 26
-  let%span sghost_map4 = "ghost_map.rs" 8 28 8 30
-  let%span sghost_map5 = "ghost_map.rs" 10 22 10 47
-  let%span sghost_map6 = "ghost_map.rs" 11 22 11 34
-  let%span sghost_map7 = "ghost_map.rs" 12 28 12 29
-  let%span sghost_map8 = "ghost_map.rs" 12 31 12 32
-  let%span sghost_map9 = "ghost_map.rs" 12 34 12 35
-  let%span sghost_map10 = "ghost_map.rs" 14 17 14 19
-  let%span sghost_map11 = "ghost_map.rs" 16 22 16 47
-  let%span sghost_map12 = "ghost_map.rs" 18 45 18 46
-  let%span sghost_map13 = "ghost_map.rs" 18 48 18 50
-  let%span sghost_map14 = "ghost_map.rs" 19 45 19 46
-  let%span sghost_map15 = "ghost_map.rs" 19 48 19 51
-  let%span sghost_map16 = "ghost_map.rs" 21 22 21 43
-  let%span sghost_map17 = "ghost_map.rs" 22 22 22 50
-  let%span sghost_map18 = "ghost_map.rs" 23 22 23 34
-  let%span sghost_map19 = "ghost_map.rs" 24 22 24 48
-  let%span sghost_map20 = "ghost_map.rs" 25 22 25 47
-  let%span sghost_map21 = "ghost_map.rs" 30 22 30 42
-  let%span sghost_map22 = "ghost_map.rs" 31 22 31 49
-  let%span sghost_map23 = "ghost_map.rs" 32 22 32 42
-  let%span sghost_map24 = "ghost_map.rs" 33 22 33 43
-  let%span sghost_map25 = "ghost_map.rs" 38 22 38 31
-  let%span sghost_map26 = "ghost_map.rs" 39 22 39 32
-  let%span sghost_map27 = "ghost_map.rs" 40 22 40 32
-  let%span sghost_map28 = "ghost_map.rs" 45 22 45 42
-  let%span sghost_map29 = "ghost_map.rs" 46 22 46 34
-  let%span sghost_map30 = "ghost_map.rs" 47 22 47 34
-  let%span sghost31 = "../../../../creusot-contracts/src/ghost.rs" 217 9 217 15
-  let%span sfmap32 = "../../../../creusot-contracts/src/logic/fmap.rs" 139 8 139 34
-  let%span sfmap33 = "../../../../creusot-contracts/src/logic/fmap.rs" 132 8 132 35
-  let%span sghost34 = "../../../../creusot-contracts/src/ghost.rs" 85 22 85 26
-  let%span sghost35 = "../../../../creusot-contracts/src/ghost.rs" 85 4 85 48
-  let%span sghost36 = "../../../../creusot-contracts/src/ghost.rs" 84 14 84 36
-  let%span sfmap37 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 35 376 38
-  let%span sfmap38 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 43 376 48
-  let%span sfmap39 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 4 378 17
-  let%span sfmap40 = "../../../../creusot-contracts/src/logic/fmap.rs" 374 14 374 49
-  let%span sfmap41 = "../../../../creusot-contracts/src/logic/fmap.rs" 375 14 375 40
-  let%span sghost42 = "../../../../creusot-contracts/src/ghost.rs" 69 14 69 18
-  let%span sghost43 = "../../../../creusot-contracts/src/ghost.rs" 69 4 69 36
-  let%span sghost44 = "../../../../creusot-contracts/src/ghost.rs" 68 14 68 35
-  let%span sfmap45 = "../../../../creusot-contracts/src/logic/fmap.rs" 264 14 264 34
-  let%span sfmap46 = "../../../../creusot-contracts/src/logic/fmap.rs" 116 9 116 31
-  let%span sfmap47 = "../../../../creusot-contracts/src/logic/fmap.rs" 348 36 348 39
-  let%span sfmap48 = "../../../../creusot-contracts/src/logic/fmap.rs" 348 4 348 62
-  let%span sfmap49 = "../../../../creusot-contracts/src/logic/fmap.rs" 336 4 345 11
-  let%span sfmap50 = "../../../../creusot-contracts/src/logic/fmap.rs" 346 14 346 89
-  let%span sfmap51 = "../../../../creusot-contracts/src/logic/fmap.rs" 347 14 347 44
-  let%span sfmap52 = "../../../../creusot-contracts/src/logic/fmap.rs" 415 35 415 38
-  let%span sfmap53 = "../../../../creusot-contracts/src/logic/fmap.rs" 415 4 417 17
-  let%span sfmap54 = "../../../../creusot-contracts/src/logic/fmap.rs" 413 14 413 43
-  let%span sfmap55 = "../../../../creusot-contracts/src/logic/fmap.rs" 414 14 414 41
-  let%span sfmap56 = "../../../../creusot-contracts/src/logic/fmap.rs" 92 8 95 9
-  let%span sfmap57 = "../../../../creusot-contracts/src/logic/fmap.rs" 285 33 285 36
-  let%span sfmap58 = "../../../../creusot-contracts/src/logic/fmap.rs" 284 14 284 43
-  let%span sfmap59 = "../../../../creusot-contracts/src/logic/fmap.rs" 314 28 314 31
-  let%span sfmap60 = "../../../../creusot-contracts/src/logic/fmap.rs" 314 4 314 50
-  let%span sfmap61 = "../../../../creusot-contracts/src/logic/fmap.rs" 306 4 313 11
-  let%span sghost62 = "../../../../creusot-contracts/src/ghost.rs" 181 15 181 16
-  let%span sghost63 = "../../../../creusot-contracts/src/ghost.rs" 181 4 181 28
-  let%span sghost64 = "../../../../creusot-contracts/src/ghost.rs" 179 14 179 28
-  let%span sfmap65 = "../../../../creusot-contracts/src/logic/fmap.rs" 39 14 39 31
-  let%span sfmap66 = "../../../../creusot-contracts/src/logic/fmap.rs" 40 14 40 49
-  let%span sfmap67 = "../../../../creusot-contracts/src/logic/fmap.rs" 214 14 214 38
-  let%span sfmap68 = "../../../../creusot-contracts/src/logic/fmap.rs" 215 14 215 83
-  let%span sfmap69 = "../../../../creusot-contracts/src/logic/fmap.rs" 217 8 217 35
-  let%span sfmap70 = "../../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26
-  let%span sfmap71 = "../../../../creusot-contracts/src/logic/fmap.rs" 66 14 66 71
-  let%span sfmap72 = "../../../../creusot-contracts/src/logic/fmap.rs" 67 14 67 61
-  let%span sfmap73 = "../../../../creusot-contracts/src/logic/fmap.rs" 68 14 68 66
-  let%span sresolve74 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
-  let%span sfmap75 = "../../../../creusot-contracts/src/logic/fmap.rs" 48 14 48 25
-  let%span sfmap76 = "../../../../creusot-contracts/src/logic/fmap.rs" 124 8 124 35
-  let%span sfmap77 = "../../../../creusot-contracts/src/logic/fmap.rs" 76 14 76 55
-  let%span sfmap78 = "../../../../creusot-contracts/src/logic/fmap.rs" 77 14 77 84
-  let%span sfmap79 = "../../../../creusot-contracts/src/logic/fmap.rs" 58 14 58 86
-  let%span sutil80 = "../../../../creusot-contracts/src/util.rs" 21 14 21 30
-  let%span sutil81 = "../../../../creusot-contracts/src/util.rs" 43 11 43 21
-  let%span sutil82 = "../../../../creusot-contracts/src/util.rs" 44 10 44 28
+  let%span sfmap1 = "../../../../creusot-contracts/src/logic/fmap.rs" 239 4 239 34
+  let%span sfmap2 = "../../../../creusot-contracts/src/logic/fmap.rs" 237 14 237 31
+  let%span sghost_map3 = "ghost_map.rs" 7 22 7 53
+  let%span sghost_map4 = "ghost_map.rs" 8 25 8 26
+  let%span sghost_map5 = "ghost_map.rs" 8 28 8 30
+  let%span sghost_map6 = "ghost_map.rs" 10 22 10 47
+  let%span sghost_map7 = "ghost_map.rs" 11 22 11 34
+  let%span sghost_map8 = "ghost_map.rs" 12 28 12 29
+  let%span sghost_map9 = "ghost_map.rs" 12 31 12 32
+  let%span sghost_map10 = "ghost_map.rs" 12 34 12 35
+  let%span sghost_map11 = "ghost_map.rs" 14 17 14 19
+  let%span sghost_map12 = "ghost_map.rs" 16 22 16 47
+  let%span sghost_map13 = "ghost_map.rs" 18 45 18 46
+  let%span sghost_map14 = "ghost_map.rs" 18 48 18 50
+  let%span sghost_map15 = "ghost_map.rs" 19 45 19 46
+  let%span sghost_map16 = "ghost_map.rs" 19 48 19 51
+  let%span sghost_map17 = "ghost_map.rs" 21 22 21 43
+  let%span sghost_map18 = "ghost_map.rs" 22 22 22 50
+  let%span sghost_map19 = "ghost_map.rs" 23 22 23 34
+  let%span sghost_map20 = "ghost_map.rs" 24 22 24 48
+  let%span sghost_map21 = "ghost_map.rs" 25 22 25 47
+  let%span sghost_map22 = "ghost_map.rs" 30 22 30 42
+  let%span sghost_map23 = "ghost_map.rs" 31 22 31 49
+  let%span sghost_map24 = "ghost_map.rs" 32 22 32 42
+  let%span sghost_map25 = "ghost_map.rs" 33 22 33 43
+  let%span sghost_map26 = "ghost_map.rs" 38 22 38 31
+  let%span sghost_map27 = "ghost_map.rs" 39 22 39 32
+  let%span sghost_map28 = "ghost_map.rs" 40 22 40 32
+  let%span sghost_map29 = "ghost_map.rs" 45 22 45 42
+  let%span sghost_map30 = "ghost_map.rs" 46 22 46 34
+  let%span sghost_map31 = "ghost_map.rs" 47 22 47 34
+  let%span sghost32 = "../../../../creusot-contracts/src/ghost.rs" 217 9 217 15
+  let%span sfmap33 = "../../../../creusot-contracts/src/logic/fmap.rs" 139 8 139 34
+  let%span sfmap34 = "../../../../creusot-contracts/src/logic/fmap.rs" 132 8 132 35
+  let%span sghost35 = "../../../../creusot-contracts/src/ghost.rs" 85 22 85 26
+  let%span sghost36 = "../../../../creusot-contracts/src/ghost.rs" 85 4 85 48
+  let%span sghost37 = "../../../../creusot-contracts/src/ghost.rs" 84 14 84 36
+  let%span sfmap38 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 29 376 33
+  let%span sfmap39 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 35 376 38
+  let%span sfmap40 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 43 376 48
+  let%span sfmap41 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 4 378 17
+  let%span sfmap42 = "../../../../creusot-contracts/src/logic/fmap.rs" 374 14 374 49
+  let%span sfmap43 = "../../../../creusot-contracts/src/logic/fmap.rs" 375 14 375 40
+  let%span sghost44 = "../../../../creusot-contracts/src/ghost.rs" 69 14 69 18
+  let%span sghost45 = "../../../../creusot-contracts/src/ghost.rs" 69 4 69 36
+  let%span sghost46 = "../../../../creusot-contracts/src/ghost.rs" 68 14 68 35
+  let%span sfmap47 = "../../../../creusot-contracts/src/logic/fmap.rs" 265 22 265 26
+  let%span sfmap48 = "../../../../creusot-contracts/src/logic/fmap.rs" 264 14 264 34
+  let%span sfmap49 = "../../../../creusot-contracts/src/logic/fmap.rs" 116 9 116 31
+  let%span sfmap50 = "../../../../creusot-contracts/src/logic/fmap.rs" 348 30 348 34
+  let%span sfmap51 = "../../../../creusot-contracts/src/logic/fmap.rs" 348 36 348 39
+  let%span sfmap52 = "../../../../creusot-contracts/src/logic/fmap.rs" 348 4 348 62
+  let%span sfmap53 = "../../../../creusot-contracts/src/logic/fmap.rs" 336 4 345 11
+  let%span sfmap54 = "../../../../creusot-contracts/src/logic/fmap.rs" 346 14 346 89
+  let%span sfmap55 = "../../../../creusot-contracts/src/logic/fmap.rs" 347 14 347 44
+  let%span sfmap56 = "../../../../creusot-contracts/src/logic/fmap.rs" 415 29 415 33
+  let%span sfmap57 = "../../../../creusot-contracts/src/logic/fmap.rs" 415 35 415 38
+  let%span sfmap58 = "../../../../creusot-contracts/src/logic/fmap.rs" 415 4 417 17
+  let%span sfmap59 = "../../../../creusot-contracts/src/logic/fmap.rs" 413 14 413 43
+  let%span sfmap60 = "../../../../creusot-contracts/src/logic/fmap.rs" 414 14 414 41
+  let%span sfmap61 = "../../../../creusot-contracts/src/logic/fmap.rs" 92 8 95 9
+  let%span sfmap62 = "../../../../creusot-contracts/src/logic/fmap.rs" 285 27 285 31
+  let%span sfmap63 = "../../../../creusot-contracts/src/logic/fmap.rs" 285 33 285 36
+  let%span sfmap64 = "../../../../creusot-contracts/src/logic/fmap.rs" 284 14 284 43
+  let%span sfmap65 = "../../../../creusot-contracts/src/logic/fmap.rs" 314 22 314 26
+  let%span sfmap66 = "../../../../creusot-contracts/src/logic/fmap.rs" 314 28 314 31
+  let%span sfmap67 = "../../../../creusot-contracts/src/logic/fmap.rs" 314 4 314 50
+  let%span sfmap68 = "../../../../creusot-contracts/src/logic/fmap.rs" 306 4 313 11
+  let%span sghost69 = "../../../../creusot-contracts/src/ghost.rs" 181 15 181 16
+  let%span sghost70 = "../../../../creusot-contracts/src/ghost.rs" 181 4 181 28
+  let%span sghost71 = "../../../../creusot-contracts/src/ghost.rs" 179 14 179 28
+  let%span sfmap72 = "../../../../creusot-contracts/src/logic/fmap.rs" 39 14 39 31
+  let%span sfmap73 = "../../../../creusot-contracts/src/logic/fmap.rs" 40 14 40 49
+  let%span sfmap74 = "../../../../creusot-contracts/src/logic/fmap.rs" 214 14 214 38
+  let%span sfmap75 = "../../../../creusot-contracts/src/logic/fmap.rs" 215 14 215 83
+  let%span sfmap76 = "../../../../creusot-contracts/src/logic/fmap.rs" 217 8 217 35
+  let%span sfmap77 = "../../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26
+  let%span sfmap78 = "../../../../creusot-contracts/src/logic/fmap.rs" 66 14 66 71
+  let%span sfmap79 = "../../../../creusot-contracts/src/logic/fmap.rs" 67 14 67 61
+  let%span sfmap80 = "../../../../creusot-contracts/src/logic/fmap.rs" 68 14 68 66
+  let%span sresolve81 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
+  let%span sfmap82 = "../../../../creusot-contracts/src/logic/fmap.rs" 48 14 48 25
+  let%span sfmap83 = "../../../../creusot-contracts/src/logic/fmap.rs" 124 8 124 35
+  let%span sfmap84 = "../../../../creusot-contracts/src/logic/fmap.rs" 76 14 76 55
+  let%span sfmap85 = "../../../../creusot-contracts/src/logic/fmap.rs" 77 14 77 84
+  let%span sfmap86 = "../../../../creusot-contracts/src/logic/fmap.rs" 58 14 58 86
+  let%span sutil87 = "../../../../creusot-contracts/src/util.rs" 21 14 21 30
+  let%span sutil88 = "../../../../creusot-contracts/src/util.rs" 43 11 43 21
+  let%span sutil89 = "../../../../creusot-contracts/src/util.rs" 44 10 44 28
   
   type t_FMap'0
   
   type t_GhostBox'0  =
     { t_GhostBox__0'0: t_FMap'0 }
   
+  predicate inv'0 (_1 : t_GhostBox'0)
+  
+  axiom inv_axiom'0 [@rewrite] : forall x : t_GhostBox'0 [inv'0 x] . inv'0 x = true
+  
   function inner_logic'0 (self : t_GhostBox'0) : t_FMap'0 =
-    [%#sghost31] self.t_GhostBox__0'0
+    [%#sghost32] self.t_GhostBox__0'0
   
   use prelude.prelude.Int
   
   function len'0 (self : t_FMap'0) : int
   
-  axiom len'0_spec : forall self : t_FMap'0 . [%#sfmap75] len'0 self >= 0
+  axiom len'0_spec : forall self : t_FMap'0 . [%#sfmap82] len'0 self >= 0
   
   use prelude.prelude.Int32
   
@@ -107,147 +118,150 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18]
   
   function view'0 (self : t_FMap'0) : Map.map int32 (t_Option'3)
   
-  axiom view'0_spec : forall self : t_FMap'0 . [%#sfmap79] forall m1 : t_FMap'0, m2 : t_FMap'0 . m1 <> m2
+  axiom view'0_spec : forall self : t_FMap'0 . [%#sfmap86] forall m1 : t_FMap'0, m2 : t_FMap'0 . m1 <> m2
    -> view'0 m1 <> view'0 m2
   
   use map.Const
   
   function empty'0 (_1 : ()) : t_FMap'0
   
-  axiom empty'0_spec : forall _1 : () . ([%#sfmap65] len'0 (empty'0 _1) = 0)
-  && ([%#sfmap66] view'0 (empty'0 _1) = Const.const (C_None'3))
+  axiom empty'0_spec : forall _1 : () . ([%#sfmap72] len'0 (empty'0 _1) = 0)
+  && ([%#sfmap73] view'0 (empty'0 _1) = Const.const (C_None'3))
   
   use map.Map
   
   function get_unsized'0 [@inline:trivial] (self : t_FMap'0) (k : int32) : t_Option'3 =
-    [%#sfmap70] Map.get (view'0 self) k
+    [%#sfmap77] Map.get (view'0 self) k
   
   function ext_eq'0 (self : t_FMap'0) (other : t_FMap'0) : bool =
-    [%#sfmap69] view'0 self = view'0 other
+    [%#sfmap76] view'0 self = view'0 other
   
-  axiom ext_eq'0_spec : forall self : t_FMap'0, other : t_FMap'0 . ([%#sfmap67] ext_eq'0 self other  -> self = other)
-  && ([%#sfmap68] (forall k : int32 . get_unsized'0 self k = get_unsized'0 other k)  -> ext_eq'0 self other)
+  axiom ext_eq'0_spec : forall self : t_FMap'0, other : t_FMap'0 . ([%#sfmap74] ext_eq'0 self other  -> self = other)
+  && ([%#sfmap75] (forall k : int32 . get_unsized'0 self k = get_unsized'0 other k)  -> ext_eq'0 self other)
   
   function is_empty'0 (self : t_FMap'0) : bool =
-    [%#sfmap32] ext_eq'0 self (empty'0 ())
+    [%#sfmap33] ext_eq'0 self (empty'0 ())
   
   let rec new'0 (_1:()) (return'  (ret:t_GhostBox'0))= any
-    [ return' (result:t_GhostBox'0)-> {[%#sfmap1] is_empty'0 (inner_logic'0 result)} (! return' {result}) ]
+    [ return' (result:t_GhostBox'0)-> {[%#sfmap1] inv'0 result}
+      {[%#sfmap2] is_empty'0 (inner_logic'0 result)}
+      (! return' {result}) ]
     
   
   use prelude.prelude.Borrow
   
   function contains'0 [@inline:trivial] (self : t_FMap'0) (k : int32) : bool =
-    [%#sfmap33] get_unsized'0 self k <> C_None'3
+    [%#sfmap34] get_unsized'0 self k <> C_None'3
   
-  predicate inv'0 (_1 : borrowed (t_GhostBox'0))
+  predicate inv'1 (_1 : borrowed (t_GhostBox'0))
   
-  axiom inv_axiom'0 [@rewrite] : forall x : borrowed (t_GhostBox'0) [inv'0 x] . inv'0 x = true
+  axiom inv_axiom'1 [@rewrite] : forall x : borrowed (t_GhostBox'0) [inv'1 x] . inv'1 x = true
   
-  predicate inv'1 (_1 : borrowed (t_FMap'0))
+  predicate inv'2 (_1 : borrowed (t_FMap'0))
   
-  axiom inv_axiom'1 [@rewrite] : forall x : borrowed (t_FMap'0) [inv'1 x] . inv'1 x = true
+  axiom inv_axiom'2 [@rewrite] : forall x : borrowed (t_FMap'0) [inv'2 x] . inv'2 x = true
   
-  let rec deref_mut'0 (self:borrowed (t_GhostBox'0)) (return'  (ret:borrowed (t_FMap'0)))= {[@expl:deref_mut 'self' type invariant] [%#sghost34] inv'0 self}
+  let rec deref_mut'0 (self:borrowed (t_GhostBox'0)) (return'  (ret:borrowed (t_FMap'0)))= {[@expl:deref_mut 'self' type invariant] [%#sghost35] inv'1 self}
     any
-    [ return' (result:borrowed (t_FMap'0))-> {[%#sghost35] inv'1 result}
-      {[%#sghost36] result
+    [ return' (result:borrowed (t_FMap'0))-> {[%#sghost36] inv'2 result}
+      {[%#sghost37] result
       = Borrow.borrow_logic (self.current).t_GhostBox__0'0 (self.final).t_GhostBox__0'0 (Borrow.inherit_id (Borrow.get_id self) 1)}
       (! return' {result}) ]
     
   
-  predicate inv'2 (_1 : int32)
+  predicate inv'3 (_1 : int32)
   
-  axiom inv_axiom'2 [@rewrite] : forall x : int32 [inv'2 x] . inv'2 x = true
+  axiom inv_axiom'3 [@rewrite] : forall x : int32 [inv'3 x] . inv'3 x = true
   
   type t_Option'0  =
     | C_None'1
     | C_Some'1 int32
   
-  predicate inv'3 (_1 : t_Option'0)
+  predicate inv'4 (_1 : t_Option'0)
   
-  axiom inv_axiom'3 [@rewrite] : forall x : t_Option'0 [inv'3 x] . inv'3 x = true
+  axiom inv_axiom'4 [@rewrite] : forall x : t_Option'0 [inv'4 x] . inv'4 x = true
   
   function make_sized'0 (self : int32) : int32
   
-  axiom make_sized'0_spec : forall self : int32 . [%#sutil80] make_sized'0 self = self
+  axiom make_sized'0_spec : forall self : int32 . [%#sutil87] make_sized'0 self = self
   
   use map.Map
   
   function insert'0 (self : t_FMap'0) (k : int32) (v : int32) : t_FMap'0
   
-  axiom insert'0_spec : forall self : t_FMap'0, k : int32, v : int32 . ([%#sfmap71] view'0 (insert'0 self k v)
+  axiom insert'0_spec : forall self : t_FMap'0, k : int32, v : int32 . ([%#sfmap78] view'0 (insert'0 self k v)
   = Map.set (view'0 self) k (C_Some'3 (make_sized'0 v)))
-  && ([%#sfmap72] contains'0 self k  -> len'0 (insert'0 self k v) = len'0 self)
-  && ([%#sfmap73] not contains'0 self k  -> len'0 (insert'0 self k v) = len'0 self + 1)
+  && ([%#sfmap79] contains'0 self k  -> len'0 (insert'0 self k v) = len'0 self)
+  && ([%#sfmap80] not contains'0 self k  -> len'0 (insert'0 self k v) = len'0 self + 1)
   
   function get'0 [@inline:trivial] (self : t_FMap'0) (k : int32) : t_Option'0 =
-    [%#sfmap56] match get_unsized'0 self k with
+    [%#sfmap61] match get_unsized'0 self k with
       | C_None'3 -> C_None'1
       | C_Some'3 x -> C_Some'1 x
       end
   
-  let rec insert_ghost'0 (self:borrowed (t_FMap'0)) (key:int32) (value:int32) (return'  (ret:t_Option'0))= {[@expl:insert_ghost 'key' type invariant] [%#sfmap37] inv'2 key}
-    {[@expl:insert_ghost 'value' type invariant] [%#sfmap38] inv'2 value}
+  let rec insert_ghost'0 (self:borrowed (t_FMap'0)) (key:int32) (value:int32) (return'  (ret:t_Option'0))= {[@expl:insert_ghost 'self' type invariant] [%#sfmap38] inv'2 self}
+    {[@expl:insert_ghost 'key' type invariant] [%#sfmap39] inv'3 key}
+    {[@expl:insert_ghost 'value' type invariant] [%#sfmap40] inv'3 value}
     any
-    [ return' (result:t_Option'0)-> {[%#sfmap39] inv'3 result}
-      {[%#sfmap40] self.final = insert'0 self.current key value}
-      {[%#sfmap41] result = get'0 self.current key}
+    [ return' (result:t_Option'0)-> {[%#sfmap41] inv'4 result}
+      {[%#sfmap42] self.final = insert'0 self.current key value}
+      {[%#sfmap43] result = get'0 self.current key}
       (! return' {result}) ]
     
   
   predicate resolve'3 (self : borrowed (t_FMap'0)) =
-    [%#sresolve74] self.final = self.current
+    [%#sresolve81] self.final = self.current
   
   predicate resolve'0 (_1 : borrowed (t_FMap'0)) =
     resolve'3 _1
   
-  predicate inv'4 (_1 : t_GhostBox'0)
+  predicate inv'5 (_1 : t_GhostBox'0)
   
-  axiom inv_axiom'4 [@rewrite] : forall x : t_GhostBox'0 [inv'4 x] . inv'4 x = true
+  axiom inv_axiom'5 [@rewrite] : forall x : t_GhostBox'0 [inv'5 x] . inv'5 x = true
   
-  predicate inv'5 (_1 : t_FMap'0)
+  predicate inv'6 (_1 : t_FMap'0)
   
-  axiom inv_axiom'5 [@rewrite] : forall x : t_FMap'0 [inv'5 x] . inv'5 x = true
+  axiom inv_axiom'6 [@rewrite] : forall x : t_FMap'0 [inv'6 x] . inv'6 x = true
   
-  let rec deref'0 (self:t_GhostBox'0) (return'  (ret:t_FMap'0))= {[@expl:deref 'self' type invariant] [%#sghost42] inv'4 self}
+  let rec deref'0 (self:t_GhostBox'0) (return'  (ret:t_FMap'0))= {[@expl:deref 'self' type invariant] [%#sghost44] inv'5 self}
     any
-    [ return' (result:t_FMap'0)-> {[%#sghost43] inv'5 result}
-      {[%#sghost44] self.t_GhostBox__0'0 = result}
+    [ return' (result:t_FMap'0)-> {[%#sghost45] inv'6 result}
+      {[%#sghost46] self.t_GhostBox__0'0 = result}
       (! return' {result}) ]
     
   
-  let rec len_ghost'0 (self:t_FMap'0) (return'  (ret:int))= any
-    [ return' (result:int)-> {[%#sfmap45] result = len'0 self} (! return' {result}) ]
-    
+  let rec len_ghost'0 (self:t_FMap'0) (return'  (ret:int))= {[@expl:len_ghost 'self' type invariant] [%#sfmap47] inv'6 self}
+    any [ return' (result:int)-> {[%#sfmap48] result = len'0 self} (! return' {result}) ] 
   
   function unwrap'0 (op : t_Option'3) : int32
   
-  axiom unwrap'0_spec : forall op : t_Option'3 . ([%#sutil81] op <> C_None'3)
-   -> ([%#sutil82] C_Some'3 (unwrap'0 op) = op)
+  axiom unwrap'0_spec : forall op : t_Option'3 . ([%#sutil88] op <> C_None'3)
+   -> ([%#sutil89] C_Some'3 (unwrap'0 op) = op)
   
   function lookup_unsized'0 [@inline:trivial] (self : t_FMap'0) (k : int32) : int32 =
-    [%#sfmap76] unwrap'0 (get_unsized'0 self k)
+    [%#sfmap83] unwrap'0 (get_unsized'0 self k)
   
   function lookup'0 [@inline:trivial] (self : t_FMap'0) (k : int32) : int32 =
-    [%#sfmap46] lookup_unsized'0 self k
+    [%#sfmap49] lookup_unsized'0 self k
   
-  predicate inv'6 (_1 : int32)
+  predicate inv'7 (_1 : int32)
   
-  axiom inv_axiom'6 [@rewrite] : forall x : int32 [inv'6 x] . inv'6 x = true
+  axiom inv_axiom'7 [@rewrite] : forall x : int32 [inv'7 x] . inv'7 x = true
   
   type t_Option'1  =
     | C_None'0
     | C_Some'0 (borrowed int32)
   
-  predicate inv'7 (_1 : t_Option'1)
+  predicate inv'8 (_1 : t_Option'1)
   
-  axiom inv_axiom'7 [@rewrite] : forall x : t_Option'1 [inv'7 x] . inv'7 x = true
+  axiom inv_axiom'8 [@rewrite] : forall x : t_Option'1 [inv'8 x] . inv'8 x = true
   
-  let rec get_mut_ghost'0 (self:borrowed (t_FMap'0)) (key:int32) (return'  (ret:t_Option'1))= {[@expl:get_mut_ghost 'key' type invariant] [%#sfmap47] inv'6 key}
+  let rec get_mut_ghost'0 (self:borrowed (t_FMap'0)) (key:int32) (return'  (ret:t_Option'1))= {[@expl:get_mut_ghost 'self' type invariant] [%#sfmap50] inv'2 self}
+    {[@expl:get_mut_ghost 'key' type invariant] [%#sfmap51] inv'7 key}
     any
-    [ return' (result:t_Option'1)-> {[%#sfmap48] inv'7 result}
-      {[%#sfmap49] if contains'0 self.current key then
+    [ return' (result:t_Option'1)-> {[%#sfmap52] inv'8 result}
+      {[%#sfmap53] if contains'0 self.current key then
         match result with
           | C_None'0 -> false
           | C_Some'0 r -> contains'0 self.final key
@@ -256,13 +270,13 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18]
       else
         result = C_None'0 /\ self.current = self.final
       }
-      {[%#sfmap50] forall k : int32 . k <> key  -> get_unsized'0 self.current k = get_unsized'0 self.final k}
-      {[%#sfmap51] len'0 self.current = len'0 self.final}
+      {[%#sfmap54] forall k : int32 . k <> key  -> get_unsized'0 self.current k = get_unsized'0 self.final k}
+      {[%#sfmap55] len'0 self.current = len'0 self.final}
       (! return' {result}) ]
     
   
   predicate resolve'4 (self : borrowed int32) =
-    [%#sresolve74] self.final = self.current
+    [%#sresolve81] self.final = self.current
   
   predicate resolve'1 (_1 : borrowed int32) =
     resolve'4 _1
@@ -276,33 +290,36 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18]
   
   function remove'0 (self : t_FMap'0) (k : int32) : t_FMap'0
   
-  axiom remove'0_spec : forall self : t_FMap'0, k : int32 . ([%#sfmap77] view'0 (remove'0 self k)
+  axiom remove'0_spec : forall self : t_FMap'0, k : int32 . ([%#sfmap84] view'0 (remove'0 self k)
   = Map.set (view'0 self) k (C_None'3))
-  && ([%#sfmap78] len'0 (remove'0 self k) = (if contains'0 self k then len'0 self - 1 else len'0 self))
+  && ([%#sfmap85] len'0 (remove'0 self k) = (if contains'0 self k then len'0 self - 1 else len'0 self))
   
-  let rec remove_ghost'0 (self:borrowed (t_FMap'0)) (key:int32) (return'  (ret:t_Option'0))= {[@expl:remove_ghost 'key' type invariant] [%#sfmap52] inv'6 key}
+  let rec remove_ghost'0 (self:borrowed (t_FMap'0)) (key:int32) (return'  (ret:t_Option'0))= {[@expl:remove_ghost 'self' type invariant] [%#sfmap56] inv'2 self}
+    {[@expl:remove_ghost 'key' type invariant] [%#sfmap57] inv'7 key}
     any
-    [ return' (result:t_Option'0)-> {[%#sfmap53] inv'3 result}
-      {[%#sfmap54] self.final = remove'0 self.current key}
-      {[%#sfmap55] result = get'0 self.current key}
+    [ return' (result:t_Option'0)-> {[%#sfmap58] inv'4 result}
+      {[%#sfmap59] self.final = remove'0 self.current key}
+      {[%#sfmap60] result = get'0 self.current key}
       (! return' {result}) ]
     
   
-  let rec contains_ghost'0 (self:t_FMap'0) (key:int32) (return'  (ret:bool))= {[@expl:contains_ghost 'key' type invariant] [%#sfmap57] inv'6 key}
-    any [ return' (result:bool)-> {[%#sfmap58] result = contains'0 self key} (! return' {result}) ] 
+  let rec contains_ghost'0 (self:t_FMap'0) (key:int32) (return'  (ret:bool))= {[@expl:contains_ghost 'self' type invariant] [%#sfmap62] inv'6 self}
+    {[@expl:contains_ghost 'key' type invariant] [%#sfmap63] inv'7 key}
+    any [ return' (result:bool)-> {[%#sfmap64] result = contains'0 self key} (! return' {result}) ] 
   
   type t_Option'2  =
     | C_None'2
     | C_Some'2 int32
   
-  predicate inv'8 (_1 : t_Option'2)
+  predicate inv'9 (_1 : t_Option'2)
   
-  axiom inv_axiom'8 [@rewrite] : forall x : t_Option'2 [inv'8 x] . inv'8 x = true
+  axiom inv_axiom'9 [@rewrite] : forall x : t_Option'2 [inv'9 x] . inv'9 x = true
   
-  let rec get_ghost'0 (self:t_FMap'0) (key:int32) (return'  (ret:t_Option'2))= {[@expl:get_ghost 'key' type invariant] [%#sfmap59] inv'6 key}
+  let rec get_ghost'0 (self:t_FMap'0) (key:int32) (return'  (ret:t_Option'2))= {[@expl:get_ghost 'self' type invariant] [%#sfmap65] inv'6 self}
+    {[@expl:get_ghost 'key' type invariant] [%#sfmap66] inv'7 key}
     any
-    [ return' (result:t_Option'2)-> {[%#sfmap60] inv'8 result}
-      {[%#sfmap61] if contains'0 self key then
+    [ return' (result:t_Option'2)-> {[%#sfmap67] inv'9 result}
+      {[%#sfmap68] if contains'0 self key then
         match result with
           | C_None'2 -> false
           | C_Some'2 r -> lookup_unsized'0 self key = r
@@ -317,7 +334,7 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18]
     { field_0'0: borrowed (t_GhostBox'0) }
   
   predicate resolve'6 (self : borrowed (t_GhostBox'0)) =
-    [%#sresolve74] self.final = self.current
+    [%#sresolve81] self.final = self.current
   
   predicate resolve'5 (_1 : borrowed (t_GhostBox'0)) =
     resolve'6 _1
@@ -325,21 +342,21 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18]
   predicate resolve'2 (_1 : closure0'1) =
     resolve'5 _1.field_0'0
   
-  predicate inv'9 (_1 : ())
+  predicate inv'10 (_1 : ())
   
-  axiom inv_axiom'9 [@rewrite] : forall x : () [inv'9 x] . inv'9 x = true
+  axiom inv_axiom'10 [@rewrite] : forall x : () [inv'10 x] . inv'10 x = true
   
   type t_GhostBox'1  =
     { t_GhostBox__0'1: () }
   
-  predicate inv'10 (_1 : t_GhostBox'1)
+  predicate inv'11 (_1 : t_GhostBox'1)
   
-  axiom inv_axiom'10 [@rewrite] : forall x : t_GhostBox'1 [inv'10 x] . inv'10 x = true
+  axiom inv_axiom'11 [@rewrite] : forall x : t_GhostBox'1 [inv'11 x] . inv'11 x = true
   
-  let rec new'1 (x:()) (return'  (ret:t_GhostBox'1))= {[@expl:new 'x' type invariant] [%#sghost62] inv'9 x}
+  let rec new'1 (x:()) (return'  (ret:t_GhostBox'1))= {[@expl:new 'x' type invariant] [%#sghost69] inv'10 x}
     any
-    [ return' (result:t_GhostBox'1)-> {[%#sghost63] inv'10 result}
-      {[%#sghost64] result.t_GhostBox__0'1 = x}
+    [ return' (result:t_GhostBox'1)-> {[%#sghost70] inv'11 result}
+      {[%#sghost71] result.t_GhostBox__0'1 = x}
       (! return' {result}) ]
     
   
@@ -347,7 +364,7 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18]
   
   let rec closure0'0 (_1:closure0'1) (return'  (ret:t_GhostBox'1))= bb0
     [ bb0 = s0
-      [ s0 = {[@expl:assertion] [%#sghost_map2] forall k : int32 . not contains'0 (inner_logic'0 (_1.field_0'0).current) k}
+      [ s0 = {[@expl:assertion] [%#sghost_map3] forall k : int32 . not contains'0 (inner_logic'0 (_1.field_0'0).current) k}
         s1
       | s1 = Borrow.borrow_mut <t_GhostBox'0> {(_1.field_0'0).current}
           (fun (_ret':borrowed (t_GhostBox'0)) ->
@@ -360,7 +377,7 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18]
     | bb1 = s0
       [ s0 = Borrow.borrow_final <t_FMap'0> {_7.current} {Borrow.get_id _7}
           (fun (_ret':borrowed (t_FMap'0)) ->  [ &_6 <- _ret' ]  [ &_7 <- { _7 with current = _ret'.final } ] s1)
-      | s1 = insert_ghost'0 {_6} {[%#sghost_map3] (1 : int32)} {[%#sghost_map4] (21 : int32)}
+      | s1 = insert_ghost'0 {_6} {[%#sghost_map4] (1 : int32)} {[%#sghost_map5] (21 : int32)}
           (fun (_ret':t_Option'0) ->  [ &_5 <- _ret' ] s2)
       | s2 = bb2 ]
       
@@ -371,11 +388,13 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18]
       
     | bb3 = s0 [ s0 = len_ghost'0 {_11} (fun (_ret':int) ->  [ &length1 <- _ret' ] s1) | s1 = bb4 ] 
     | bb4 = s0
-      [ s0 = {[@expl:assertion] [%#sghost_map5] lookup'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32)
+      [ s0 = {[@expl:assertion] [%#sghost_map6] lookup'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32)
         = (21 : int32)}
         s1
-      | s1 = {[@expl:assertion] [%#sghost_map6] length1 = 1} s2
-      | s2 =  [ &_20 <- (([%#sghost_map7] (1 : int32)), ([%#sghost_map8] (2 : int32)), ([%#sghost_map9] (3 : int32))) ] 
+      | s1 = {[@expl:assertion] [%#sghost_map7] length1 = 1} s2
+      | s2 = 
+        [ &_20 <- (([%#sghost_map8] (1 : int32)), ([%#sghost_map9] (2 : int32)), ([%#sghost_map10] (3 : int32))) ]
+        
         s3
       | s3 =  [ &x1 <- let (r'0, _, _) = _20 in r'0 ] s4
       | s4 =  [ &x2 <- let (_, r'1, _) = _20 in r'1 ] s5
@@ -408,13 +427,13 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18]
     | bb7 = bb8
     | bb8 = s0
       [ s0 = v_Some'0 {_22} (fun (r0'0:borrowed int32) ->  [ &x <- r0'0 ] s1)
-      | s1 =  [ &x <- { x with current = ([%#sghost_map10] (42 : int32)) } ] s2
+      | s1 =  [ &x <- { x with current = ([%#sghost_map11] (42 : int32)) } ] s2
       | s2 = -{resolve'1 x}- s3
       | s3 = -{resolve'0 _24}- s4
       | s4 = bb10 ]
       
     | bb10 = s0
-      [ s0 = {[@expl:assertion] [%#sghost_map11] lookup'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32)
+      [ s0 = {[@expl:assertion] [%#sghost_map12] lookup'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32)
         = (42 : int32)}
         s1
       | s1 = Borrow.borrow_mut <t_GhostBox'0> {(_1.field_0'0).current}
@@ -428,7 +447,7 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18]
     | bb11 = s0
       [ s0 = Borrow.borrow_final <t_FMap'0> {_34.current} {Borrow.get_id _34}
           (fun (_ret':borrowed (t_FMap'0)) ->  [ &_33 <- _ret' ]  [ &_34 <- { _34 with current = _ret'.final } ] s1)
-      | s1 = insert_ghost'0 {_33} {[%#sghost_map12] (2 : int32)} {[%#sghost_map13] (50 : int32)}
+      | s1 = insert_ghost'0 {_33} {[%#sghost_map13] (2 : int32)} {[%#sghost_map14] (50 : int32)}
           (fun (_ret':t_Option'0) ->  [ &inserted_none <- _ret' ] s2)
       | s2 = bb12 ]
       
@@ -445,7 +464,7 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18]
     | bb13 = s0
       [ s0 = Borrow.borrow_final <t_FMap'0> {_38.current} {Borrow.get_id _38}
           (fun (_ret':borrowed (t_FMap'0)) ->  [ &_37 <- _ret' ]  [ &_38 <- { _38 with current = _ret'.final } ] s1)
-      | s1 = insert_ghost'0 {_37} {[%#sghost_map14] (2 : int32)} {[%#sghost_map15] (100 : int32)}
+      | s1 = insert_ghost'0 {_37} {[%#sghost_map15] (2 : int32)} {[%#sghost_map16] (100 : int32)}
           (fun (_ret':t_Option'0) ->  [ &inserted_some <- _ret' ] s2)
       | s2 = bb14 ]
       
@@ -456,13 +475,13 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18]
       
     | bb15 = s0 [ s0 = len_ghost'0 {_42} (fun (_ret':int) ->  [ &length2 <- _ret' ] s1) | s1 = bb16 ] 
     | bb16 = s0
-      [ s0 = {[@expl:assertion] [%#sghost_map16] inserted_none = C_None'1} s1
-      | s1 = {[@expl:assertion] [%#sghost_map17] inserted_some = C_Some'1 (50 : int32)} s2
-      | s2 = {[@expl:assertion] [%#sghost_map18] length2 = 2} s3
-      | s3 = {[@expl:assertion] [%#sghost_map19] lookup'0 (inner_logic'0 (_1.field_0'0).current) (2 : int32)
+      [ s0 = {[@expl:assertion] [%#sghost_map17] inserted_none = C_None'1} s1
+      | s1 = {[@expl:assertion] [%#sghost_map18] inserted_some = C_Some'1 (50 : int32)} s2
+      | s2 = {[@expl:assertion] [%#sghost_map19] length2 = 2} s3
+      | s3 = {[@expl:assertion] [%#sghost_map20] lookup'0 (inner_logic'0 (_1.field_0'0).current) (2 : int32)
         = (100 : int32)}
         s4
-      | s4 = {[@expl:assertion] [%#sghost_map20] lookup'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32)
+      | s4 = {[@expl:assertion] [%#sghost_map21] lookup'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32)
         = (42 : int32)}
         s5
       | s5 = Borrow.borrow_mut <t_GhostBox'0> {(_1.field_0'0).current}
@@ -516,10 +535,10 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18]
       
     | bb22 = s0
       [ s0 = -{resolve'0 _68}- s1
-      | s1 = {[@expl:assertion] [%#sghost_map21] remove_none1 = C_None'1} s2
-      | s2 = {[@expl:assertion] [%#sghost_map22] remove_some = C_Some'1 (100 : int32)} s3
-      | s3 = {[@expl:assertion] [%#sghost_map23] remove_none2 = C_None'1} s4
-      | s4 = {[@expl:assertion] [%#sghost_map24] get'0 (inner_logic'0 (_1.field_0'0).current) (2 : int32) = C_None'1} s5
+      | s1 = {[@expl:assertion] [%#sghost_map22] remove_none1 = C_None'1} s2
+      | s2 = {[@expl:assertion] [%#sghost_map23] remove_some = C_Some'1 (100 : int32)} s3
+      | s3 = {[@expl:assertion] [%#sghost_map24] remove_none2 = C_None'1} s4
+      | s4 = {[@expl:assertion] [%#sghost_map25] get'0 (inner_logic'0 (_1.field_0'0).current) (2 : int32) = C_None'1} s5
       | s5 = deref'0 {(_1.field_0'0).current} (fun (_ret':t_FMap'0) ->  [ &_82 <- _ret' ] s6)
       | s6 = bb23 ]
       
@@ -541,9 +560,9 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18]
       | s2 = bb28 ]
       
     | bb28 = s0
-      [ s0 = {[@expl:assertion] [%#sghost_map25] contains1} s1
-      | s1 = {[@expl:assertion] [%#sghost_map26] not contains2} s2
-      | s2 = {[@expl:assertion] [%#sghost_map27] not contains3} s3
+      [ s0 = {[@expl:assertion] [%#sghost_map26] contains1} s1
+      | s1 = {[@expl:assertion] [%#sghost_map27] not contains2} s2
+      | s2 = {[@expl:assertion] [%#sghost_map28] not contains3} s3
       | s3 = deref'0 {(_1.field_0'0).current} (fun (_ret':t_FMap'0) ->  [ &_106 <- _ret' ] s4)
       | s4 = bb29 ]
       
@@ -566,9 +585,9 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18]
       
     | bb34 = s0
       [ s0 = -{resolve'2 _1}- s1
-      | s1 = {[@expl:assertion] [%#sghost_map28] get1 = C_Some'2 (42 : int32)} s2
-      | s2 = {[@expl:assertion] [%#sghost_map29] get2 = C_None'2} s3
-      | s3 = {[@expl:assertion] [%#sghost_map30] get3 = C_None'2} s4
+      | s1 = {[@expl:assertion] [%#sghost_map29] get1 = C_Some'2 (42 : int32)} s2
+      | s2 = {[@expl:assertion] [%#sghost_map30] get2 = C_None'2} s3
+      | s3 = {[@expl:assertion] [%#sghost_map31] get3 = C_None'2} s4
       | s4 = new'1 {_2} (fun (_ret':t_GhostBox'1) ->  [ &_0 <- _ret' ] s5)
       | s5 = bb35 ]
       
diff --git a/creusot/tests/should_succeed/ghost/ghost_map/why3session.xml b/creusot/tests/should_succeed/ghost/ghost_map/why3session.xml
index 0c98bfe61..fb4e30b79 100644
--- a/creusot/tests/should_succeed/ghost/ghost_map/why3session.xml
+++ b/creusot/tests/should_succeed/ghost/ghost_map/why3session.xml
@@ -2,12 +2,12 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "https://www.why3.org/why3session.dtd">
 <why3session shape_version="6">
-<prover id="0" name="CVC5" version="1.0.5" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="1" name="CVC4" version="1.8" timelimit="1" steplimit="0" memlimit="1000"/>
 <file format="coma" proved="true">
 <path name=".."/><path name="ghost_map.coma"/>
 <theory name="M_ghost_map__ghost_map" proved="true">
  <goal name="vc_ghost_map&#39;0" proved="true">
- <proof prover="0"><result status="valid" time="4.430404" steps="542227"/></proof>
+ <proof prover="1"><result status="valid" time="0.510540" steps="61961"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/creusot/tests/should_succeed/ghost/ghost_map/why3shapes.gz b/creusot/tests/should_succeed/ghost/ghost_map/why3shapes.gz
index d2efb203a..1a76a6eab 100644
Binary files a/creusot/tests/should_succeed/ghost/ghost_map/why3shapes.gz and b/creusot/tests/should_succeed/ghost/ghost_map/why3shapes.gz differ
diff --git a/creusot/tests/should_succeed/ghost/ghost_set.coma b/creusot/tests/should_succeed/ghost/ghost_set.coma
index 4a11cd619..e4e93b45f 100644
--- a/creusot/tests/should_succeed/ghost/ghost_set.coma
+++ b/creusot/tests/should_succeed/ghost/ghost_set.coma
@@ -1,47 +1,52 @@
 module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18]
   let%span sghost_set0 = "ghost_set.rs" 5 18 5 36
-  let%span sfset1 = "../../../../creusot-contracts/src/logic/fset.rs" 183 14 183 31
-  let%span sghost_set2 = "ghost_set.rs" 7 22 7 53
-  let%span sghost_set3 = "ghost_set.rs" 8 25 8 26
-  let%span sghost_set4 = "ghost_set.rs" 10 22 10 63
-  let%span sghost_set5 = "ghost_set.rs" 11 22 11 34
-  let%span sghost_set6 = "ghost_set.rs" 12 28 12 29
-  let%span sghost_set7 = "ghost_set.rs" 12 31 12 32
-  let%span sghost_set8 = "ghost_set.rs" 12 34 12 35
-  let%span sghost_set9 = "ghost_set.rs" 14 45 14 46
-  let%span sghost_set10 = "ghost_set.rs" 15 46 15 47
-  let%span sghost_set11 = "ghost_set.rs" 17 22 17 54
-  let%span sghost_set12 = "ghost_set.rs" 18 22 18 34
-  let%span sghost_set13 = "ghost_set.rs" 19 22 19 62
-  let%span sghost_set14 = "ghost_set.rs" 24 22 24 69
-  let%span sghost_set15 = "ghost_set.rs" 25 22 25 41
-  let%span sghost_set16 = "ghost_set.rs" 26 22 26 36
-  let%span sghost_set17 = "ghost_set.rs" 31 22 31 31
-  let%span sghost_set18 = "ghost_set.rs" 32 22 32 32
-  let%span sghost_set19 = "ghost_set.rs" 33 22 33 32
-  let%span sghost20 = "../../../../creusot-contracts/src/ghost.rs" 217 9 217 15
-  let%span sfset21 = "../../../../creusot-contracts/src/logic/fset.rs" 46 8 46 26
-  let%span sghost22 = "../../../../creusot-contracts/src/ghost.rs" 85 22 85 26
-  let%span sghost23 = "../../../../creusot-contracts/src/ghost.rs" 85 4 85 48
-  let%span sghost24 = "../../../../creusot-contracts/src/ghost.rs" 84 14 84 36
-  let%span sfset25 = "../../../../creusot-contracts/src/logic/fset.rs" 266 35 266 40
-  let%span sfset26 = "../../../../creusot-contracts/src/logic/fset.rs" 264 14 264 44
-  let%span sfset27 = "../../../../creusot-contracts/src/logic/fset.rs" 265 14 265 48
-  let%span sghost28 = "../../../../creusot-contracts/src/ghost.rs" 69 14 69 18
-  let%span sghost29 = "../../../../creusot-contracts/src/ghost.rs" 69 4 69 36
-  let%span sghost30 = "../../../../creusot-contracts/src/ghost.rs" 68 14 68 35
-  let%span sfset31 = "../../../../creusot-contracts/src/logic/fset.rs" 210 14 210 34
-  let%span sfset32 = "../../../../creusot-contracts/src/logic/fset.rs" 302 35 302 40
-  let%span sfset33 = "../../../../creusot-contracts/src/logic/fset.rs" 300 14 300 45
-  let%span sfset34 = "../../../../creusot-contracts/src/logic/fset.rs" 301 14 301 48
-  let%span sfset35 = "../../../../creusot-contracts/src/logic/fset.rs" 232 33 232 38
-  let%span sfset36 = "../../../../creusot-contracts/src/logic/fset.rs" 231 14 231 45
-  let%span sghost37 = "../../../../creusot-contracts/src/ghost.rs" 181 15 181 16
-  let%span sghost38 = "../../../../creusot-contracts/src/ghost.rs" 181 4 181 28
-  let%span sghost39 = "../../../../creusot-contracts/src/ghost.rs" 179 14 179 28
-  let%span sfset40 = "../../../../creusot-contracts/src/logic/fset.rs" 65 8 65 26
-  let%span sresolve41 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
-  let%span sfset42 = "../../../../creusot-contracts/src/logic/fset.rs" 92 8 92 26
+  let%span sfset1 = "../../../../creusot-contracts/src/logic/fset.rs" 185 4 185 34
+  let%span sfset2 = "../../../../creusot-contracts/src/logic/fset.rs" 183 14 183 31
+  let%span sghost_set3 = "ghost_set.rs" 7 22 7 53
+  let%span sghost_set4 = "ghost_set.rs" 8 25 8 26
+  let%span sghost_set5 = "ghost_set.rs" 10 22 10 63
+  let%span sghost_set6 = "ghost_set.rs" 11 22 11 34
+  let%span sghost_set7 = "ghost_set.rs" 12 28 12 29
+  let%span sghost_set8 = "ghost_set.rs" 12 31 12 32
+  let%span sghost_set9 = "ghost_set.rs" 12 34 12 35
+  let%span sghost_set10 = "ghost_set.rs" 14 45 14 46
+  let%span sghost_set11 = "ghost_set.rs" 15 46 15 47
+  let%span sghost_set12 = "ghost_set.rs" 17 22 17 54
+  let%span sghost_set13 = "ghost_set.rs" 18 22 18 34
+  let%span sghost_set14 = "ghost_set.rs" 19 22 19 62
+  let%span sghost_set15 = "ghost_set.rs" 24 22 24 69
+  let%span sghost_set16 = "ghost_set.rs" 25 22 25 41
+  let%span sghost_set17 = "ghost_set.rs" 26 22 26 36
+  let%span sghost_set18 = "ghost_set.rs" 31 22 31 31
+  let%span sghost_set19 = "ghost_set.rs" 32 22 32 32
+  let%span sghost_set20 = "ghost_set.rs" 33 22 33 32
+  let%span sghost21 = "../../../../creusot-contracts/src/ghost.rs" 217 9 217 15
+  let%span sfset22 = "../../../../creusot-contracts/src/logic/fset.rs" 46 8 46 26
+  let%span sghost23 = "../../../../creusot-contracts/src/ghost.rs" 85 22 85 26
+  let%span sghost24 = "../../../../creusot-contracts/src/ghost.rs" 85 4 85 48
+  let%span sghost25 = "../../../../creusot-contracts/src/ghost.rs" 84 14 84 36
+  let%span sfset26 = "../../../../creusot-contracts/src/logic/fset.rs" 266 29 266 33
+  let%span sfset27 = "../../../../creusot-contracts/src/logic/fset.rs" 266 35 266 40
+  let%span sfset28 = "../../../../creusot-contracts/src/logic/fset.rs" 264 14 264 44
+  let%span sfset29 = "../../../../creusot-contracts/src/logic/fset.rs" 265 14 265 48
+  let%span sghost30 = "../../../../creusot-contracts/src/ghost.rs" 69 14 69 18
+  let%span sghost31 = "../../../../creusot-contracts/src/ghost.rs" 69 4 69 36
+  let%span sghost32 = "../../../../creusot-contracts/src/ghost.rs" 68 14 68 35
+  let%span sfset33 = "../../../../creusot-contracts/src/logic/fset.rs" 211 22 211 26
+  let%span sfset34 = "../../../../creusot-contracts/src/logic/fset.rs" 210 14 210 34
+  let%span sfset35 = "../../../../creusot-contracts/src/logic/fset.rs" 302 29 302 33
+  let%span sfset36 = "../../../../creusot-contracts/src/logic/fset.rs" 302 35 302 40
+  let%span sfset37 = "../../../../creusot-contracts/src/logic/fset.rs" 300 14 300 45
+  let%span sfset38 = "../../../../creusot-contracts/src/logic/fset.rs" 301 14 301 48
+  let%span sfset39 = "../../../../creusot-contracts/src/logic/fset.rs" 232 27 232 31
+  let%span sfset40 = "../../../../creusot-contracts/src/logic/fset.rs" 232 33 232 38
+  let%span sfset41 = "../../../../creusot-contracts/src/logic/fset.rs" 231 14 231 45
+  let%span sghost42 = "../../../../creusot-contracts/src/ghost.rs" 181 15 181 16
+  let%span sghost43 = "../../../../creusot-contracts/src/ghost.rs" 181 4 181 28
+  let%span sghost44 = "../../../../creusot-contracts/src/ghost.rs" 179 14 179 28
+  let%span sfset45 = "../../../../creusot-contracts/src/logic/fset.rs" 65 8 65 26
+  let%span sresolve46 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
+  let%span sfset47 = "../../../../creusot-contracts/src/logic/fset.rs" 92 8 92 26
   
   use prelude.prelude.Int32
   
@@ -50,13 +55,19 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18]
   type t_GhostBox'0  =
     { t_GhostBox__0'0: Fset.fset int32 }
   
+  predicate inv'0 (_1 : t_GhostBox'0)
+  
+  axiom inv_axiom'0 [@rewrite] : forall x : t_GhostBox'0 [inv'0 x] . inv'0 x = true
+  
   function inner_logic'0 (self : t_GhostBox'0) : Fset.fset int32 =
-    [%#sghost20] self.t_GhostBox__0'0
+    [%#sghost21] self.t_GhostBox__0'0
   
   use set.Fset
   
   let rec new'0 (_1:()) (return'  (ret:t_GhostBox'0))= any
-    [ return' (result:t_GhostBox'0)-> {[%#sfset1] Fset.is_empty (inner_logic'0 result)} (! return' {result}) ]
+    [ return' (result:t_GhostBox'0)-> {[%#sfset1] inv'0 result}
+      {[%#sfset2] Fset.is_empty (inner_logic'0 result)}
+      (! return' {result}) ]
     
   
   use prelude.prelude.Borrow
@@ -64,58 +75,59 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18]
   use set.Fset
   
   predicate contains'0 [@inline:trivial] (self : Fset.fset int32) (e : int32) =
-    [%#sfset21] Fset.mem e self
+    [%#sfset22] Fset.mem e self
   
-  predicate inv'0 (_1 : borrowed (t_GhostBox'0))
+  predicate inv'1 (_1 : borrowed (t_GhostBox'0))
   
-  axiom inv_axiom'0 [@rewrite] : forall x : borrowed (t_GhostBox'0) [inv'0 x] . inv'0 x = true
+  axiom inv_axiom'1 [@rewrite] : forall x : borrowed (t_GhostBox'0) [inv'1 x] . inv'1 x = true
   
-  predicate inv'1 (_1 : borrowed (Fset.fset int32))
+  predicate inv'2 (_1 : borrowed (Fset.fset int32))
   
-  axiom inv_axiom'1 [@rewrite] : forall x : borrowed (Fset.fset int32) [inv'1 x] . inv'1 x = true
+  axiom inv_axiom'2 [@rewrite] : forall x : borrowed (Fset.fset int32) [inv'2 x] . inv'2 x = true
   
-  let rec deref_mut'0 (self:borrowed (t_GhostBox'0)) (return'  (ret:borrowed (Fset.fset int32)))= {[@expl:deref_mut 'self' type invariant] [%#sghost22] inv'0 self}
+  let rec deref_mut'0 (self:borrowed (t_GhostBox'0)) (return'  (ret:borrowed (Fset.fset int32)))= {[@expl:deref_mut 'self' type invariant] [%#sghost23] inv'1 self}
     any
-    [ return' (result:borrowed (Fset.fset int32))-> {[%#sghost23] inv'1 result}
-      {[%#sghost24] result
+    [ return' (result:borrowed (Fset.fset int32))-> {[%#sghost24] inv'2 result}
+      {[%#sghost25] result
       = Borrow.borrow_logic (self.current).t_GhostBox__0'0 (self.final).t_GhostBox__0'0 (Borrow.inherit_id (Borrow.get_id self) 1)}
       (! return' {result}) ]
     
   
-  predicate inv'2 (_1 : int32)
+  predicate inv'3 (_1 : int32)
   
-  axiom inv_axiom'2 [@rewrite] : forall x : int32 [inv'2 x] . inv'2 x = true
+  axiom inv_axiom'3 [@rewrite] : forall x : int32 [inv'3 x] . inv'3 x = true
   
   use set.Fset
   
   function insert'0 [@inline:trivial] (self : Fset.fset int32) (e : int32) : Fset.fset int32 =
-    [%#sfset40] Fset.add e self
+    [%#sfset45] Fset.add e self
   
-  let rec insert_ghost'0 (self:borrowed (Fset.fset int32)) (value:int32) (return'  (ret:bool))= {[@expl:insert_ghost 'value' type invariant] [%#sfset25] inv'2 value}
+  let rec insert_ghost'0 (self:borrowed (Fset.fset int32)) (value:int32) (return'  (ret:bool))= {[@expl:insert_ghost 'self' type invariant] [%#sfset26] inv'2 self}
+    {[@expl:insert_ghost 'value' type invariant] [%#sfset27] inv'3 value}
     any
-    [ return' (result:bool)-> {[%#sfset26] self.final = insert'0 self.current value}
-      {[%#sfset27] result = (not contains'0 self.current value)}
+    [ return' (result:bool)-> {[%#sfset28] self.final = insert'0 self.current value}
+      {[%#sfset29] result = (not contains'0 self.current value)}
       (! return' {result}) ]
     
   
   predicate resolve'2 (self : borrowed (Fset.fset int32)) =
-    [%#sresolve41] self.final = self.current
+    [%#sresolve46] self.final = self.current
   
   predicate resolve'0 (_1 : borrowed (Fset.fset int32)) =
     resolve'2 _1
   
-  predicate inv'3 (_1 : t_GhostBox'0)
+  predicate inv'4 (_1 : t_GhostBox'0)
   
-  axiom inv_axiom'3 [@rewrite] : forall x : t_GhostBox'0 [inv'3 x] . inv'3 x = true
+  axiom inv_axiom'4 [@rewrite] : forall x : t_GhostBox'0 [inv'4 x] . inv'4 x = true
   
-  predicate inv'4 (_1 : Fset.fset int32)
+  predicate inv'5 (_1 : Fset.fset int32)
   
-  axiom inv_axiom'4 [@rewrite] : forall x : Fset.fset int32 [inv'4 x] . inv'4 x = true
+  axiom inv_axiom'5 [@rewrite] : forall x : Fset.fset int32 [inv'5 x] . inv'5 x = true
   
-  let rec deref'0 (self:t_GhostBox'0) (return'  (ret:Fset.fset int32))= {[@expl:deref 'self' type invariant] [%#sghost28] inv'3 self}
+  let rec deref'0 (self:t_GhostBox'0) (return'  (ret:Fset.fset int32))= {[@expl:deref 'self' type invariant] [%#sghost30] inv'4 self}
     any
-    [ return' (result:Fset.fset int32)-> {[%#sghost29] inv'4 result}
-      {[%#sghost30] self.t_GhostBox__0'0 = result}
+    [ return' (result:Fset.fset int32)-> {[%#sghost31] inv'5 result}
+      {[%#sghost32] self.t_GhostBox__0'0 = result}
       (! return' {result}) ]
     
   
@@ -123,34 +135,35 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18]
   
   use prelude.prelude.Int
   
-  let rec len_ghost'0 (self:Fset.fset int32) (return'  (ret:int))= any
-    [ return' (result:int)-> {[%#sfset31] result = Fset.cardinal self} (! return' {result}) ]
-    
+  let rec len_ghost'0 (self:Fset.fset int32) (return'  (ret:int))= {[@expl:len_ghost 'self' type invariant] [%#sfset33] inv'5 self}
+    any [ return' (result:int)-> {[%#sfset34] result = Fset.cardinal self} (! return' {result}) ] 
   
-  predicate inv'5 (_1 : int32)
+  predicate inv'6 (_1 : int32)
   
-  axiom inv_axiom'5 [@rewrite] : forall x : int32 [inv'5 x] . inv'5 x = true
+  axiom inv_axiom'6 [@rewrite] : forall x : int32 [inv'6 x] . inv'6 x = true
   
   use set.Fset
   
   function remove'0 [@inline:trivial] (self : Fset.fset int32) (e : int32) : Fset.fset int32 =
-    [%#sfset42] Fset.remove e self
+    [%#sfset47] Fset.remove e self
   
-  let rec remove_ghost'0 (self:borrowed (Fset.fset int32)) (value:int32) (return'  (ret:bool))= {[@expl:remove_ghost 'value' type invariant] [%#sfset32] inv'5 value}
+  let rec remove_ghost'0 (self:borrowed (Fset.fset int32)) (value:int32) (return'  (ret:bool))= {[@expl:remove_ghost 'self' type invariant] [%#sfset35] inv'2 self}
+    {[@expl:remove_ghost 'value' type invariant] [%#sfset36] inv'6 value}
     any
-    [ return' (result:bool)-> {[%#sfset33] self.final = remove'0 self.current value}
-      {[%#sfset34] result = contains'0 self.current value}
+    [ return' (result:bool)-> {[%#sfset37] self.final = remove'0 self.current value}
+      {[%#sfset38] result = contains'0 self.current value}
       (! return' {result}) ]
     
   
-  let rec contains_ghost'0 (self:Fset.fset int32) (value:int32) (return'  (ret:bool))= {[@expl:contains_ghost 'value' type invariant] [%#sfset35] inv'5 value}
-    any [ return' (result:bool)-> {[%#sfset36] result = contains'0 self value} (! return' {result}) ] 
+  let rec contains_ghost'0 (self:Fset.fset int32) (value:int32) (return'  (ret:bool))= {[@expl:contains_ghost 'self' type invariant] [%#sfset39] inv'5 self}
+    {[@expl:contains_ghost 'value' type invariant] [%#sfset40] inv'6 value}
+    any [ return' (result:bool)-> {[%#sfset41] result = contains'0 self value} (! return' {result}) ] 
   
   type closure0'1  =
     { field_0'0: borrowed (t_GhostBox'0) }
   
   predicate resolve'4 (self : borrowed (t_GhostBox'0)) =
-    [%#sresolve41] self.final = self.current
+    [%#sresolve46] self.final = self.current
   
   predicate resolve'3 (_1 : borrowed (t_GhostBox'0)) =
     resolve'4 _1
@@ -158,21 +171,21 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18]
   predicate resolve'1 (_1 : closure0'1) =
     resolve'3 _1.field_0'0
   
-  predicate inv'6 (_1 : ())
+  predicate inv'7 (_1 : ())
   
-  axiom inv_axiom'6 [@rewrite] : forall x : () [inv'6 x] . inv'6 x = true
+  axiom inv_axiom'7 [@rewrite] : forall x : () [inv'7 x] . inv'7 x = true
   
   type t_GhostBox'1  =
     { t_GhostBox__0'1: () }
   
-  predicate inv'7 (_1 : t_GhostBox'1)
+  predicate inv'8 (_1 : t_GhostBox'1)
   
-  axiom inv_axiom'7 [@rewrite] : forall x : t_GhostBox'1 [inv'7 x] . inv'7 x = true
+  axiom inv_axiom'8 [@rewrite] : forall x : t_GhostBox'1 [inv'8 x] . inv'8 x = true
   
-  let rec new'1 (x:()) (return'  (ret:t_GhostBox'1))= {[@expl:new 'x' type invariant] [%#sghost37] inv'6 x}
+  let rec new'1 (x:()) (return'  (ret:t_GhostBox'1))= {[@expl:new 'x' type invariant] [%#sghost42] inv'7 x}
     any
-    [ return' (result:t_GhostBox'1)-> {[%#sghost38] inv'7 result}
-      {[%#sghost39] result.t_GhostBox__0'1 = x}
+    [ return' (result:t_GhostBox'1)-> {[%#sghost43] inv'8 result}
+      {[%#sghost44] result.t_GhostBox__0'1 = x}
       (! return' {result}) ]
     
   
@@ -180,7 +193,7 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18]
   
   let rec closure0'0 (_1:closure0'1) (return'  (ret:t_GhostBox'1))= bb0
     [ bb0 = s0
-      [ s0 = {[@expl:assertion] [%#sghost_set2] forall k : int32 . not contains'0 (inner_logic'0 (_1.field_0'0).current) k}
+      [ s0 = {[@expl:assertion] [%#sghost_set3] forall k : int32 . not contains'0 (inner_logic'0 (_1.field_0'0).current) k}
         s1
       | s1 = Borrow.borrow_mut <t_GhostBox'0> {(_1.field_0'0).current}
           (fun (_ret':borrowed (t_GhostBox'0)) ->
@@ -193,7 +206,7 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18]
     | bb1 = s0
       [ s0 = Borrow.borrow_final <Fset.fset int32> {_7.current} {Borrow.get_id _7}
           (fun (_ret':borrowed (Fset.fset int32)) ->  [ &_6 <- _ret' ]  [ &_7 <- { _7 with current = _ret'.final } ] s1)
-      | s1 = insert_ghost'0 {_6} {[%#sghost_set3] (1 : int32)} (fun (_ret':bool) ->  [ &_5 <- _ret' ] s2)
+      | s1 = insert_ghost'0 {_6} {[%#sghost_set4] (1 : int32)} (fun (_ret':bool) ->  [ &_5 <- _ret' ] s2)
       | s2 = bb2 ]
       
     | bb2 = s0
@@ -203,11 +216,11 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18]
       
     | bb3 = s0 [ s0 = len_ghost'0 {_11} (fun (_ret':int) ->  [ &length1 <- _ret' ] s1) | s1 = bb4 ] 
     | bb4 = s0
-      [ s0 = {[@expl:assertion] [%#sghost_set4] contains'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32)
+      [ s0 = {[@expl:assertion] [%#sghost_set5] contains'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32)
         /\ not contains'0 (inner_logic'0 (_1.field_0'0).current) (2 : int32)}
         s1
-      | s1 = {[@expl:assertion] [%#sghost_set5] length1 = 1} s2
-      | s2 =  [ &_20 <- (([%#sghost_set6] (1 : int32)), ([%#sghost_set7] (2 : int32)), ([%#sghost_set8] (3 : int32))) ] 
+      | s1 = {[@expl:assertion] [%#sghost_set6] length1 = 1} s2
+      | s2 =  [ &_20 <- (([%#sghost_set7] (1 : int32)), ([%#sghost_set8] (2 : int32)), ([%#sghost_set9] (3 : int32))) ] 
         s3
       | s3 =  [ &x1 <- let (r'0, _, _) = _20 in r'0 ] s4
       | s4 =  [ &x2 <- let (_, r'1, _) = _20 in r'1 ] s5
@@ -226,7 +239,7 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18]
              [ &_22 <- _ret' ] 
              [ &_23 <- { _23 with current = _ret'.final } ] 
             s1)
-      | s1 = insert_ghost'0 {_22} {[%#sghost_set9] (2 : int32)} (fun (_ret':bool) ->  [ &inserted_true <- _ret' ] s2)
+      | s1 = insert_ghost'0 {_22} {[%#sghost_set10] (2 : int32)} (fun (_ret':bool) ->  [ &inserted_true <- _ret' ] s2)
       | s2 = bb6 ]
       
     | bb6 = s0
@@ -245,7 +258,7 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18]
              [ &_26 <- _ret' ] 
              [ &_27 <- { _27 with current = _ret'.final } ] 
             s1)
-      | s1 = insert_ghost'0 {_26} {[%#sghost_set10] (2 : int32)} (fun (_ret':bool) ->  [ &inserted_false <- _ret' ] s2)
+      | s1 = insert_ghost'0 {_26} {[%#sghost_set11] (2 : int32)} (fun (_ret':bool) ->  [ &inserted_false <- _ret' ] s2)
       | s2 = bb8 ]
       
     | bb8 = s0
@@ -255,9 +268,9 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18]
       
     | bb9 = s0 [ s0 = len_ghost'0 {_31} (fun (_ret':int) ->  [ &length2 <- _ret' ] s1) | s1 = bb10 ] 
     | bb10 = s0
-      [ s0 = {[@expl:assertion] [%#sghost_set11] inserted_true /\ not inserted_false} s1
-      | s1 = {[@expl:assertion] [%#sghost_set12] length2 = 2} s2
-      | s2 = {[@expl:assertion] [%#sghost_set13] contains'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32)
+      [ s0 = {[@expl:assertion] [%#sghost_set12] inserted_true /\ not inserted_false} s1
+      | s1 = {[@expl:assertion] [%#sghost_set13] length2 = 2} s2
+      | s2 = {[@expl:assertion] [%#sghost_set14] contains'0 (inner_logic'0 (_1.field_0'0).current) (1 : int32)
         /\ contains'0 (inner_logic'0 (_1.field_0'0).current) (2 : int32)}
         s3
       | s3 = Borrow.borrow_mut <t_GhostBox'0> {(_1.field_0'0).current}
@@ -320,9 +333,9 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18]
       
     | bb16 = s0
       [ s0 = -{resolve'0 _53}- s1
-      | s1 = {[@expl:assertion] [%#sghost_set14] not remove_false1 /\ remove_true /\ not remove_false2} s2
-      | s2 = {[@expl:assertion] [%#sghost_set15] not contains'0 (inner_logic'0 (_1.field_0'0).current) (2 : int32)} s3
-      | s3 = {[@expl:assertion] [%#sghost_set16] Fset.cardinal (inner_logic'0 (_1.field_0'0).current) = 1} s4
+      | s1 = {[@expl:assertion] [%#sghost_set15] not remove_false1 /\ remove_true /\ not remove_false2} s2
+      | s2 = {[@expl:assertion] [%#sghost_set16] not contains'0 (inner_logic'0 (_1.field_0'0).current) (2 : int32)} s3
+      | s3 = {[@expl:assertion] [%#sghost_set17] Fset.cardinal (inner_logic'0 (_1.field_0'0).current) = 1} s4
       | s4 = deref'0 {(_1.field_0'0).current} (fun (_ret':Fset.fset int32) ->  [ &_65 <- _ret' ] s5)
       | s5 = bb17 ]
       
@@ -349,9 +362,9 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18]
       
     | bb22 = s0
       [ s0 = -{resolve'1 _1}- s1
-      | s1 = {[@expl:assertion] [%#sghost_set17] contains1} s2
-      | s2 = {[@expl:assertion] [%#sghost_set18] not contains2} s3
-      | s3 = {[@expl:assertion] [%#sghost_set19] not contains3} s4
+      | s1 = {[@expl:assertion] [%#sghost_set18] contains1} s2
+      | s2 = {[@expl:assertion] [%#sghost_set19] not contains2} s3
+      | s3 = {[@expl:assertion] [%#sghost_set20] not contains3} s4
       | s4 = new'1 {_2} (fun (_ret':t_GhostBox'1) ->  [ &_0 <- _ret' ] s5)
       | s5 = bb23 ]
       
diff --git a/creusot/tests/should_succeed/ghost/ghost_set/why3session.xml b/creusot/tests/should_succeed/ghost/ghost_set/why3session.xml
index cbca4290d..f7c485e07 100644
--- a/creusot/tests/should_succeed/ghost/ghost_set/why3session.xml
+++ b/creusot/tests/should_succeed/ghost/ghost_set/why3session.xml
@@ -2,12 +2,12 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "https://www.why3.org/why3session.dtd">
 <why3session shape_version="6">
-<prover id="0" name="CVC4" version="1.8" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="1" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <file format="coma" proved="true">
 <path name=".."/><path name="ghost_set.coma"/>
 <theory name="M_ghost_set__ghost_map" proved="true">
  <goal name="vc_ghost_map&#39;0" proved="true">
- <proof prover="0"><result status="valid" time="0.083601" steps="33312"/></proof>
+ <proof prover="1"><result status="valid" time="0.251525" steps="28055"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/creusot/tests/should_succeed/ghost/ghost_set/why3shapes.gz b/creusot/tests/should_succeed/ghost/ghost_set/why3shapes.gz
index ee3c4c000..55a9638a9 100644
Binary files a/creusot/tests/should_succeed/ghost/ghost_set/why3shapes.gz and b/creusot/tests/should_succeed/ghost/ghost_set/why3shapes.gz differ
diff --git a/creusot/tests/should_succeed/hashmap.coma b/creusot/tests/should_succeed/hashmap.coma
index 7cb911505..b1f13ef05 100644
--- a/creusot/tests/should_succeed/hashmap.coma
+++ b/creusot/tests/should_succeed/hashmap.coma
@@ -136,7 +136,7 @@ module M_hashmap__qyi15467499327297494705__resolve_coherence [#"hashmap.rs" 116
   let%span shashmap16 = "hashmap.rs" 133 12 133 91
   let%span shashmap17 = "hashmap.rs" 41 12 44 13
   let%span svec18 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
-  let%span sseq19 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq19 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed20 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
@@ -348,7 +348,7 @@ module M_hashmap__qyi7664122466964245986__new [#"hashmap.rs" 152 4 152 46] (* My
   let%span shashmap13 = "hashmap.rs" 133 12 133 91
   let%span shashmap14 = "hashmap.rs" 41 12 44 13
   let%span sboxed15 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
-  let%span sseq16 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq16 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   
   type t_K'0
   
@@ -575,7 +575,7 @@ module M_hashmap__qyi7664122466964245986__add [#"hashmap.rs" 158 4 158 41] (* My
   let%span sindex41 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span sinvariant42 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
   let%span sresolve43 = "../../../creusot-contracts/src/resolve.rs" 82 8 85 9
-  let%span sseq44 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq44 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span shashmap45 = "hashmap.rs" 143 12 144 139
   
   use prelude.prelude.Snapshot
@@ -1152,7 +1152,7 @@ module M_hashmap__qyi7664122466964245986__get [#"hashmap.rs" 190 4 190 43] (* My
   let%span shashmap26 = "hashmap.rs" 133 12 133 91
   let%span shashmap27 = "hashmap.rs" 41 12 44 13
   let%span sboxed28 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
-  let%span sseq29 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq29 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   
   use prelude.prelude.Borrow
   
@@ -1534,7 +1534,7 @@ module M_hashmap__qyi7664122466964245986__resize [#"hashmap.rs" 209 4 209 24] (*
   let%span sinvariant57 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
   let%span sresolve58 = "../../../creusot-contracts/src/resolve.rs" 82 8 85 9
   let%span sboxed59 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
-  let%span sseq60 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq60 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   
   use prelude.prelude.Snapshot
   
@@ -2508,7 +2508,7 @@ module M_hashmap__qyi15467499327297494705__resolve_coherence__refines [#"hashmap
   let%span shashmap13 = "hashmap.rs" 133 12 133 91
   let%span shashmap14 = "hashmap.rs" 41 12 44 13
   let%span svec15 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
-  let%span sseq16 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq16 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed17 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
diff --git a/creusot/tests/should_succeed/heapsort_generic.coma b/creusot/tests/should_succeed/heapsort_generic.coma
index 241a95d98..3b2ecf33f 100644
--- a/creusot/tests/should_succeed/heapsort_generic.coma
+++ b/creusot/tests/should_succeed/heapsort_generic.coma
@@ -176,7 +176,7 @@ module M_heapsort_generic__sift_down [#"heapsort_generic.rs" 41 0 43 29]
   let%span svec63 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sslice64 = "../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
   let%span sinvariant65 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
-  let%span sseq66 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq66 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed67 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Snapshot
@@ -689,7 +689,7 @@ module M_heapsort_generic__heap_sort [#"heapsort_generic.rs" 94 0 96 29]
   let%span sinvariant72 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sslice73 = "../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
   let%span sinvariant74 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
-  let%span sseq75 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq75 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed76 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Snapshot
diff --git a/creusot/tests/should_succeed/hillel.coma b/creusot/tests/should_succeed/hillel.coma
index 5d8605759..7aebfd4e4 100644
--- a/creusot/tests/should_succeed/hillel.coma
+++ b/creusot/tests/should_succeed/hillel.coma
@@ -24,7 +24,7 @@ module M_hillel__right_pad [#"hillel.rs" 17 0 17 59]
   let%span svec22 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sinvariant23 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sinvariant24 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
-  let%span sseq25 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq25 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed26 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Snapshot
@@ -243,7 +243,7 @@ module M_hillel__left_pad [#"hillel.rs" 34 0 34 58]
   let%span svec27 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sinvariant28 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sinvariant29 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
-  let%span sseq30 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq30 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed31 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Snapshot
@@ -534,7 +534,7 @@ module M_hillel__insert_unique [#"hillel.rs" 80 0 80 62]
   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 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 sseq55 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 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
   let%span sinvariant58 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
@@ -1055,7 +1055,7 @@ module M_hillel__unique [#"hillel.rs" 102 0 102 56]
   let%span svec56 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sinvariant57 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sinvariant58 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
-  let%span sseq59 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq59 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sslice60 = "../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
   let%span sboxed61 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
diff --git a/creusot/tests/should_succeed/iterators/02_iter_mut.coma b/creusot/tests/should_succeed/iterators/02_iter_mut.coma
index dddc58149..d2286803d 100644
--- a/creusot/tests/should_succeed/iterators/02_iter_mut.coma
+++ b/creusot/tests/should_succeed/iterators/02_iter_mut.coma
@@ -227,7 +227,7 @@ module M_02_iter_mut__qyi4305820612590367313__next [#"02_iter_mut.rs" 64 4 64 44
   let%span sinvariant14 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sslice15 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
   let%span s02_iter_mut16 = "02_iter_mut.rs" 23 20 23 64
-  let%span sseq17 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq17 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed18 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
@@ -456,7 +456,7 @@ module M_02_iter_mut__qyi7060081090368749043__into_iter [#"02_iter_mut.rs" 71 4
   let%span sslice5 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
   let%span sinvariant6 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sslice7 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
-  let%span sseq8 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq8 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed9 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
@@ -568,7 +568,7 @@ module M_02_iter_mut__iter_mut [#"02_iter_mut.rs" 79 0 79 55]
   let%span sslice19 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
   let%span sinvariant20 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span s02_iter_mut21 = "02_iter_mut.rs" 23 20 23 64
-  let%span sseq22 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq22 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed23 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
@@ -1129,7 +1129,7 @@ module M_02_iter_mut__qyi9908912287408438076__resolve_coherence__refines [#"02_i
   let%span sslice6 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
   let%span sinvariant7 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sslice8 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
-  let%span sseq9 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq9 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed10 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
@@ -1322,7 +1322,7 @@ module M_02_iter_mut__qyi4305820612590367313__next__refines [#"02_iter_mut.rs" 6
   let%span sindex10 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31
   let%span s02_iter_mut11 = "02_iter_mut.rs" 23 20 23 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
+  let%span sseq13 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed14 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
diff --git a/creusot/tests/should_succeed/iterators/03_std_iterators.coma b/creusot/tests/should_succeed/iterators/03_std_iterators.coma
index 8fb0ee8f3..7b532d253 100644
--- a/creusot/tests/should_succeed/iterators/03_std_iterators.coma
+++ b/creusot/tests/should_succeed/iterators/03_std_iterators.coma
@@ -29,7 +29,7 @@ module M_03_std_iterators__slice_iter [#"03_std_iterators.rs" 6 0 6 42]
   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 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 sseq30 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 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
   let%span sboxed33 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
@@ -340,7 +340,7 @@ module M_03_std_iterators__vec_iter [#"03_std_iterators.rs" 17 0 17 41]
   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 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 sseq28 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 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
   let%span sslice31 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
@@ -2287,7 +2287,7 @@ module M_03_std_iterators__my_reverse [#"03_std_iterators.rs" 94 0 94 37]
   let%span sslice54 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
   let%span sinvariant55 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sinvariant56 = "../../../../creusot-contracts/src/invariant.rs" 24 8 24 18
-  let%span sseq57 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq57 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed58 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
diff --git a/creusot/tests/should_succeed/iterators/08_collect_extend.coma b/creusot/tests/should_succeed/iterators/08_collect_extend.coma
index 023e1bffa..3e47177b0 100644
--- a/creusot/tests/should_succeed/iterators/08_collect_extend.coma
+++ b/creusot/tests/should_succeed/iterators/08_collect_extend.coma
@@ -24,7 +24,7 @@ module M_08_collect_extend__extend [#"08_collect_extend.rs" 26 0 26 66]
   let%span siter22 = "../../../../creusot-contracts/src/std/iter.rs" 44 14 44 42
   let%span sresolve23 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   let%span sinvariant24 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
-  let%span sseq25 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq25 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span svec26 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sboxed27 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
@@ -345,7 +345,7 @@ module M_08_collect_extend__collect [#"08_collect_extend.rs" 44 0 44 52]
   let%span sresolve21 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   let%span smodel22 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22
   let%span svec23 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
-  let%span sseq24 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq24 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sinvariant25 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sboxed26 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
diff --git a/creusot/tests/should_succeed/knapsack.coma b/creusot/tests/should_succeed/knapsack.coma
index fb5f3e65a..e4f12d799 100644
--- a/creusot/tests/should_succeed/knapsack.coma
+++ b/creusot/tests/should_succeed/knapsack.coma
@@ -146,7 +146,7 @@ module M_knapsack__knapsack01_dyn [#"knapsack.rs" 49 0 49 91]
   let%span svec55 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sinvariant56 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
   let%span sinvariant57 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
-  let%span sseq58 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq58 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed59 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.UIntSize
diff --git a/creusot/tests/should_succeed/knapsack_full.coma b/creusot/tests/should_succeed/knapsack_full.coma
index 8030b62c4..70ab1200a 100644
--- a/creusot/tests/should_succeed/knapsack_full.coma
+++ b/creusot/tests/should_succeed/knapsack_full.coma
@@ -408,7 +408,7 @@ module M_knapsack_full__knapsack01_dyn [#"knapsack_full.rs" 86 0 86 91]
   let%span svec103 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sinvariant104 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
   let%span sinvariant105 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
-  let%span sseq106 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq106 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed107 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.UIntSize
diff --git a/creusot/tests/should_succeed/linked_list.coma b/creusot/tests/should_succeed/linked_list.coma
index fd457fb8e..484004290 100644
--- a/creusot/tests/should_succeed/linked_list.coma
+++ b/creusot/tests/should_succeed/linked_list.coma
@@ -14,7 +14,7 @@ module M_linked_list__qyi14323471455460008969__new [#"linked_list.rs" 72 4 72 27
   let%span slinked_list12 = "linked_list.rs" 67 4 67 41
   let%span slinked_list13 = "linked_list.rs" 26 12 36 69
   let%span sboxed14 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
-  let%span sseq15 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq15 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sptr_own16 = "../../../creusot-contracts/src/ptr_own.rs" 44 20 44 66
   
   use prelude.prelude.Opaque
@@ -239,7 +239,7 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
   let%span sinvariant50 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sseq51 = "../../../creusot-contracts/src/logic/seq.rs" 80 4 80 12
   let%span sboxed52 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
-  let%span sseq53 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq53 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sresolve54 = "../../../creusot-contracts/src/resolve.rs" 68 8 68 23
   let%span sptr_own55 = "../../../creusot-contracts/src/ptr_own.rs" 44 20 44 66
   let%span sinvariant56 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
@@ -986,7 +986,7 @@ module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 100
   let%span sresolve28 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   let%span slinked_list29 = "linked_list.rs" 67 4 67 41
   let%span sinvariant30 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
-  let%span sseq31 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq31 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sresolve32 = "../../../creusot-contracts/src/resolve.rs" 68 8 68 23
   let%span sboxed33 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   let%span sptr_own34 = "../../../creusot-contracts/src/ptr_own.rs" 44 20 44 66
diff --git a/creusot/tests/should_succeed/selection_sort_generic.coma b/creusot/tests/should_succeed/selection_sort_generic.coma
index 64810d5c6..7a5adc59a 100644
--- a/creusot/tests/should_succeed/selection_sort_generic.coma
+++ b/creusot/tests/should_succeed/selection_sort_generic.coma
@@ -74,7 +74,7 @@ module M_selection_sort_generic__selection_sort [#"selection_sort_generic.rs" 30
   let%span sslice72 = "../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
   let%span sinvariant73 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sinvariant74 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
-  let%span sseq75 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq75 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed76 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Snapshot
diff --git a/creusot/tests/should_succeed/slices/01.coma b/creusot/tests/should_succeed/slices/01.coma
index 3e1c6156f..7460fc368 100644
--- a/creusot/tests/should_succeed/slices/01.coma
+++ b/creusot/tests/should_succeed/slices/01.coma
@@ -157,7 +157,7 @@ module M_01__slice_first [#"01.rs" 20 0 20 44]
   let%span sslice10 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42
   let%span sinvariant11 = "../../../../creusot-contracts/src/invariant.rs" 24 8 24 18
   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
+  let%span sseq13 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed14 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
diff --git a/creusot/tests/should_succeed/sparse_array.coma b/creusot/tests/should_succeed/sparse_array.coma
index f321f913a..ec0da28f4 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__qyi13879026616235705248__resolve_coherence [#"sparse_arra
   let%span svec11 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span ssparse_array12 = "sparse_array.rs" 68 12 76 17
   let%span svec13 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
-  let%span sseq14 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq14 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed15 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
@@ -227,7 +227,7 @@ module M_sparse_array__qyi912363311032332466__get [#"sparse_array.rs" 105 4 105
   let%span sindex14 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span ssparse_array15 = "sparse_array.rs" 68 12 76 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
+  let%span sseq17 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed18 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.UIntSize
@@ -514,7 +514,7 @@ module M_sparse_array__qyi912363311032332466__lemma_permutation [#"sparse_array.
   let%span ssparse_array7 = "sparse_array.rs" 68 12 76 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
-  let%span sseq10 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq10 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed11 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.UIntSize
@@ -681,7 +681,7 @@ module M_sparse_array__qyi912363311032332466__set [#"sparse_array.rs" 129 4 129
   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" 68 12 76 17
-  let%span sseq34 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq34 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed35 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
@@ -1098,7 +1098,7 @@ module M_sparse_array__create [#"sparse_array.rs" 151 0 151 56]
   let%span ssparse_array12 = "sparse_array.rs" 89 20 90 52
   let%span ssparse_array13 = "sparse_array.rs" 68 12 76 17
   let%span svec14 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
-  let%span sseq15 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq15 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed16 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   type t_T'0
@@ -1679,7 +1679,7 @@ module M_sparse_array__qyi13879026616235705248__resolve_coherence__refines [#"sp
   let%span svec8 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span ssparse_array9 = "sparse_array.rs" 68 12 76 17
   let%span svec10 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
-  let%span sseq11 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq11 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed12 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
diff --git a/creusot/tests/should_succeed/take_first_mut.coma b/creusot/tests/should_succeed/take_first_mut.coma
index ff4c89567..c7b349603 100644
--- a/creusot/tests/should_succeed/take_first_mut.coma
+++ b/creusot/tests/should_succeed/take_first_mut.coma
@@ -14,7 +14,7 @@ module M_take_first_mut__take_first_mut [#"take_first_mut.rs" 14 0 14 74]
   let%span sresolve12 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   let%span sinvariant13 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sslice14 = "../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
-  let%span sseq15 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq15 = "../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed16 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
diff --git a/creusot/tests/should_succeed/traits/16_impl_cloning.coma b/creusot/tests/should_succeed/traits/16_impl_cloning.coma
index 740b86e61..f33c99265 100644
--- a/creusot/tests/should_succeed/traits/16_impl_cloning.coma
+++ b/creusot/tests/should_succeed/traits/16_impl_cloning.coma
@@ -6,7 +6,7 @@ module M_16_impl_cloning__test [#"16_impl_cloning.rs" 16 0 16 30]
   let%span sinvariant4 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span svec5 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span svec6 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span sseq7 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq7 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed8 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
diff --git a/creusot/tests/should_succeed/type_invariants/vec_inv.coma b/creusot/tests/should_succeed/type_invariants/vec_inv.coma
index 6f47f35f8..9f3950339 100644
--- a/creusot/tests/should_succeed/type_invariants/vec_inv.coma
+++ b/creusot/tests/should_succeed/type_invariants/vec_inv.coma
@@ -7,7 +7,7 @@ module M_vec_inv__vec [#"vec_inv.rs" 18 0 18 32]
   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
   let%span sresolve7 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
-  let%span sseq8 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq8 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed9 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   let%span sinvariant10 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span svec_inv11 = "vec_inv.rs" 13 20 13 43
diff --git a/creusot/tests/should_succeed/vector/02_gnome.coma b/creusot/tests/should_succeed/vector/02_gnome.coma
index 652efa037..c08b5a218 100644
--- a/creusot/tests/should_succeed/vector/02_gnome.coma
+++ b/creusot/tests/should_succeed/vector/02_gnome.coma
@@ -54,7 +54,7 @@ module M_02_gnome__gnome_sort [#"02_gnome.rs" 22 0 24 29]
   let%span sslice52 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
   let%span sinvariant53 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sinvariant54 = "../../../../creusot-contracts/src/invariant.rs" 24 8 24 18
-  let%span sseq55 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq55 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed56 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Snapshot
diff --git a/creusot/tests/should_succeed/vector/03_knuth_shuffle.coma b/creusot/tests/should_succeed/vector/03_knuth_shuffle.coma
index 63c4c17d2..aa5094ddc 100644
--- a/creusot/tests/should_succeed/vector/03_knuth_shuffle.coma
+++ b/creusot/tests/should_succeed/vector/03_knuth_shuffle.coma
@@ -41,7 +41,7 @@ module M_03_knuth_shuffle__knuth_shuffle [#"03_knuth_shuffle.rs" 13 0 13 39]
   let%span sslice39 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30
   let%span sinvariant40 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   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 sseq42 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed43 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Snapshot
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 ded10f9d3..a012a5535 100644
--- a/creusot/tests/should_succeed/vector/05_binary_search_generic.coma
+++ b/creusot/tests/should_succeed/vector/05_binary_search_generic.coma
@@ -46,7 +46,7 @@ module M_05_binary_search_generic__binary_search [#"05_binary_search_generic.rs"
   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
+  let%span sseq47 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed48 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
diff --git a/creusot/tests/should_succeed/vector/07_read_write.coma b/creusot/tests/should_succeed/vector/07_read_write.coma
index 41aa7f9cc..c2fd7c3f5 100644
--- a/creusot/tests/should_succeed/vector/07_read_write.coma
+++ b/creusot/tests/should_succeed/vector/07_read_write.coma
@@ -22,7 +22,7 @@ module M_07_read_write__read_write [#"07_read_write.rs" 6 0 6 75]
   let%span svec20 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sinvariant21 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sinvariant22 = "../../../../creusot-contracts/src/invariant.rs" 24 8 24 18
-  let%span sseq23 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq23 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed24 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
diff --git a/creusot/tests/should_succeed/vector/09_capacity.coma b/creusot/tests/should_succeed/vector/09_capacity.coma
index 280ba8d6c..4defb97dd 100644
--- a/creusot/tests/should_succeed/vector/09_capacity.coma
+++ b/creusot/tests/should_succeed/vector/09_capacity.coma
@@ -15,7 +15,7 @@ module M_09_capacity__change_capacity [#"09_capacity.rs" 6 0 6 41]
   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
-  let%span sseq16 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq16 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed17 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow
@@ -191,7 +191,7 @@ module M_09_capacity__clear_vec [#"09_capacity.rs" 14 0 14 35]
   let%span sresolve4 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34
   let%span svec5 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sinvariant6 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44
-  let%span sseq7 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
+  let%span sseq7 = "../../../../creusot-contracts/src/logic/seq.rs" 623 20 623 95
   let%span sboxed8 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
   use prelude.prelude.Borrow