diff --git a/Makefile.in b/Makefile.in
index 0f86df60111d80e8bf1fa75f57fedfbab58ce5d3..47a4852d255f58484cd66e3557dda0dca6e22387 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -866,7 +866,7 @@ COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
 COQLIBS_SET_FILES = Set
 COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
 
-COQLIBS_MAP_FILES = Map Occ MapPermut MapInjection
+COQLIBS_MAP_FILES = Map Const Occ MapPermut MapInjection
 COQLIBS_MAP = $(addprefix lib/coq/map/, $(COQLIBS_MAP_FILES))
 
 COQLIBS_LIST_FILES = List Length Mem Nth NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt NthNoOpt RevAppend Combine Distinct NumOcc Permut
diff --git a/lib/coq/int/NumOf.v b/lib/coq/int/NumOf.v
index c24f1d83799d5fd0a4b3cef4cd2a8f68b8ff7ce7..650106437d73ecf8e44ef2e1502c31dafbcc1b6d 100644
--- a/lib/coq/int/NumOf.v
+++ b/lib/coq/int/NumOf.v
@@ -282,3 +282,4 @@ intros p1 p2 a b h1.
 apply le_ge_eq.
 split; apply numof_change_any; apply h1.
 Qed.
+
diff --git a/lib/coq/map/Map.v b/lib/coq/map/Map.v
index c8db967f1d8026bc13eef280d7b064e9907881a2..e4def485924a20d7407f6007c0e0152c2a335345 100644
--- a/lib/coq/map/Map.v
+++ b/lib/coq/map/Map.v
@@ -77,17 +77,13 @@ unfold get, set.
 now case why_decidable_eq.
 Qed.
 
-(* Why3 goal *)
-Definition const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
-  b -> (map a b).
+(* Unused content named const
 intros a a_WT b b_WT y.
 exact (_map_constr _ _ (fun _ => y)).
 Defined.
-
-(* Why3 goal *)
-Lemma Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
-  forall (b1:b) (a1:a), ((get (const b1: (map a b)) a1) = b1).
+ *)
+(* Unused content named Const
 Proof.
 easy.
 Qed.
-
+ *)
diff --git a/lib/coq/seq/Seq.v b/lib/coq/seq/Seq.v
index 8e739c0fdb83c2fea33eda7ba5dd6b7ce96a17c0..baae044f4f0280f66133de0c40dd44a743b199c4 100644
--- a/lib/coq/seq/Seq.v
+++ b/lib/coq/seq/Seq.v
@@ -1,3 +1,14 @@
+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
 (* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
@@ -59,6 +70,36 @@ exact ((fix nth n l := match l with
   | cons h t => if Zeq_bool n 0%Z then h else nth (n - 1)%Z t end) i s).
 Defined.
 
+(* Why3 goal *)
+Definition set: forall {a:Type} {a_WT:WhyType a}, (seq a) -> Z -> a -> (seq
+  a).
+admit.
+Defined.
+
+(* Why3 goal *)
+Lemma set_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (i:Z)
+  (v:a), ((0%Z <= i)%Z /\ (i < (length s))%Z) -> ((length (set s i
+  v)) = (length s)).
+intros a a_WT s i v (h1,h2).
+admit.
+Qed.
+
+(* Why3 goal *)
+Lemma set_def2 : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (i:Z)
+  (v:a), ((0%Z <= i)%Z /\ (i < (length s))%Z) -> ((get (set s i v) i) = v).
+intros a a_WT s i v (h1,h2).
+admit.
+Qed.
+
+(* Why3 goal *)
+Lemma set_def3 : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (i:Z)
+  (v:a), ((0%Z <= i)%Z /\ (i < (length s))%Z) -> forall (j:Z),
+  ((0%Z <= j)%Z /\ (j < (length s))%Z) -> ((~ (j = i)) -> ((get (set s i v)
+  j) = (get s j))).
+intros a a_WT s i v (h1,h2) j (h3,h4) h5.
+admit.
+Qed.
+
 (* Why3 assumption *)
 Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(seq a)) (s2:(seq
   a)): Prop := ((length s1) = (length s2)) /\ forall (i:Z), ((0%Z <= i)%Z /\
@@ -179,6 +220,7 @@ Lemma snoc_get : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (x:a)
   (i:Z), ((0%Z <= i)%Z /\ (i <= (length s))%Z) -> (((i < (length s))%Z ->
   ((get (snoc s x) i) = (get s i))) /\ ((~ (i < (length s))%Z) ->
   ((get (snoc s x) i) = x))).
+admit.
 (*
 intros a a_WT (l, d) x i (h1,h2).
 split; intros.
@@ -200,9 +242,8 @@ subst i.
 rewrite (Zabs2Nat.id (Datatypes.length l)). omega.
 subst i.
 rewrite (Zabs2Nat.id (Datatypes.length l)). omega.
-Qed.
 *)
-Admitted. (* TODO *)
+Qed.
 
 (* Why3 goal *)
 Definition mixfix_lb_dtdt_rb: forall {a:Type} {a_WT:WhyType a}, (seq a) ->
@@ -242,14 +283,14 @@ Defined.
 Lemma concat_length : forall {a:Type} {a_WT:WhyType a}, forall (s1:(seq a))
   (s2:(seq a)), ((length (infix_plpl s1
   s2)) = ((length s1) + (length s2))%Z).
+admit.
 (*
 intros a a_WT s1 s2.
 unfold length, infix_plpl.
 rewrite List.app_length.
 rewrite Nat2Z.inj_add. auto.
-Qed.
 *)
-Admitted. (* TODO *)
+Qed.
 
 (* Why3 goal *)
 Lemma concat_get1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(seq a))
diff --git a/modules/array.mlw b/modules/array.mlw
index 52107b7606f027c773456b39086f2819047472e3..dfe44979dc0db23b6766dedcffaf5e695607b8d8 100644
--- a/modules/array.mlw
+++ b/modules/array.mlw
@@ -49,11 +49,17 @@ module Array
   = if i < 0 || i >= length a then raise OutOfBounds;
     a[i] <- v
 
-  function make (n: int) (v: ~'a) : array 'a =
-    { length = n; elts = M.const v }
+  function make (n: int) (v: ~'a) : array 'a
+  axiom make_length:
+    forall n:int, v:'a. length (make n v) = n
+  axiom make_elts:
+    forall n i:int, v:'a. get (make n v) i = v
+
 
   val make (n: int) (v: ~'a) : array 'a
-    requires { "expl:array creation size" n >= 0 } ensures { result = make n v }
+    requires { "expl:array creation size" n >= 0 }
+    ensures { length result = n }
+    ensures { forall i:int. result[i] = v }
 
   val append (a1: array ~'a) (a2: array 'a) : array 'a
     ensures { length result = length a1 + length a2 }
diff --git a/theories/map.why b/theories/map.why
index e47d4755e96576115738d4b5ad2f40a340a18f35..31556417df1ebe3d3161a6460820cb179f341560 100644
--- a/theories/map.why
+++ b/theories/map.why
@@ -28,6 +28,13 @@ theory Map
     forall b : 'b [m[a1 <- b][a2]].
     a1 <> a2 -> m[a1 <- b][a2] = m[a2]
 
+end
+
+
+theory Const
+
+  use import Map
+
   function const ~'b : map 'a 'b
 
   axiom Const : forall b:'b, a:'a. (const b)[a] = b
@@ -239,4 +246,3 @@ theory MapParam
 
 end
 *)
-
diff --git a/theories/set.why b/theories/set.why
index cbf839e76ab69f19e991e15227b6d9473f4acc9e..64b50b1dd402a52730279aabe06247bd42aa80ec 100644
--- a/theories/set.why
+++ b/theories/set.why
@@ -339,6 +339,7 @@ end
 theory SetMap
 
   use import map.Map
+  use import map.Const
   use import bool.Bool
 
   type set 'a = map 'a bool