diff --git a/examples/cursor_examples.mlw b/examples/cursor_examples.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..7c2e128864097eeb1ab7bad33dc39e7cf1488270
--- /dev/null
+++ b/examples/cursor_examples.mlw
@@ -0,0 +1,262 @@
+
+(** Cursors
+
+   TO BE DISCUSSED
+   - a [coherent] predicate is also convenient for an immutable collection
+   - having [next] raising an exception imposes a try-with around the loop
+     it is simpler to have [next] with a precondition together with
+     an operation [has_next]
+
+  QUESTION: in IntListCursor, field to_do is no more ghost; will it be
+  allowed by refinement? otherwise, simply add a non-ghost field
+  identical to to_do
+*)
+
+module TestCursor
+
+  use import int.Int
+  use import int.Sum
+  use import seq.Seq
+  use import ref.Refint
+
+  use import cursor.Cursor
+
+  (** sums all the remaining elements in the cursor *)
+  let sum (c: cursor int) : int
+    requires { permitted c }
+    requires { c.visited = empty }
+    ensures  { result = sum (get c.visited) 0 (length c.visited) }
+    diverges
+  = let s = ref 0 in
+    while has_next c do
+      invariant { permitted c }
+      invariant { !s = sum (get c.visited) 0 (length c.visited) }
+      let x = next c in
+      s += x
+    done;
+    !s
+
+end
+
+(** {2 Iteration over an immuable collection}
+
+    here we choose a list *)
+
+module ListCursorImpl (* : ListCursor *)
+
+  use import int.Int
+  use import list.List
+  use import seq.Seq
+  use import seq.OfList
+
+  type cursor 'a = {
+    mutable ghost visited    : seq 'a;
+            ghost collection : list 'a;
+    mutable       to_visit   : list 'a;
+  } invariant { visited ++ to_visit = collection }
+    by { visited = empty; collection = Nil; to_visit = Nil }
+
+  predicate permitted (c: cursor 'a) =
+    length c.visited <= length c.collection /\
+    forall i. 0 <= i < length c.visited -> c.visited[i] = c.collection[i]
+
+  predicate complete (c: cursor 'a) =
+    length c.visited = length c.collection
+
+  let lemma snoc_Cons (s: seq 'a) (l: list 'a) (x: 'a)
+    ensures { snoc s x ++ l == s ++ Cons x l }
+  = ()
+
+  let next (c: cursor 'a) : 'a
+    requires { not (complete c) }
+    writes   { c }
+    ensures  { c.visited = snoc (old c).visited result }
+    ensures  { match (old c).to_visit with
+               | Nil -> false
+               | Cons x r -> c.to_visit = r /\ x = result
+               end }
+  = match c.to_visit with
+    | Nil -> absurd
+    | Cons x r ->
+      let ghost v0 = c.visited in
+      c.visited <- snoc c.visited x; c.to_visit <- r;
+      snoc_Cons v0 r x;
+      assert { c.to_visit == c.collection [length c.visited ..] };
+      x
+    end
+
+  let has_next (c: cursor 'a) : bool
+    ensures { result <-> not (complete c) }
+  = match c.to_visit with (* could define a [val eq (l1 l2: list 'a) : bool] *)
+    | Nil -> false
+    | _   -> true
+    end
+
+  let create (t: list 'a) : cursor 'a
+    ensures { result.visited = empty }
+    ensures { result.collection = t }
+    ensures { result.to_visit = t }
+  = { visited = empty; collection = t; to_visit = t }
+
+  clone cursor.ListCursor with
+    type cursor     = cursor,
+    val  create     = create,
+    val  C.has_next = has_next,
+    val  C.next     = next
+
+end
+
+module TestListCursor
+
+  use import int.Int
+  use import int.Sum as S
+  use import list.List
+  use import list.Length
+  use import list.Sum
+  use import ref.Refint
+  use import seq.Seq
+  use import seq.OfList
+
+  clone import cursor.ListCursor
+
+  lemma sum_of_list: forall l: list int.
+    sum l = S.sum (get (of_list l)) 0 (length l)
+
+  let list_sum (l: list int) : int
+    ensures { result = sum l }
+  = let s = ref 0 in
+    let c = create l in
+    while C.has_next c do
+      invariant { !s = S.sum (get c.visited) 0 (length c.visited) }
+      invariant { permitted c }
+      variant   { length l - length c.visited }
+      let x = C.next c in
+      s += x
+    done;
+    !s
+
+end
+
+module TestListCursorLink
+
+  use import ListCursorImpl
+
+  clone import TestListCursor with
+    type ListCursor.cursor     = cursor,
+    val  ListCursor.C.next     = next,
+    val  ListCursor.C.has_next = has_next,
+    val  ListCursor.create     = create
+
+end
+
+(** {2 Iteration over a mutable collection}
+
+    here we choose an array of integers *)
+
+module ArrayCursorImpl (* : ArrayCursor *)
+
+  use import int.Int
+  use import array.Array
+  use import array.ToSeq
+  use import list.List
+  use import list.Reverse
+  use import array.ToList
+  use import seq.Seq
+
+  type cursor 'a = {
+    mutable ghost visited    : seq 'a;
+                  collection : seq 'a; (* FIXME : extraction of seq *)
+    mutable       index      : int;    (** index of next element *)
+  } invariant { 0 <= index <= length collection /\
+                index = length visited /\
+                forall i. 0 <= i < index -> collection[i] = visited[i] }
+    by { visited = empty; collection = empty; index = 0 }
+
+  predicate permitted (c: cursor 'a) =
+    length c.visited <= length c.collection /\
+    forall i. 0 <= i < length c.visited -> c.visited[i] = c.collection[i]
+
+  predicate complete (c: cursor 'a) =
+    length c.visited = length c.collection
+
+  let create (a: array 'a) : cursor 'a
+    ensures { result.visited = empty }
+    ensures { result.index = 0 }
+    ensures { result.collection = to_seq a }
+  = { visited = empty; collection = to_seq a; index = 0; }
+
+  let has_next (c: cursor 'a) : bool
+    ensures  { result <-> not (complete c) }
+  = c.index < length c.collection
+
+  let next (c: cursor 'a) : 'a
+    requires { not (complete c) }
+    writes   { c }
+    ensures  { c.visited = snoc (old c).visited result }
+    ensures  { c.index = (old c).index + 1 }
+  = if c.index >= length c.collection then absurd
+    else begin let x = c.collection[c.index] in
+      c.visited <- snoc c.visited x;
+      c.index <- c.index + 1;
+      x end
+
+  clone cursor.ArrayCursor with
+    type cursor   = cursor,
+    val  C.next     = next,
+    val  C.has_next = has_next,
+    val  create     = create
+
+end
+
+module TestArrayCursor
+
+  use import int.Int
+  use import array.Array
+  use import array.ToSeq
+  use import seq.Seq
+  use import int.Sum
+  use import ref.Refint
+
+  clone import cursor.ArrayCursor
+
+  let array_sum (a: array int) : int
+    ensures { result = sum (Array.([]) a) 0 (length a) }
+  = let s = ref 0 in
+    let c = create a in
+    while C.has_next c do
+      invariant { !s = sum (get c.visited) 0 (length c.visited) }
+      invariant { permitted c }
+      variant   { length c.collection - length c.visited }
+      let x = C.next c in
+      s += x
+    done;
+    !s
+
+  let harness1 () : unit
+  = let a = Array.make 42 0 in
+    let c = create a in
+    let x = C.next c in
+    assert { x = 0 }
+
+(*
+  let harness2 () : unit
+  = let a = Array.make 42 0 in
+    let c = create a in
+    a[1] <- 17;
+    let x = C.next c in
+    assert { x = 0 }
+*)
+
+end
+
+module TestArrayCursorLink
+
+  use import ArrayCursorImpl
+
+  clone import TestArrayCursor with
+    type ArrayCursor.cursor     = cursor,
+    val  ArrayCursor.C.next     = next,
+    val  ArrayCursor.C.has_next = has_next,
+    val  ArrayCursor.create     = create
+
+end
\ No newline at end of file
diff --git a/examples/to_port/cursor/why3session.xml b/examples/to_port/cursor/why3session.xml
deleted file mode 100644
index 64e225a78e51857cca3d23eb689cad67ee91f944..0000000000000000000000000000000000000000
--- a/examples/to_port/cursor/why3session.xml
+++ /dev/null
@@ -1,52 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
-"http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="4">
-<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../cursor.mlw">
-<theory name="TestCursor" sum="401d4ce6900374ae25d5039a681f2923">
- <goal name="VC sum" expl="VC for sum">
- <proof prover="0"><result status="valid" time="1.00" steps="461"/></proof>
- </goal>
-</theory>
-<theory name="ListCursor" sum="98ec1f1e0527eca4c14a2ff349314fb9">
- <goal name="VC cursor" expl="VC for cursor">
- <proof prover="0"><result status="valid" time="0.01" steps="33"/></proof>
- </goal>
- <goal name="VC snoc_Cons" expl="VC for snoc_Cons">
- <proof prover="0"><result status="valid" time="0.04" steps="99"/></proof>
- </goal>
- <goal name="VC next" expl="VC for next">
- <proof prover="0"><result status="valid" time="0.23" steps="465"/></proof>
- </goal>
- <goal name="VC has_next" expl="VC for has_next">
- <proof prover="0"><result status="valid" time="0.03" steps="66"/></proof>
- </goal>
- <goal name="VC create" expl="VC for create">
- <proof prover="0"><result status="valid" time="0.02" steps="51"/></proof>
- </goal>
- <goal name="Cursor.VC create" expl="VC for create">
- <proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
- </goal>
- <goal name="Cursor.VC next" expl="VC for next">
- <proof prover="0"><result status="valid" time="0.02" steps="55"/></proof>
- </goal>
- <goal name="Cursor.VC has_next" expl="VC for has_next">
- <proof prover="0"><result status="valid" time="0.01" steps="1"/></proof>
- </goal>
-</theory>
-<theory name="TestListCursor" sum="912c61d8c8a3a20497d6a0b557c300d1">
- <goal name="VC list_sum" expl="VC for list_sum">
- <proof prover="0"><result status="valid" time="2.58" steps="1648"/></proof>
- </goal>
-</theory>
-<theory name="IntArrayCursor" sum="4c9dca290af968fc2d686a13d791aecc">
- <goal name="VC a" expl="VC for a">
- <proof prover="0"><result status="valid" time="0.01" steps="1"/></proof>
- </goal>
- <goal name="VC cursor" expl="VC for cursor">
- <proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
- </goal>
-</theory>
-</file>
-</why3session>
diff --git a/examples/to_port/cursor/why3shapes.gz b/examples/to_port/cursor/why3shapes.gz
deleted file mode 100644
index 733b83b6d0859af7da84d69b18e1f549c4849c62..0000000000000000000000000000000000000000
Binary files a/examples/to_port/cursor/why3shapes.gz and /dev/null differ
diff --git a/examples/to_port/cursor_examples.mlw b/examples/to_port/cursor_examples.mlw
deleted file mode 100644
index dfdf982bf5b77fe22a22383d64c8d56f7a617c1a..0000000000000000000000000000000000000000
--- a/examples/to_port/cursor_examples.mlw
+++ /dev/null
@@ -1,272 +0,0 @@
-
-(** Cursors
-
-   TO BE DISCUSSED
-   - a [coherent] predicate is also convenient for an immutable collection
-   - having [next] raising an exception imposes a try-with around the loop
-     it is simpler to have [next] with a precondition together with
-     an operation [has_next]
-
-  QUESTION: in IntListCursor, field to_do is no more ghost; will it be
-  allowed by refinement? otherwise, simply add a non-ghost field
-  identical to to_do
-*)
-
-module TestCursor
-
-  use import int.Int
-  use import int.Sum
-  use import seq.Seq
-  use import ref.Refint
-
-  use import cursor.Cursor
-
-  (** sums all the remaining elements in the cursor *)
-  let sum (c: cursor int) : int
-    requires { permitted c }
-    requires { c.visited = empty }
-    ensures  { result = sum (get c.visited) 0 (length c.visited) }
-    diverges
-  = let s = ref 0 in
-    while has_next c do
-      invariant { permitted c }
-      invariant { !s = sum (get c.visited) 0 (length c.visited) }
-      let x = next c in
-      s += x
-    done;
-    !s
-
-end
-
-(** {2 Iteration over an immuable collection}
-
-    here we choose a list *)
-
-module ListCursorImpl (* : IterableList *)
-
-  use import int.Int
-  use import list.List
-  use import seq.Seq
-  use import seq.OfList
-
-  type cursor 'a = {
-    mutable ghost visited    : seq 'a;
-            ghost collection : list 'a;
-    mutable       to_visit   : list 'a;
-  } invariant { visited ++ to_visit = collection }
-    by { visited = empty; collection = Nil; to_visit = Nil }
-
-  predicate permitted (c: cursor 'a) =
-    length c.visited <= length c.collection /\
-    forall i. 0 <= i < length c.visited -> c.visited[i] = c.collection[i]
-
-  predicate complete (c: cursor 'a) =
-    length c.visited = length c.collection
-
-  let lemma snoc_Cons (s: seq 'a) (l: list 'a) (x: 'a)
-    ensures { snoc s x ++ l == s ++ Cons x l }
-  = ()
-
-  let next (c: cursor 'a) : 'a
-    requires { not (complete c) }
-    writes   { c }
-    ensures  { c.visited = snoc (old c).visited result }
-    ensures  { match (old c).to_visit with
-               | Nil -> false
-               | Cons x r -> c.to_visit = r /\ x = result
-               end }
-  = match c.to_visit with
-    | Nil -> absurd
-    | Cons x r ->
-      let ghost v0 = c.visited in
-      c.visited <- snoc c.visited x; c.to_visit <- r;
-      snoc_Cons v0 r x;
-      assert { c.to_visit == c.collection [length c.visited ..] };
-      x
-    end
-
-  let has_next (c: cursor 'a) : bool
-    ensures { result <-> not (complete c) }
-  = match c.to_visit with (* could define a [val eq (l1 l2: list 'a) : bool] *)
-    | Nil -> false
-    | _   -> true
-    end
-
-  let create (t: list 'a) : cursor 'a
-    ensures { result.visited = empty }
-    ensures { result.collection = t }
-    ensures { result.to_visit = t }
-  = { visited = empty; collection = t; to_visit = t }
-
-  clone cursor.ListCursor with
-    type cursor = cursor,
-    val create = create,
-    val C.has_next = has_next,
-    val C.next = next
-
-end
-
-module TestListCursor
-
-  use import int.Int
-  use import int.Sum as S
-  use import list.List
-  use import list.Length
-  use import list.Sum
-  use import ref.Refint
-  use import seq.Seq
-  use import seq.OfList
-  use import cursor.ListCursor
-
-  let lemma aux2 (f g: int -> int) (a b c d: int)
-    requires { b - a = d - c }
-    requires { forall i. a <= i < b -> f i  = g i }
-    ensures  { S.sum f a b = S.sum g a b }
-  = ()
-
-  let lemma aux (s: seq int) (x: int)
-    ensures { let ss = cons x s in
-              S.sum (get ss) 0 (length ss) = x + S.sum (get s) 0 (length s) }
-  = let ss = cons x s in
-    assert { forall i. 0 <= i < length s -> get s i = get ss (i+1) }
-
-  lemma sum_of_list: forall l: list int.
-    sum l = S.sum (get (of_list l)) 0 (length l)
-
-  let list_sum (l: list int) : int
-    ensures { result = sum l }
-  = let s = ref 0 in
-    let c = create l in
-    while C.has_next c do
-      invariant { !s = S.sum (get c.visited) 0 (length c.visited) }
-      invariant { permitted c }
-      variant   { length l - length c.visited }
-      let x = C.next c in
-      s += x
-    done;
-    !s
-
-end
-
-(** {2 Iteration over a mutable collection}
-
-    here we choose an array of integers *)
-
-(* module IntArrayCursor (\* : IterableList *\) *)
-
-(*   use import int.Int *)
-(*   use import array.Array *)
-(*   use import list.List *)
-(*   use import list.Reverse *)
-(*   use import array.ToList *)
-(*   use import seq.Seq *)
-
-(*   type t 'a = array 'a *)
-
-(*   val ghost constant a : {array 'a} *)
-(*     ensures { Array.length result = 0 } *)
-
-(*   type cursor 'a = { *)
-(*     mutable ghost visited: seq 'a; *)
-(*             ghost collection: {t 'a}; *)
-(*     mutable       index: int;      (\** index of next element *\) *)
-(*   } invariant { 0 <= index <= Array.length collection /\ *)
-(*                 index = length visited /\ *)
-(*                 forall i. 0 <= i < index -> *)
-(*                   Array.([]) collection i = visited[i] } *)
-(*     by { visited = empty; collection = a; index = 0 } *)
-
-(*   clone import cursor.Cursor with *)
-(*     type cursor = cursor, *)
-(*     type t = t *)
-
-(*   (\* predicate permitted (v: seq int) (t: t) = *\) *)
-(*   (\*   length v <= length t /\ *\) *)
-(*   (\*   forall i. 0 <= i *\) *)
-
-(*   (\* let create (t: t) : cursor *\) *)
-(*   (\*   ensures { result.done_ = Nil } *\) *)
-(*   (\*   ensures { coherent t result } *\) *)
-(*   (\* = *\) *)
-(*   (\*   { done_ = Nil; to_do = to_list t 0 (length t); index = 0; } *\) *)
-
-(*   (\* let has_next (t: t) (c: cursor) : bool *\) *)
-(*   (\*   requires { coherent t c } *\) *)
-(*   (\*   ensures  { result <-> c.to_do <> Nil } *\) *)
-(*   (\* = *\) *)
-(*   (\*   c.index < length t *\) *)
-
-(*   (\* let rec lemma reverse_cons (a: array int) (l u: int) *\) *)
-(*   (\*   requires { l <= u } *\) *)
-(*   (\*   ensures  { reverse (to_list a l (u+1)) = *\) *)
-(*   (\*              Cons a[u] (reverse (to_list a l u)) } *\) *)
-(*   (\*   variant  { u - l } *\) *)
-(*   (\* = if l < u then reverse_cons a (l+1) u *\) *)
-
-(*   (\* let next (t: t) (c: cursor) : elt *\) *)
-(*   (\*   requires { c.to_do <> Nil } *\) *)
-(*   (\*   requires { coherent t c } *\) *)
-(*   (\*   writes   { c } *\) *)
-(*   (\*   ensures  { match old c.to_do with *\) *)
-(*   (\*              | Nil -> false *\) *)
-(*   (\*              | Cons x l -> result = x /\ c.done_ = Cons x (old c.done_) /\ *\) *)
-(*   (\*                            c.to_do = l end } *\) *)
-(*   (\*   ensures  { coherent t c } *\) *)
-(*   (\* = *\) *)
-(*   (\*   match c.to_do with *\) *)
-(*   (\*   | Nil -> absurd *\) *)
-(*   (\*   | Cons x r -> c.to_do <- r; c.done_ <- Cons x c.done_ *\) *)
-(*   (\*   end; *\) *)
-(*   (\*   let x = t[c.index] in *\) *)
-(*   (\*   c.index <- c.index + 1; *\) *)
-(*   (\*   x *\) *)
-
-(* end *)
-
-(* module TestArrayCursor *)
-
-(*   use import int.Int *)
-(*   use list.Sum as L *)
-(*   use list.Length as LL *)
-(*   use import array.Array *)
-(*   use import array.ArraySum *)
-(*   use import array.ToList *)
-(*   use import ref.Refint *)
-(*   use import IntArrayCursor *)
-
-(*   let rec lemma array_sum_array_to_list (a: array int) (l u: int) : unit *)
-(*     ensures { sum a l u = L.sum (to_list a l u) } variant { u-l } *)
-(*   = if l < u then array_sum_array_to_list a (l+1) u *)
-
-(*   let array_sum (a: array int) : int *)
-(*     ensures { result = sum a 0 (length a) } *)
-(*   = *)
-(*     let s = ref 0 in *)
-(*     let c = create a in *)
-(*     while has_next a c do *)
-(*       invariant { sum a 0 (length a) = !s + L.sum c.to_do } *)
-(*       invariant { coherent a c } *)
-(*       variant   { LL.length c.to_do } *)
-(*       let x = next a c in *)
-(*       s += x *)
-(*     done; *)
-(*     !s *)
-
-(*   let harness1 () : unit *)
-(*   = *)
-(*     let a = Array.make 42 0 in *)
-(*     let c = create a in *)
-(*     let x = next a c in *)
-(*     assert { x = 0 } *)
-
-(* (\* *)
-(*   let harness2 () : unit *)
-(*   = *)
-(*     let a = Array.make 42 0 in *)
-(*     let c = create a in *)
-(*     a[1] <- 17; *)
-(*     let x = next a c in *)
-(*     assert { x = 0 } *)
-(* *\) *)
-
-(* end *)
diff --git a/modules/array.mlw b/modules/array.mlw
index eda3e7a17d0de7c117a9b7f6be8e54d127f54e44..b2927ba74baf415480658e061a289d746c3e778f 100644
--- a/modules/array.mlw
+++ b/modules/array.mlw
@@ -339,15 +339,13 @@ module ToSeq
     variant { u - l }
   = if u <= l then S.empty else S.cons a[l] (to_seq_sub a (l+1) u)
 
-  let rec lemma to_seq_length
-    (a: array 'a) (l u: int)
+  let rec lemma to_seq_length (a: array 'a) (l u: int)
     requires { 0 <= l <= u <= length a }
     variant  { u - l }
     ensures  { S.length (to_seq_sub a l u) = u - l }
   = if l < u then to_seq_length a (l+1) u
 
-  let rec lemma to_seq_nth
-    (a: array 'a) (l i u: int)
+  let rec lemma to_seq_nth (a: array 'a) (l i u: int)
     requires { 0 <= l <= i < u <= length a }
     variant  { i - l }
     ensures  { S.get (to_seq_sub a l u) (i - l) = a[i] }
diff --git a/modules/cursor.mlw b/modules/cursor.mlw
index 9b47621279d7dc085b67a08ac7b02b42ce292f1f..41dd879e48aee13353c98ae3d716612eb6e8a52c 100644
--- a/modules/cursor.mlw
+++ b/modules/cursor.mlw
@@ -56,29 +56,30 @@ module ListCursor
 
 end
 
-module CursorArray
+module ArrayCursor
 
   use import array.Array
+  use import array.ToSeq
   use import seq.Seq
   use import seq.OfList
   use import int.Int
 
   type cursor 'a = private {
-    ghost mutable visited : seq 'a;
-    ghost         array   : array 'a;
+    ghost mutable visited    : seq 'a;
+    ghost         collection : seq 'a;
   }
 
   predicate permitted (c: cursor 'a) =
-    length c.visited <= Array.length c.array /\
-    forall i. 0 <= i < length c.visited -> c.visited[i] = Array.([]) c.array i
+    length c.visited <= length c.collection /\
+    forall i. 0 <= i < length c.visited -> c.visited[i] = c.collection[i]
 
   predicate complete  (c: cursor 'a) =
-    length c.visited = Array.length c.array
+    length c.visited = length c.collection
 
   val create (a: array 'a) : cursor 'a
     ensures { permitted result }
     ensures { result.visited = empty }
-    ensures { result.array = a }
+    ensures { result.collection = to_seq a }
 
   clone import Cursor as C with
     type cursor = cursor,
diff --git a/src/mlw/pmodule.ml b/src/mlw/pmodule.ml
index a8aadd6a628898f2128380efdb0d974a605b3c9a..408d18309669e7bc1a14cd2cc37684ee5a1a62fd 100644
--- a/src/mlw/pmodule.ml
+++ b/src/mlw/pmodule.ml
@@ -864,8 +864,8 @@ let clone_type_record cl s d s' d' =
     let pj_str = pj.pv_vs.vs_name.id_string in
     let pj_ity = clone_ity cl pj.pv_ity in
     let pj_ght = pj.pv_ghost in
-    let rs' = try Hstr.find fields' pj_str
-      with Not_found -> raise (BadInstance id) in
+    let rs' = try Hstr.find fields' pj_str with Not_found ->
+      raise (BadInstance id) in
     let pj' = fd_of_rs rs' in
     let pj'_ity = pj'.pv_ity in
     let pj'_ght = pj'.pv_ghost in
diff --git a/theories/int.why b/theories/int.why
index 671b0f8ea270c90e192b2aa10c108a50edb19a3f..b286034b5a5066d882b7c29ff5ee37dd3060eeca 100644
--- a/theories/int.why
+++ b/theories/int.why
@@ -416,6 +416,13 @@ theory Sum
     forall f: int -> int, a b c: int. a <= b <= c ->
     sum f a c = sum f a b + sum f b c
 
+  let rec lemma shift_left (f g: int -> int) (a b c d: int)
+    requires { b - a = d - c }
+    requires { forall i. a <= i < b -> f i  = g (c + i - a) }
+    variant  { b - a }
+    ensures  { sum f a b = sum g c d }
+  = if a < b then shift_left f g (a+1) b (c+1) d
+
 end
 
 (** {2 Factorial function} *)