diff --git a/lib/coq/bv/BV_Gen.v b/lib/coq/bv/BV_Gen.v
index a8685281cde29ade4c75e69ec4abcc8d832060fe..f30132285d45a6fc471c6bbb25418124e313b007 100644
--- a/lib/coq/bv/BV_Gen.v
+++ b/lib/coq/bv/BV_Gen.v
@@ -212,8 +212,8 @@ omega.
 Qed.
 
 (* Why3 goal *)
-Lemma nth_out_of_bound : forall (x:t) (n:Z), ((n < 0%Z)%Z \/
-  (size <= n)%Z) -> ((nth x n) = false).
+Lemma nth_out_of_bound :
+  forall (x:t) (n:Z), ((n < 0%Z)%Z \/ (size <= n)%Z) -> ((nth x n) = false).
 intros.
 unfold nth.
 rewrite nth_aux_out_of_bound; auto with zarith.
@@ -1202,8 +1202,8 @@ Lemma to_int_def : forall (x:t), ((is_signed_positive x) ->
 Qed.
 
 (* Why3 goal *)
-Lemma to_uint_extensionality : forall (v:t) (v':t),
-  ((to_uint v) = (to_uint v')) -> (v = v').
+Lemma to_uint_extensionality :
+  forall (v:t) (v':t), ((to_uint v) = (to_uint v')) -> (v = v').
   unfold to_uint.
   intros v v'.
   rewrite Nat2Z.inj_iff.
@@ -1211,8 +1211,8 @@ Lemma to_uint_extensionality : forall (v:t) (v':t),
 Qed.
 
 (* Why3 goal *)
-Lemma to_int_extensionality : forall (v:t) (v':t),
-  ((to_int v) = (to_int v')) -> (v = v').
+Lemma to_int_extensionality :
+  forall (v:t) (v':t), ((to_int v) = (to_int v')) -> (v = v').
   apply twos_complement_extensionality.
 Qed.
 
@@ -1220,8 +1220,8 @@ Qed.
 Definition uint_in_range (i:Z) : Prop := (0%Z <= i)%Z /\ (i <= max_int)%Z.
 
 (* Why3 goal *)
-Lemma to_uint_bounds : forall (v:t), (0%Z <= (to_uint v))%Z /\
-  ((to_uint v) < two_power_size)%Z.
+Lemma to_uint_bounds :
+  forall (v:t), (0%Z <= (to_uint v))%Z /\ ((to_uint v) < two_power_size)%Z.
   intros v.
   unfold to_uint, uint_in_range.
   split.
@@ -1430,8 +1430,8 @@ Lemma zeros_sign_false: Bsign last_bit zeros = false.
 Qed.
 
 (* Why3 goal *)
-Lemma positive_is_ge_zeros : forall (x:t), (is_signed_positive x) <-> (sge x
-  zeros).
+Lemma positive_is_ge_zeros :
+  forall (x:t), (is_signed_positive x) <-> (sge x zeros).
   intros.
   unfold is_signed_positive, sge, to_int, twos_complement, size_nat.
   rewrite zeros_sign_false. destruct Bsign.
@@ -1586,8 +1586,8 @@ Definition lsr_bv : t -> t -> t.
 Defined.
 
 (* Why3 goal *)
-Lemma lsr_bv_is_lsr : forall (x:t) (n:t), ((lsr_bv x n) = (lsr x
-  (to_uint n))).
+Lemma lsr_bv_is_lsr :
+  forall (x:t) (n:t), ((lsr_bv x n) = (lsr x (to_uint n))).
   easy.
 Qed.
 
@@ -1616,8 +1616,8 @@ Definition lsl_bv : t -> t -> t.
 Defined.
 
 (* Why3 goal *)
-Lemma lsl_bv_is_lsl : forall (x:t) (n:t), ((lsl_bv x n) = (lsl x
-  (to_uint n))).
+Lemma lsl_bv_is_lsl :
+  forall (x:t) (n:t), ((lsl_bv x n) = (lsl x (to_uint n))).
   easy.
 Qed.
 
@@ -1640,14 +1640,14 @@ Definition rotate_left_bv : t -> t -> t.
 Defined.
 
 (* Why3 goal *)
-Lemma rotate_left_bv_is_rotate_left : forall (v:t) (n:t), ((rotate_left_bv v
-  n) = (rotate_left v (to_uint n))).
+Lemma rotate_left_bv_is_rotate_left :
+  forall (v:t) (n:t), ((rotate_left_bv v n) = (rotate_left v (to_uint n))).
 trivial.
 Qed.
 
 (* Why3 goal *)
-Lemma rotate_right_bv_is_rotate_right : forall (v:t) (n:t),
-  ((rotate_right_bv v n) = (rotate_right v (to_uint n))).
+Lemma rotate_right_bv_is_rotate_right :
+  forall (v:t) (n:t), ((rotate_right_bv v n) = (rotate_right v (to_uint n))).
 trivial.
 Qed.
 
diff --git a/lib/coq/ieee_float/Float32.v b/lib/coq/ieee_float/Float32.v
index 5fc132b5815f274b9827d62a1e9ca3756847c139..3919e5013c803c58532f4e05b0c7c3e83e7a3b4a 100644
--- a/lib/coq/ieee_float/Float32.v
+++ b/lib/coq/ieee_float/Float32.v
@@ -255,8 +255,8 @@ Proof.
 Qed.
 
 (* Why3 goal *)
-Lemma zero_to_real : forall (x:t), (is_zero x) <-> ((t'isFinite x) /\
-  ((t'real x) = 0%R)).
+Lemma zero_to_real :
+  forall (x:t), (is_zero x) <-> ((t'isFinite x) /\ ((t'real x) = 0%R)).
 Proof.
   apply zero_to_real.
 Qed.
@@ -274,8 +274,8 @@ Proof.
 Defined.
 
 (* Why3 goal *)
-Lemma zero_of_int : forall (m:ieee_float.RoundingMode.mode),
-  (zeroF = (of_int m 0%Z)).
+Lemma zero_of_int :
+  forall (m:ieee_float.RoundingMode.mode), (zeroF = (of_int m 0%Z)).
 Proof.
   apply zero_of_int.
 Qed.
@@ -302,7 +302,8 @@ Proof.
 Defined.
 
 (* Why3 goal *)
-Lemma max_real_int : ((33554430 * 10141204801825835211973625643008)%R = (BuiltIn.IZR max_int)).
+Lemma max_real_int :
+  ((33554430 * 10141204801825835211973625643008)%R = (BuiltIn.IZR max_int)).
 Proof.
   unfold max_int.
   now rewrite mult_IZR, <- !Z2R_IZR.
@@ -314,8 +315,8 @@ Definition in_range (x:R) : Prop :=
   (x <= (33554430 * 10141204801825835211973625643008)%R)%R.
 
 (* Why3 assumption *)
-Definition in_int_range (i:Z): Prop := ((-max_int)%Z <= i)%Z /\
-  (i <= max_int)%Z.
+Definition in_int_range (i:Z) : Prop :=
+  ((-max_int)%Z <= i)%Z /\ (i <= max_int)%Z.
 
 (* Why3 goal *)
 Lemma is_finite : forall (x:t), (t'isFinite x) -> (in_range (t'real x)).
@@ -362,15 +363,15 @@ Proof.
 Qed.
 
 (* Why3 goal *)
-Lemma Round_down_le : forall (x:R), ((round ieee_float.RoundingMode.RTN
-  x) <= x)%R.
+Lemma Round_down_le :
+  forall (x:R), ((round ieee_float.RoundingMode.RTN x) <= x)%R.
 Proof.
   apply Round_down_le.
 Qed.
 
 (* Why3 goal *)
-Lemma Round_up_ge : forall (x:R), (x <= (round ieee_float.RoundingMode.RTP
-  x))%R.
+Lemma Round_up_ge :
+  forall (x:R), (x <= (round ieee_float.RoundingMode.RTP x))%R.
 Proof.
   apply Round_up_ge.
 Qed.
@@ -390,8 +391,8 @@ Proof.
 Qed.
 
 (* Why3 assumption *)
-Definition in_safe_int_range (i:Z): Prop := ((-16777216%Z)%Z <= i)%Z /\
-  (i <= 16777216%Z)%Z.
+Definition in_safe_int_range (i:Z) : Prop :=
+  ((-16777216%Z)%Z <= i)%Z /\ (i <= 16777216%Z)%Z.
 
 (* Why3 goal *)
 Lemma Exact_rounding_for_integers : forall (m:ieee_float.RoundingMode.mode)
@@ -403,12 +404,14 @@ Proof.
 Qed.
 
 (* Why3 assumption *)
-Definition same_sign (x:t) (y:t): Prop := ((is_positive x) /\ (is_positive
-  y)) \/ ((is_negative x) /\ (is_negative y)).
+Definition same_sign (x:t) (y:t) : Prop :=
+  ((is_positive x) /\ (is_positive y)) \/
+  ((is_negative x) /\ (is_negative y)).
 
 (* Why3 assumption *)
-Definition diff_sign (x:t) (y:t): Prop := ((is_positive x) /\ (is_negative
-  y)) \/ ((is_negative x) /\ (is_positive y)).
+Definition diff_sign (x:t) (y:t) : Prop :=
+  ((is_positive x) /\ (is_negative y)) \/
+  ((is_negative x) /\ (is_positive y)).
 
 (* Why3 goal *)
 Lemma feq_eq : forall (x:t) (y:t), (t'isFinite x) -> ((t'isFinite y) ->
@@ -530,50 +533,50 @@ Proof.
 Qed.
 
 (* Why3 goal *)
-Lemma lt_lt_finite : forall (x:t) (y:t) (z:t), (lt x y) -> ((lt y z) ->
-  (t'isFinite y)).
+Lemma lt_lt_finite :
+  forall (x:t) (y:t) (z:t), (lt x y) -> ((lt y z) -> (t'isFinite y)).
 Proof.
   apply lt_lt_finite.
 Qed.
 
 (* Why3 goal *)
-Lemma positive_to_real : forall (x:t), (t'isFinite x) -> ((is_positive x) ->
-  (0%R <= (t'real x))%R).
+Lemma positive_to_real :
+  forall (x:t), (t'isFinite x) -> ((is_positive x) -> (0%R <= (t'real x))%R).
 Proof.
   apply positive_to_real.
 Qed.
 
 (* Why3 goal *)
-Lemma to_real_positive : forall (x:t), (t'isFinite x) ->
-  ((0%R < (t'real x))%R -> (is_positive x)).
+Lemma to_real_positive :
+  forall (x:t), (t'isFinite x) -> ((0%R < (t'real x))%R -> (is_positive x)).
 Proof.
   apply to_real_positive.
 Qed.
 
 (* Why3 goal *)
-Lemma negative_to_real : forall (x:t), (t'isFinite x) -> ((is_negative x) ->
-  ((t'real x) <= 0%R)%R).
+Lemma negative_to_real :
+  forall (x:t), (t'isFinite x) -> ((is_negative x) -> ((t'real x) <= 0%R)%R).
 Proof.
   apply negative_to_real.
 Qed.
 
 (* Why3 goal *)
-Lemma to_real_negative : forall (x:t), (t'isFinite x) ->
-  (((t'real x) < 0%R)%R -> (is_negative x)).
+Lemma to_real_negative :
+  forall (x:t), (t'isFinite x) -> (((t'real x) < 0%R)%R -> (is_negative x)).
 Proof.
   apply to_real_negative.
 Qed.
 
 (* Why3 goal *)
-Lemma negative_xor_positive : forall (x:t), ~ ((is_positive x) /\
-  (is_negative x)).
+Lemma negative_xor_positive :
+  forall (x:t), ~ ((is_positive x) /\ (is_negative x)).
 Proof.
   apply negative_xor_positive.
 Qed.
 
 (* Why3 goal *)
-Lemma negative_or_positive : forall (x:t), (is_not_nan x) -> ((is_positive
-  x) \/ (is_negative x)).
+Lemma negative_or_positive :
+  forall (x:t), (is_not_nan x) -> ((is_positive x) \/ (is_negative x)).
 Proof.
   apply negative_or_positive.
 Qed.
@@ -600,8 +603,9 @@ Proof.
 Qed.
 
 (* Why3 assumption *)
-Definition product_sign (z:t) (x:t) (y:t): Prop := ((same_sign x y) ->
-  (is_positive z)) /\ ((diff_sign x y) -> (is_negative z)).
+Definition product_sign (z:t) (x:t) (y:t) : Prop :=
+  ((same_sign x y) -> (is_positive z)) /\
+  ((diff_sign x y) -> (is_negative z)).
 
 (* Why3 assumption *)
 Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t): Prop :=
@@ -621,7 +625,7 @@ Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t): Prop :=
   end.
 
 (* Why3 assumption *)
-Definition sign_zero_result (m:ieee_float.RoundingMode.mode) (x:t): Prop :=
+Definition sign_zero_result (m:ieee_float.RoundingMode.mode) (x:t) : Prop :=
   (is_zero x) ->
   match m with
   | ieee_float.RoundingMode.RTN => (is_negative x)
diff --git a/lib/coq/ieee_float/Float64.v b/lib/coq/ieee_float/Float64.v
index 1ba36351778f0bf52e502df6d8297b44813d36d7..d0e3d03207ea8b37bc540883072ed64c824d3124 100644
--- a/lib/coq/ieee_float/Float64.v
+++ b/lib/coq/ieee_float/Float64.v
@@ -274,8 +274,8 @@ Proof.
 Defined.
 
 (* Why3 goal *)
-Lemma zero_of_int : forall (m:ieee_float.RoundingMode.mode),
-  (zeroF = (of_int m 0%Z)).
+Lemma zero_of_int :
+  forall (m:ieee_float.RoundingMode.mode), (zeroF = (of_int m 0%Z)).
 Proof.
   apply zero_of_int.
 Qed.
@@ -402,12 +402,14 @@ Proof.
 Qed.
 
 (* Why3 assumption *)
-Definition same_sign (x:t) (y:t): Prop := ((is_positive x) /\ (is_positive
-  y)) \/ ((is_negative x) /\ (is_negative y)).
+Definition same_sign (x:t) (y:t) : Prop :=
+  ((is_positive x) /\ (is_positive y)) \/
+  ((is_negative x) /\ (is_negative y)).
 
 (* Why3 assumption *)
-Definition diff_sign (x:t) (y:t): Prop := ((is_positive x) /\ (is_negative
-  y)) \/ ((is_negative x) /\ (is_positive y)).
+Definition diff_sign (x:t) (y:t) : Prop :=
+  ((is_positive x) /\ (is_negative y)) \/
+  ((is_negative x) /\ (is_positive y)).
 
 (* Why3 goal *)
 Lemma feq_eq : forall (x:t) (y:t), (t'isFinite x) -> ((t'isFinite y) ->
@@ -529,50 +531,50 @@ Proof.
 Qed.
 
 (* Why3 goal *)
-Lemma lt_lt_finite : forall (x:t) (y:t) (z:t), (lt x y) -> ((lt y z) ->
-  (t'isFinite y)).
+Lemma lt_lt_finite :
+  forall (x:t) (y:t) (z:t), (lt x y) -> ((lt y z) -> (t'isFinite y)).
 Proof.
   apply lt_lt_finite.
 Qed.
 
 (* Why3 goal *)
-Lemma positive_to_real : forall (x:t), (t'isFinite x) -> ((is_positive x) ->
-  (0%R <= (t'real x))%R).
+Lemma positive_to_real :
+  forall (x:t), (t'isFinite x) -> ((is_positive x) -> (0%R <= (t'real x))%R).
 Proof.
   apply positive_to_real.
 Qed.
 
 (* Why3 goal *)
-Lemma to_real_positive : forall (x:t), (t'isFinite x) ->
-  ((0%R < (t'real x))%R -> (is_positive x)).
+Lemma to_real_positive :
+  forall (x:t), (t'isFinite x) -> ((0%R < (t'real x))%R -> (is_positive x)).
 Proof.
   apply to_real_positive.
 Qed.
 
 (* Why3 goal *)
-Lemma negative_to_real : forall (x:t), (t'isFinite x) -> ((is_negative x) ->
-  ((t'real x) <= 0%R)%R).
+Lemma negative_to_real :
+  forall (x:t), (t'isFinite x) -> ((is_negative x) -> ((t'real x) <= 0%R)%R).
 Proof.
   apply negative_to_real.
 Qed.
 
 (* Why3 goal *)
-Lemma to_real_negative : forall (x:t), (t'isFinite x) ->
-  (((t'real x) < 0%R)%R -> (is_negative x)).
+Lemma to_real_negative :
+  forall (x:t), (t'isFinite x) -> (((t'real x) < 0%R)%R -> (is_negative x)).
 Proof.
   apply to_real_negative.
 Qed.
 
 (* Why3 goal *)
-Lemma negative_xor_positive : forall (x:t), ~ ((is_positive x) /\
-  (is_negative x)).
+Lemma negative_xor_positive :
+  forall (x:t), ~ ((is_positive x) /\ (is_negative x)).
 Proof.
   apply negative_xor_positive.
 Qed.
 
 (* Why3 goal *)
-Lemma negative_or_positive : forall (x:t), (is_not_nan x) -> ((is_positive
-  x) \/ (is_negative x)).
+Lemma negative_or_positive :
+  forall (x:t), (is_not_nan x) -> ((is_positive x) \/ (is_negative x)).
 Proof.
   apply negative_or_positive.
 Qed.
@@ -599,8 +601,9 @@ Proof.
 Qed.
 
 (* Why3 assumption *)
-Definition product_sign (z:t) (x:t) (y:t): Prop := ((same_sign x y) ->
-  (is_positive z)) /\ ((diff_sign x y) -> (is_negative z)).
+Definition product_sign (z:t) (x:t) (y:t) : Prop :=
+  ((same_sign x y) -> (is_positive z)) /\
+  ((diff_sign x y) -> (is_negative z)).
 
 (* Why3 assumption *)
 Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t): Prop :=
diff --git a/lib/coq/ieee_float/GenericFloat.v b/lib/coq/ieee_float/GenericFloat.v
index 4db31c53b5b07927eaf7396a1710880a58ec65ad..526426efc4f8d24cf632b2681dd7c396bcfbe301 100644
--- a/lib/coq/ieee_float/GenericFloat.v
+++ b/lib/coq/ieee_float/GenericFloat.v
@@ -782,8 +782,8 @@ Proof.
 Qed.
 
 (* Why3 goal *)
-Lemma zero_to_real : forall (x:t), (is_zero x) <-> ((is_finite x) /\
-  ((to_real x) = 0%R)).
+Lemma zero_to_real :
+  forall (x:t), (is_zero x) <-> ((is_finite x) /\ ((to_real x) = 0%R)).
 Proof.
   unfold is_zero.
   assert (is_finite zeroF) by easy.
@@ -856,8 +856,8 @@ Proof.
 Qed.
 
 (* Why3 goal *)
-Lemma zero_of_int : forall (m:ieee_float.RoundingMode.mode),
-  (zeroF = (of_int m 0%Z)).
+Lemma zero_of_int :
+  forall (m:ieee_float.RoundingMode.mode), (zeroF = (of_int m 0%Z)).
 Proof.
 auto.
 Qed.
@@ -1699,8 +1699,8 @@ destruct x, y, z; destruct b, b0, b1; easy.
 Qed.
 
 (* Why3 goal *)
-Lemma positive_to_real : forall (x:t), (is_finite x) -> ((is_positive x) ->
-  (0%R <= (to_real x))%R).
+Lemma positive_to_real :
+  forall (x:t), (is_finite x) -> ((is_positive x) -> (0%R <= (to_real x))%R).
 Proof.
   intros x h1 h2.
   assert (is_finite zeroF) as zero_is_finite by easy.
@@ -1731,8 +1731,8 @@ Proof.
 Qed.
 
 (* Why3 goal *)
-Lemma to_real_positive : forall (x:t), (is_finite x) ->
-  ((0%R < (to_real x))%R -> (is_positive x)).
+Lemma to_real_positive :
+  forall (x:t), (is_finite x) -> ((0%R < (to_real x))%R -> (is_positive x)).
 Proof.
   intros x h1 h2.
   assert (is_finite zeroF) as zero_is_finite by easy.
@@ -1741,8 +1741,8 @@ Proof.
 Qed.
 
 (* Why3 goal *)
-Lemma negative_to_real : forall (x:t), (is_finite x) -> ((is_negative x) ->
-  ((to_real x) <= 0%R)%R).
+Lemma negative_to_real :
+  forall (x:t), (is_finite x) -> ((is_negative x) -> ((to_real x) <= 0%R)%R).
 Proof.
   intros x h1 h2.
   assert (is_finite zeroF) as zero_is_finite by easy.
@@ -1773,8 +1773,8 @@ Proof.
 Qed.
 
 (* Why3 goal *)
-Lemma to_real_negative : forall (x:t), (is_finite x) ->
-  (((to_real x) < 0%R)%R -> (is_negative x)).
+Lemma to_real_negative :
+  forall (x:t), (is_finite x) -> (((to_real x) < 0%R)%R -> (is_negative x)).
 Proof.
   intros x h1 h2.
   assert (is_finite zeroF) as zero_is_finite by easy.
@@ -1783,16 +1783,16 @@ Proof.
 Qed.
 
 (* Why3 goal *)
-Lemma negative_xor_positive : forall (x:t), ~ ((is_positive x) /\
-  (is_negative x)).
+Lemma negative_xor_positive :
+  forall (x:t), ~ ((is_positive x) /\ (is_negative x)).
 Proof.
 intros x.
 destruct x ; destruct b; easy.
 Qed.
 
 (* Why3 goal *)
-Lemma negative_or_positive : forall (x:t), (is_not_nan x) -> ((is_positive
-  x) \/ (is_negative x)).
+Lemma negative_or_positive :
+  forall (x:t), (is_not_nan x) -> ((is_positive x) \/ (is_negative x)).
 Proof.
 intros x h1.
 destruct x ; destruct b; simpl; auto; now elim h1.
@@ -1868,7 +1868,7 @@ Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t) : Prop :=
   end.
 
 (* Why3 assumption *)
-Definition sign_zero_result (m:ieee_float.RoundingMode.mode) (x:t): Prop :=
+Definition sign_zero_result (m:ieee_float.RoundingMode.mode) (x:t) : Prop :=
   (is_zero x) ->
   match m with
   | ieee_float.RoundingMode.RTN => (is_negative x)
@@ -3507,7 +3507,7 @@ Proof.
 Qed.
 
 (* Why3 goal *)
-Definition is_int: t -> Prop.
+Definition is_int : t -> Prop.
 Proof.
  exact (fun x => is_finite x /\ is_intR (to_real x)).
 Defined.
diff --git a/lib/coq/int/Exponentiation.v b/lib/coq/int/Exponentiation.v
index 4da4fa48032ba81426f5eb698e54790418742885..d2a18d02bd8277a8d1c984c48afcd7f2cb2edc23 100644
--- a/lib/coq/int/Exponentiation.v
+++ b/lib/coq/int/Exponentiation.v
@@ -52,8 +52,9 @@ easy.
 Qed.
 
 (* Why3 goal *)
-Lemma Power_s : forall (x:t) (n:Z), (0%Z <= n)%Z -> ((power x
-  (n + 1%Z)%Z) = (infix_as x (power x n))).
+Lemma Power_s :
+  forall (x:t) (n:Z),
+  (0%Z <= n)%Z -> ((power x (n + 1%Z)%Z) = (infix_as x (power x n))).
 Proof.
 intros x n h1.
 unfold power.
@@ -62,8 +63,9 @@ now rewrite Zabs_nat_Zsucc.
 Qed.
 
 (* Why3 goal *)
-Lemma Power_s_alt : forall (x:t) (n:Z), (0%Z < n)%Z -> ((power x
-  n) = (infix_as x (power x (n - 1%Z)%Z))).
+Lemma Power_s_alt :
+  forall (x:t) (n:Z),
+  (0%Z < n)%Z -> ((power x n) = (infix_as x (power x (n - 1%Z)%Z))).
 Proof.
 intros x n h1.
 rewrite <- Power_s; auto with zarith.
diff --git a/lib/coq/int/Int.v b/lib/coq/int/Int.v
index 58bae08fe3f315cbba38bd2011b2565e9b57d7d1..5a2aaec7283468955443a2763c4506ccd9486c09 100644
--- a/lib/coq/int/Int.v
+++ b/lib/coq/int/Int.v
@@ -38,8 +38,8 @@ exact Zle_lt_or_eq_iff.
 Qed.
 
 (* Why3 goal *)
-Lemma Assoc : forall (x:Z) (y:Z) (z:Z),
-  (((x + y)%Z + z)%Z = (x + (y + z)%Z)%Z).
+Lemma Assoc :
+  forall (x:Z) (y:Z) (z:Z), (((x + y)%Z + z)%Z = (x + (y + z)%Z)%Z).
 Proof.
 intros x y z.
 apply sym_eq.
@@ -77,8 +77,8 @@ exact Zplus_comm.
 Qed.
 
 (* Why3 goal *)
-Lemma Assoc1 : forall (x:Z) (y:Z) (z:Z),
-  (((x * y)%Z * z)%Z = (x * (y * z)%Z)%Z).
+Lemma Assoc1 :
+  forall (x:Z) (y:Z) (z:Z), (((x * y)%Z * z)%Z = (x * (y * z)%Z)%Z).
 Proof.
 intros x y z.
 apply sym_eq.
@@ -86,16 +86,16 @@ apply Zmult_assoc.
 Qed.
 
 (* Why3 goal *)
-Lemma Mul_distr_l : forall (x:Z) (y:Z) (z:Z),
-  ((x * (y + z)%Z)%Z = ((x * y)%Z + (x * z)%Z)%Z).
+Lemma Mul_distr_l :
+  forall (x:Z) (y:Z) (z:Z), ((x * (y + z)%Z)%Z = ((x * y)%Z + (x * z)%Z)%Z).
 Proof.
 intros x y z.
 apply Zmult_plus_distr_r.
 Qed.
 
 (* Why3 goal *)
-Lemma Mul_distr_r : forall (x:Z) (y:Z) (z:Z),
-  (((y + z)%Z * x)%Z = ((y * x)%Z + (z * x)%Z)%Z).
+Lemma Mul_distr_r :
+  forall (x:Z) (y:Z) (z:Z), (((y + z)%Z * x)%Z = ((y * x)%Z + (z * x)%Z)%Z).
 Proof.
 intros x y z.
 apply Zmult_plus_distr_l.
@@ -127,8 +127,8 @@ apply Zle_refl.
 Qed.
 
 (* Why3 goal *)
-Lemma Trans : forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> ((y <= z)%Z ->
-  (x <= z)%Z).
+Lemma Trans :
+  forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> ((y <= z)%Z -> (x <= z)%Z).
 Proof.
 exact Zle_trans.
 Qed.
@@ -158,8 +158,8 @@ now left.
 Qed.
 
 (* Why3 goal *)
-Lemma CompatOrderAdd : forall (x:Z) (y:Z) (z:Z), (x <= y)%Z ->
-  ((x + z)%Z <= (y + z)%Z)%Z.
+Lemma CompatOrderAdd :
+  forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> ((x + z)%Z <= (y + z)%Z)%Z.
 Proof.
 exact Zplus_le_compat_r.
 Qed.
diff --git a/lib/coq/number/Divisibility.v b/lib/coq/number/Divisibility.v
index a4dd2269470698cb16a8f3b9070cc1e49af05759..46b75ebb4458e21f61c405635eccae3a5021a835 100644
--- a/lib/coq/number/Divisibility.v
+++ b/lib/coq/number/Divisibility.v
@@ -22,7 +22,8 @@ Require number.Parity.
 (* Hack so that Why3 does not override the notation below.
 
 (* Why3 assumption *)
-Definition divides (d:Z) (n:Z): Prop := ((d = 0%Z) -> (n = 0%Z)) /\
+Definition divides (d:Z) (n:Z) : Prop :=
+  ((d = 0%Z) -> (n = 0%Z)) /\
   ((~ (d = 0%Z)) -> ((ZArith.BinInt.Z.rem n d) = 0%Z)).
 
 *)
@@ -31,8 +32,8 @@ Require Import Znumtheory.
 Notation divides := Zdivide (only parsing).
 
 (* Why3 goal *)
-Lemma divides_spec : forall (d:Z) (n:Z), (divides d n) <-> exists q:Z,
-  (n = (q * d)%Z).
+Lemma divides_spec :
+  forall (d:Z) (n:Z), (divides d n) <-> exists q:Z, (n = (q * d)%Z).
 Proof.
 intros d n.
 easy.
@@ -57,15 +58,15 @@ exact Zdivide_0.
 Qed.
 
 (* Why3 goal *)
-Lemma divides_left : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides
-  (c * a)%Z (c * b)%Z).
+Lemma divides_left :
+  forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides (c * a)%Z (c * b)%Z).
 Proof.
 exact Zmult_divide_compat_l.
 Qed.
 
 (* Why3 goal *)
-Lemma divides_right : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides
-  (a * c)%Z (b * c)%Z).
+Lemma divides_right :
+  forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides (a * c)%Z (b * c)%Z).
 Proof.
 exact Zmult_divide_compat_r.
 Qed.
@@ -83,15 +84,15 @@ exact Zdivide_opp_l.
 Qed.
 
 (* Why3 goal *)
-Lemma divides_oppr_rev : forall (a:Z) (b:Z), (divides (-a)%Z b) -> (divides a
-  b).
+Lemma divides_oppr_rev :
+  forall (a:Z) (b:Z), (divides (-a)%Z b) -> (divides a b).
 Proof.
 exact Zdivide_opp_l_rev.
 Qed.
 
 (* Why3 goal *)
-Lemma divides_oppl_rev : forall (a:Z) (b:Z), (divides a (-b)%Z) -> (divides a
-  b).
+Lemma divides_oppl_rev :
+  forall (a:Z) (b:Z), (divides a (-b)%Z) -> (divides a b).
 Proof.
 exact Zdivide_opp_r_rev.
 Qed.
@@ -111,16 +112,16 @@ exact Zdivide_minus_l.
 Qed.
 
 (* Why3 goal *)
-Lemma divides_multl : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides a
-  (c * b)%Z).
+Lemma divides_multl :
+  forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides a (c * b)%Z).
 Proof.
 intros a b c.
 apply Zdivide_mult_r.
 Qed.
 
 (* Why3 goal *)
-Lemma divides_multr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides a
-  (b * c)%Z).
+Lemma divides_multr :
+  forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides a (b * c)%Z).
 Proof.
 exact Zdivide_mult_l.
 Qed.
@@ -138,8 +139,8 @@ exact Zdivide_factor_r.
 Qed.
 
 (* Why3 goal *)
-Lemma divides_n_1 : forall (n:Z), (divides n 1%Z) -> ((n = 1%Z) \/
-  (n = (-1%Z)%Z)).
+Lemma divides_n_1 :
+  forall (n:Z), (divides n 1%Z) -> ((n = 1%Z) \/ (n = (-1%Z)%Z)).
 Proof.
 exact Zdivide_1.
 Qed.
@@ -152,8 +153,8 @@ exact Zdivide_antisym.
 Qed.
 
 (* Why3 goal *)
-Lemma divides_trans : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides b
-  c) -> (divides a c)).
+Lemma divides_trans :
+  forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides b c) -> (divides a c)).
 Proof.
 exact Zdivide_trans.
 Qed.
@@ -213,16 +214,16 @@ apply Zquot.Z_rem_mult.
 Qed.
 
 (* Why3 goal *)
-Lemma even_divides : forall (a:Z), (number.Parity.even a) <-> (divides 2%Z
-  a).
+Lemma even_divides :
+  forall (a:Z), (number.Parity.even a) <-> (divides 2%Z a).
 Proof.
 split ;
   intros (q,H) ; exists q ; now rewrite Zmult_comm.
 Qed.
 
 (* Why3 goal *)
-Lemma odd_divides : forall (a:Z), (number.Parity.odd a) <-> ~ (divides 2%Z
-  a).
+Lemma odd_divides :
+  forall (a:Z), (number.Parity.odd a) <-> ~ (divides 2%Z a).
 Proof.
 split.
 intros H.
diff --git a/lib/coq/number/Gcd.v b/lib/coq/number/Gcd.v
index d75437f38c10b296b1d46e9edd1326efe695ebe8..74ad37bd626f94a00a0811dfe2abd0e8037a2b30 100644
--- a/lib/coq/number/Gcd.v
+++ b/lib/coq/number/Gcd.v
@@ -112,8 +112,8 @@ apply Zgcd_is_gcd.
 Qed.
 
 (* Why3 goal *)
-Lemma gcd_euclid : forall (a:Z) (b:Z) (q:Z), ((gcd a b) = (gcd a
-  (b - (q * a)%Z)%Z)).
+Lemma gcd_euclid :
+  forall (a:Z) (b:Z) (q:Z), ((gcd a b) = (gcd a (b - (q * a)%Z)%Z)).
 Proof.
 intros a b c.
 apply Zis_gcd_gcd.
diff --git a/lib/coq/number/Prime.v b/lib/coq/number/Prime.v
index 89281b1b7ac23b158ac38faf6c80a6ab56e2054f..58d9389dee491d61fb160542214be13af05fc731 100644
--- a/lib/coq/number/Prime.v
+++ b/lib/coq/number/Prime.v
@@ -161,8 +161,8 @@ exact Hy2.
 Qed.
 
 (* Why3 goal *)
-Lemma even_prime : forall (p:Z), (prime p) -> ((number.Parity.even p) ->
-  (p = 2%Z)).
+Lemma even_prime :
+  forall (p:Z), (prime p) -> ((number.Parity.even p) -> (p = 2%Z)).
 Proof.
 intros p Pp (q,Hq).
 generalize (proj2 Pp q).
@@ -180,8 +180,8 @@ easy.
 Qed.
 
 (* Why3 goal *)
-Lemma odd_prime : forall (p:Z), (prime p) -> ((3%Z <= p)%Z ->
-  (number.Parity.odd p)).
+Lemma odd_prime :
+  forall (p:Z), (prime p) -> ((3%Z <= p)%Z -> (number.Parity.odd p)).
 Proof.
 intros p Pp Hp.
 apply <- Divisibility.odd_divides.
diff --git a/lib/coq/real/ExpLog.v b/lib/coq/real/ExpLog.v
index dbf34109bea3151824a5fe1a7ae2599525327622..3d3b2254778ecd8d1963c33f01867c082f26c8ed 100644
--- a/lib/coq/real/ExpLog.v
+++ b/lib/coq/real/ExpLog.v
@@ -64,9 +64,9 @@ exact exp_ln.
 Qed.
 
 (* Why3 assumption *)
-Definition log2 (x:R): R := ((Reals.Rpower.ln x) / (Reals.Rpower.ln 2%R))%R.
+Definition log2 (x:R) : R := ((Reals.Rpower.ln x) / (Reals.Rpower.ln 2%R))%R.
 
 (* Why3 assumption *)
-Definition log10 (x:R): R :=
+Definition log10 (x:R) : R :=
   ((Reals.Rpower.ln x) / (Reals.Rpower.ln 10%R))%R.
 
diff --git a/lib/coq/real/FromInt.v b/lib/coq/real/FromInt.v
index 7bc889e47b3653fe6beb0fbdbf5d0f8e7275da7e..2bf0ad35c49b7e1f0a27035f2e2fc8abef97ca5c 100644
--- a/lib/coq/real/FromInt.v
+++ b/lib/coq/real/FromInt.v
@@ -59,8 +59,8 @@ exact opp_IZR.
 Qed.
 
 (* Why3 goal *)
-Lemma Monotonic : forall (x:Z) (y:Z), (x <= y)%Z ->
-  ((BuiltIn.IZR x) <= (BuiltIn.IZR y))%R.
+Lemma Monotonic :
+  forall (x:Z) (y:Z), (x <= y)%Z -> ((BuiltIn.IZR x) <= (BuiltIn.IZR y))%R.
 Proof.
 exact (IZR_le).
 Qed.
diff --git a/lib/coq/real/MinMax.v b/lib/coq/real/MinMax.v
index dfaadbaa169a857630f1cd90f0681380e7985cb3..fb52009b2cfc10bd58022c37768282ab9d645d3c 100644
--- a/lib/coq/real/MinMax.v
+++ b/lib/coq/real/MinMax.v
@@ -21,9 +21,10 @@ Require Import Rbasic_fun.
 (* min is replaced with (Reals.Rbasic_fun.Rmin x x1) by the coq driver *)
 
 (* Why3 goal *)
-Lemma min_def : forall (x:R) (y:R), ((x <= y)%R ->
-  ((Reals.Rbasic_fun.Rmin x y) = x)) /\ ((~ (x <= y)%R) ->
-  ((Reals.Rbasic_fun.Rmin x y) = y)).
+Lemma min_def :
+  forall (x:R) (y:R),
+  ((x <= y)%R -> ((Reals.Rbasic_fun.Rmin x y) = x)) /\
+  ((~ (x <= y)%R) -> ((Reals.Rbasic_fun.Rmin x y) = y)).
 Proof.
 intros x y.
 split ; intros H.
@@ -36,9 +37,10 @@ Qed.
 (* max is replaced with (Reals.Rbasic_fun.Rmax x x1) by the coq driver *)
 
 (* Why3 goal *)
-Lemma max_def : forall (x:R) (y:R), ((x <= y)%R ->
-  ((Reals.Rbasic_fun.Rmax x y) = y)) /\ ((~ (x <= y)%R) ->
-  ((Reals.Rbasic_fun.Rmax x y) = x)).
+Lemma max_def :
+  forall (x:R) (y:R),
+  ((x <= y)%R -> ((Reals.Rbasic_fun.Rmax x y) = y)) /\
+  ((~ (x <= y)%R) -> ((Reals.Rbasic_fun.Rmax x y) = x)).
 Proof.
 intros x y.
 split ; intros H.
@@ -48,14 +50,14 @@ now apply Rlt_le, Rnot_le_lt.
 Qed.
 
 (* Why3 goal *)
-Lemma Min_r : forall (x:R) (y:R), (y <= x)%R ->
-  ((Reals.Rbasic_fun.Rmin x y) = y).
+Lemma Min_r :
+  forall (x:R) (y:R), (y <= x)%R -> ((Reals.Rbasic_fun.Rmin x y) = y).
 exact Rmin_right.
 Qed.
 
 (* Why3 goal *)
-Lemma Max_l : forall (x:R) (y:R), (y <= x)%R ->
-  ((Reals.Rbasic_fun.Rmax x y) = x).
+Lemma Max_l :
+  forall (x:R) (y:R), (y <= x)%R -> ((Reals.Rbasic_fun.Rmax x y) = x).
 exact Rmax_left.
 Qed.
 
diff --git a/lib/coq/real/PowerReal.v b/lib/coq/real/PowerReal.v
index bf191f25188eaff38782a2a0f89e3bc95447f681..b4de1f821a0b74ba53a3e5860058ff8a96de7568 100644
--- a/lib/coq/real/PowerReal.v
+++ b/lib/coq/real/PowerReal.v
@@ -33,8 +33,8 @@ easy.
 Qed.
 
 (* Why3 goal *)
-Lemma Pow_pos : forall (x:R) (y:R), (0%R < x)%R ->
-  (0%R < (Reals.Rpower.Rpower x y))%R.
+Lemma Pow_pos :
+  forall (x:R) (y:R), (0%R < x)%R -> (0%R < (Reals.Rpower.Rpower x y))%R.
 Proof.
 intros x y h1.
 apply Exp_prop.exp_pos.
@@ -57,16 +57,16 @@ now apply Rpower_mult.
 Qed.
 
 (* Why3 goal *)
-Lemma Pow_x_zero : forall (x:R), (0%R < x)%R ->
-  ((Reals.Rpower.Rpower x 0%R) = 1%R).
+Lemma Pow_x_zero :
+  forall (x:R), (0%R < x)%R -> ((Reals.Rpower.Rpower x 0%R) = 1%R).
 Proof.
 intros x h1.
 now apply Rpower_O.
 Qed.
 
 (* Why3 goal *)
-Lemma Pow_x_one : forall (x:R), (0%R < x)%R ->
-  ((Reals.Rpower.Rpower x 1%R) = x).
+Lemma Pow_x_one :
+  forall (x:R), (0%R < x)%R -> ((Reals.Rpower.Rpower x 1%R) = x).
 Proof.
 intros x h1.
 now apply Rpower_1.
diff --git a/lib/coq/real/Real.v b/lib/coq/real/Real.v
index 626f07679545164baf59624660346635aa685cb5..f93e0b98d9a320c8c39e5bc4eb831db5e91d839d 100644
--- a/lib/coq/real/Real.v
+++ b/lib/coq/real/Real.v
@@ -34,8 +34,8 @@ reflexivity.
 Qed.
 
 (* Why3 goal *)
-Lemma Assoc : forall (x:R) (y:R) (z:R),
-  (((x + y)%R + z)%R = (x + (y + z)%R)%R).
+Lemma Assoc :
+  forall (x:R) (y:R) (z:R), (((x + y)%R + z)%R = (x + (y + z)%R)%R).
 Proof.
 exact Rplus_assoc.
 Qed.
@@ -71,23 +71,23 @@ exact Rplus_comm.
 Qed.
 
 (* Why3 goal *)
-Lemma Assoc1 : forall (x:R) (y:R) (z:R),
-  (((x * y)%R * z)%R = (x * (y * z)%R)%R).
+Lemma Assoc1 :
+  forall (x:R) (y:R) (z:R), (((x * y)%R * z)%R = (x * (y * z)%R)%R).
 Proof.
 exact Rmult_assoc.
 Qed.
 
 (* Why3 goal *)
-Lemma Mul_distr_l : forall (x:R) (y:R) (z:R),
-  ((x * (y + z)%R)%R = ((x * y)%R + (x * z)%R)%R).
+Lemma Mul_distr_l :
+  forall (x:R) (y:R) (z:R), ((x * (y + z)%R)%R = ((x * y)%R + (x * z)%R)%R).
 Proof.
 intros x y z.
 apply Rmult_plus_distr_l.
 Qed.
 
 (* Why3 goal *)
-Lemma Mul_distr_r : forall (x:R) (y:R) (z:R),
-  (((y + z)%R * x)%R = ((y * x)%R + (z * x)%R)%R).
+Lemma Mul_distr_r :
+  forall (x:R) (y:R) (z:R), (((y + z)%R * x)%R = ((y * x)%R + (z * x)%R)%R).
 Proof.
 intros x y z.
 apply Rmult_plus_distr_r.
@@ -116,8 +116,8 @@ Qed.
 (* inv is replaced with (Reals.Rdefinitions.Rinv x) by the coq driver *)
 
 (* Why3 goal *)
-Lemma Inverse : forall (x:R), (~ (x = 0%R)) ->
-  ((x * (Reals.Rdefinitions.Rinv x))%R = 1%R).
+Lemma Inverse :
+  forall (x:R), (~ (x = 0%R)) -> ((x * (Reals.Rdefinitions.Rinv x))%R = 1%R).
 Proof.
 exact Rinv_r.
 Qed.
@@ -129,8 +129,8 @@ reflexivity.
 Qed.
 
 (* Why3 goal *)
-Lemma infix_sl_def : forall (x:R) (y:R),
-  ((x / y)%R = (x * (Reals.Rdefinitions.Rinv y))%R).
+Lemma infix_sl_def :
+  forall (x:R) (y:R), ((x / y)%R = (x * (Reals.Rdefinitions.Rinv y))%R).
 Proof.
 reflexivity.
 Qed.
diff --git a/lib/coq/real/Square.v b/lib/coq/real/Square.v
index 70a45a276d54df923d41d5e593683d7442b80283..4b0a2e940bd2fb9e23c0a2bb3badc991ca95c07b 100644
--- a/lib/coq/real/Square.v
+++ b/lib/coq/real/Square.v
@@ -27,8 +27,8 @@ Qed.
 (* sqrt is replaced with (Reals.R_sqrt.sqrt x) by the coq driver *)
 
 (* Why3 goal *)
-Lemma Sqrt_positive : forall (x:R), (0%R <= x)%R ->
-  (0%R <= (Reals.R_sqrt.sqrt x))%R.
+Lemma Sqrt_positive :
+  forall (x:R), (0%R <= x)%R -> (0%R <= (Reals.R_sqrt.sqrt x))%R.
 intros x _.
 apply sqrt_pos.
 Qed.
@@ -40,8 +40,8 @@ exact sqrt_sqrt.
 Qed.
 
 (* Why3 goal *)
-Lemma Square_sqrt : forall (x:R), (0%R <= x)%R ->
-  ((Reals.R_sqrt.sqrt (x * x)%R) = x).
+Lemma Square_sqrt :
+  forall (x:R), (0%R <= x)%R -> ((Reals.R_sqrt.sqrt (x * x)%R) = x).
 exact sqrt_square.
 Qed.
 
diff --git a/lib/coq/seq/Seq.v b/lib/coq/seq/Seq.v
index bc4792779d67ae9d22076f5308e783e6a7cef8d7..6228e6b2745b644db913abbb802f90509cede2aa 100644
--- a/lib/coq/seq/Seq.v
+++ b/lib/coq/seq/Seq.v
@@ -41,8 +41,9 @@ Defined.
 Hint Unfold length.
 
 (* Why3 goal *)
-Lemma length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq
-  a)), (0%Z <= (length s))%Z.
+Lemma length_nonnegative :
+  forall {a:Type} {a_WT:WhyType a},
+  forall (s:(seq a)), (0%Z <= (length s))%Z.
 intros a a_WT.
 induction s.
 auto with *.
diff --git a/lib/coq/set/Set.v b/lib/coq/set/Set.v
index 63ea978bc9dd175d59b4c680bf25f45b6cae112e..d68d1d6fc9a05a0fe5d5d4ff7894dc34ad902881 100644
--- a/lib/coq/set/Set.v
+++ b/lib/coq/set/Set.v
@@ -49,8 +49,9 @@ Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(a -> bool)) (s2:(a ->
 Notation "x == y" := (infix_eqeq x y) (at level 70, no associativity).
 
 (* Why3 goal *)
-Lemma extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a ->
-  bool)) (s2:(a -> bool)), (infix_eqeq s1 s2) -> (s1 = s2).
+Lemma extensionality :
+  forall {a:Type} {a_WT:WhyType a},
+  forall (s1:(a -> bool)) (s2:(a -> bool)), (infix_eqeq s1 s2) -> (s1 = s2).
 Proof.
 intros a a_WT s1 s2 h1.
 apply predicate_extensionality.
@@ -70,8 +71,8 @@ Definition subset {a:Type} {a_WT:WhyType a} (s1:(a -> bool)) (s2:(a ->
   bool)): Prop := forall (x:a), (mem x s1) -> (mem x s2).
 
 (* Why3 goal *)
-Lemma subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(a -> bool)),
-  (subset s s).
+Lemma subset_refl :
+  forall {a:Type} {a_WT:WhyType a}, forall (s:(a -> bool)), (subset s s).
 Proof.
 now intros a a_WT s x.
 Qed.
@@ -86,7 +87,7 @@ now apply h2, h1.
 Qed.
 
 (* Why3 assumption *)
-Definition is_empty {a:Type} {a_WT:WhyType a} (s:(a -> bool)): Prop :=
+Definition is_empty {a:Type} {a_WT:WhyType a} (s:(a -> bool)) : Prop :=
   forall (x:a), ~ (mem x s).
 
 (* Why3 goal *)
@@ -237,8 +238,8 @@ now intros [H _].
 Qed.
 
 (* Why3 goal *)
-Definition complement: forall {a:Type} {a_WT:WhyType a}, (a -> bool) -> (a ->
-  bool).
+Definition complement :
+  forall {a:Type} {a_WT:WhyType a}, (a -> bool) -> (a -> bool).
 Proof.
 intros a a_WT s.
 exact (fun x => negb (s x)).
@@ -255,7 +256,7 @@ apply Bool.negb_true_iff.
 Qed.
 
 (* Why3 goal *)
-Definition choose: forall {a:Type} {a_WT:WhyType a}, (a -> bool) -> a.
+Definition choose : forall {a:Type} {a_WT:WhyType a}, (a -> bool) -> a.
 Proof.
 intros a a_WT s.
 assert (i: inhabited a) by (apply inhabits, why_inhabitant).