diff --git a/src/plugins/wp/share/why3/frama_c_wp/vlist.mlw b/src/plugins/wp/share/why3/frama_c_wp/vlist.mlw
index db170632561a16c23e801182fd0b6f1800fa7853..761b194eec3f1b044db5f9ff215c55921f7e6ae8 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/vlist.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/vlist.mlw
@@ -41,35 +41,45 @@ theory Vlist
   (* -------------------------------------------------------------------- *)
 
   function nil : list 'a = Nil
-  
+
   function cons (x: 'a) (xs: list 'a) : list 'a = Cons x xs
-  
+
   let function head (l: list 'a) : 'a
     requires {l <> Nil} ensures {hd l = Some result}
   = match l with Nil -> absurd | Cons h _ -> h end
-  
+
   let function tail (l: list 'a) : list 'a
     requires {l <> Nil} ensures {tl l = Some result}
   = match l with Nil -> absurd | Cons _ t -> t end
-  
+
   function concat (xs: list 'a) (ys: list 'a) : list 'a = xs ++ ys
-  
-  let rec function repeat (xs: list 'a) (n: int) : list 'a
-    variant {n} =
-    if (n <= 0) then Nil else xs ++ repeat xs (n - 1)
-  
-  let rec function nth (l: list 'a) (n: int): 'a
-    requires {l <> Nil}
-    requires {0 <= n}
-    requires {n < length l}
-    variant {n}
-    ensures {Nth.nth n l = Some result}
-  = match l with Nil -> absurd | Cons x r ->
-    if n = 0 then x else nth r (n - 1)
-  end
 
   function elt (x:'a) : list 'a  = cons x nil
 
+  (* repeat *)
+  (* Here we are forced to use axiomatic definition to conform to ACSL *)
+
+  function repeat (xs: list 'a) (n: int) : list 'a
+
+  axiom repeat_empty:
+    forall xs : list 'a. repeat xs 0 = Nil
+
+  axiom repeat_pos:
+    forall xs : list 'a, n. n > 0 -> repeat xs n = xs ++ repeat xs (n - 1)
+
+  (* nth *)
+  (* Here we are forced to use axiomatic definition to conform to ACSL *)
+
+  function nth (l: list 'a) (n: int): 'a
+
+  axiom nth_zero:
+    forall l : list 'a.
+      l <> Nil -> nth l 0 = head l
+
+  axiom nth_pos:
+    forall l : list 'a, n.
+      l <> Nil -> 0 < n < length l -> nth l n = nth (tail l) (n-1)
+
   (* -------------------------------------------------------------------- *)
   (* --- cons                                                         --- *)
   (* -------------------------------------------------------------------- *)
@@ -84,11 +94,11 @@ theory Vlist
   (* -------------------------------------------------------------------- *)
   (* --- concat                                                       --- *)
   (* -------------------------------------------------------------------- *)
-  
+
   lemma concat_nil_left: forall w: list 'a. concat Nil w = w
-  
+
   lemma concat_nil_right: forall w: list 'a. concat w Nil = w
-  
+
   lemma concat_cons: forall u v: list 'a, x: 'a.
     concat (cons x u) v = cons x (concat u v)
 
@@ -96,7 +106,7 @@ theory Vlist
     requires {u <> Nil}
     ensures {head (concat u v) = head u}
   = match u with Nil -> absurd | Cons _ _ -> () end
-  
+
   lemma concat_tail:
     forall u v: list 'a. u <> Nil -> concat (tail u) v = tail (concat u v)
 
@@ -188,7 +198,7 @@ theory Vlist
   (* -------------------------------------------------------------------- *)
 
   lemma eq_cons_concat:
-    forall x:'a, v,w:list 'a [concat (cons x v) w]. 
+    forall x:'a, v,w:list 'a [concat (cons x v) w].
       vlist_eq (concat (cons x v) w) (cons x (concat v w))
 
   lemma rw_cons_concat:
@@ -203,7 +213,7 @@ theory Vlist
   (* --- associativity                                                --- *)
   (* -------------------------------------------------------------------- *)
 
-  lemma eq_assoc_concat: 
+  lemma eq_assoc_concat:
     forall u,v,w:list 'a.
       vlist_eq (concat (concat u v) w) (concat u (concat v w))
 
@@ -219,8 +229,9 @@ theory Vlist
     forall w:list 'a [repeat w 0].
       repeat w 0 = nil
 
-  lemma eq_repeat_one:
-    forall w:list 'a. vlist_eq (repeat w 1) w
+  let lemma eq_repeat_one (w: list 'a)
+    ensures { vlist_eq (repeat w 1) w }
+  = assert { repeat w 1 = repeat w 0 ++ w }
 
   lemma rw_repeat_one:
     forall w:list 'a [repeat w 1]. repeat w 1 = w
@@ -272,22 +283,22 @@ theory Vlist
 
 (*--- To avoid exponential blowup of use of repeat_after by alt-ergo ---*)
 
-function repeat_box (list 'a) int : (list 'a) (* repeat *)
+  function repeat_box (list 'a) int : (list 'a) (* repeat *)
 
-axiom rw_repeat_box_unfold: 
-  forall w:list 'a, n:int [ repeat_box w n ].
-    repeat_box w n = repeat w n
+  axiom rw_repeat_box_unfold:
+    forall w:list 'a, n:int [ repeat_box w n ].
+      repeat_box w n = repeat w n
 
-axiom rw_repeat_plus_box_unfold: 
-  forall w:list 'a, a,b: int [ repeat_box w (Int.(+) a b) ].
-    (Int.(<=) 0 a)
- -> (Int.(<=) 0 b)
- -> repeat_box w (Int.(+) a b) = concat (repeat w a)
+  axiom rw_repeat_plus_box_unfold:
+    forall w:list 'a, a,b: int [ repeat_box w (Int.(+) a b) ].
+      (Int.(<=) 0 a)
+  -> (Int.(<=) 0 b)
+  -> repeat_box w (Int.(+) a b) = concat (repeat w a)
                                                 (repeat w b)
-axiom rw_repeat_plus_one_box_unfold: 
-  forall w:list 'a, n:int [ repeat_box w n ].
-    (Int.(<) 0 n)
- -> (repeat_box w n = (concat (repeat w (Int.(-) n 1)) w)
- && (repeat_box w (Int.(+) n 1) = concat (repeat w n) w))
+  axiom rw_repeat_plus_one_box_unfold:
+    forall w:list 'a, n:int [ repeat_box w n ].
+      (Int.(<) 0 n)
+  -> (repeat_box w n = (concat (repeat w (Int.(-) n 1)) w)
+  && (repeat_box w (Int.(+) n 1) = concat (repeat w n) w))
 
 end