diff --git a/src/subsequences.v b/src/subsequences.v
index 9cc0a80..e0e2631 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -188,7 +188,90 @@ Qed.
 
 
 (**
-   Decidability and equivalence of all definitions of a subsequence.
+   Equivalence of all definitions of a subsequence.
+*)
+
+Theorem subsequence_eq_def_1 {X: Type} :
+  forall l s : list X, subsequence l s -> subsequence2 l s.
+Proof.
+  intros l s. intro H. destruct H. destruct H. destruct H.
+
+  exists (
+    (repeat false (length x)) ++
+    (flat_map (fun e => true :: (repeat false (length e))) x0)).
+  split.
+  rewrite H0. rewrite app_length. rewrite app_length. rewrite repeat_length.
+  rewrite Nat.add_cancel_l. rewrite flat_map_length. rewrite flat_map_length.
+
+  assert (forall v (u: list X),
+    length u = length v
+    -> map (fun e => length (fst e :: snd e)) (combine u v)
+       = map (fun e => length (true :: repeat false (length e))) v).
+  intro v. induction v; intro u; intro I.
+  apply length_zero_iff_nil in I. rewrite I. reflexivity.
+  destruct u. apply O_S in I. contradiction I.
+  simpl. rewrite IHv. rewrite repeat_length. reflexivity.
+  inversion I. reflexivity.
+
+  rewrite H1. reflexivity. inversion H. reflexivity. rewrite H0.
+  assert (forall (u: list X) v w,
+    filter fst (combine (repeat false (length u) ++ v) (u ++ w))
+      = filter fst (combine v w)).
+  intro u. induction u; intros v w. reflexivity. simpl. apply IHu.
+
+  assert (forall (v: list (list X)) (u : list X),
+    length u = length v
+    -> u = map snd (filter fst (combine
+         (flat_map (fun e => true:: repeat false (length e)) v)
+         (flat_map (fun e => fst e :: snd e) (combine u v))))).
+  intro v. induction v; intro u; intro I.
+  apply length_zero_iff_nil in I. rewrite I. reflexivity.
+  destruct u. apply O_S in I. contradiction I.
+  simpl. rewrite H1. rewrite <- IHv. reflexivity. inversion I.
+  reflexivity. rewrite H1. rewrite <- H2. reflexivity.
+  inversion H. reflexivity.
+Qed.
+
+
+Theorem subsequence_eq_def_2 {X: Type} :
+  forall l s : list X, subsequence2 l s -> subsequence3 l s.
+Proof.
+  intros l s. intro H. destruct H. destruct H.
+
+  assert (I: forall u (v w: list X),
+    length u = length w
+    -> v = map snd (filter fst (combine u w))
+    -> subsequence3 w v).
+  intro u. induction u; intros v w; intros I J.
+  rewrite J. apply subsequence3_nil_r.
+  destruct v. apply subsequence3_nil_r.
+  destruct w. apply Nat.neq_succ_0 in I. contradiction I.
+  destruct a. exists nil. exists w.
+  inversion J. apply IHu in H3.
+  split. reflexivity. inversion J. rewrite <- H5. assumption.
+  inversion I. reflexivity. simpl in J.
+
+  assert (subsequence3 w (x0::v)). apply IHu.
+  inversion I. reflexivity. assumption.
+  apply subsequence3_cons_l. assumption.
+
+  apply I with (u := x); assumption.
+Qed.
+
+
+Theorem subsequence_eq_def_3 {X: Type} :
+  forall l s : list X, subsequence3 l s -> subsequence l s.
+Proof.
+  intros l s. generalize l. induction s; intro l0; intro H.
+  apply subsequence_nil_r. destruct H. destruct H. destruct H.
+  apply IHs in H0. destruct H0. destruct H0. destruct H0.
+  exists x. exists (x1:: x2). split. simpl. rewrite H0.
+  reflexivity. rewrite H. rewrite H1. reflexivity.
+Qed.
+
+
+(**
+   Decidability of all definitions of a subsequence.
 *)
 
 Theorem subsequence2_dec {X: Type}:
@@ -224,64 +307,14 @@ Theorem subsequence3_dec {X: Type}:
   (forall x y : X, {x = y} + {x <> y})
   -> forall (l s : list X), { subsequence3 l s } + { ~ subsequence3 l s }.
 Proof.
-  intro H. intro l. induction l. intro s. destruct s. left. reflexivity.
-  right. apply subsequence3_nil_cons_r.
-
-  intro s. assert({subsequence3 l s} + {~ subsequence3 l s}). apply IHl.
-  destruct H0.
-
-  rewrite <- subsequence3_cons_eq with (a := a) in s0.
-  apply subsequence3_cons_r in s0. left. assumption.
-
-  destruct s. left. apply subsequence3_nil_r.
-  assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.
-  destruct IHl with (s := s); [ left | right ];
-  rewrite subsequence3_cons_eq; assumption.
-
-  right. intro I.
-  destruct I. destruct H0. destruct H0. destruct x0.
-  inversion H0. rewrite H3 in n0. contradiction n0. reflexivity.
-
-  assert (subsequence3 l (x::s)). exists x2. exists x1.
-  inversion H0. split. reflexivity. assumption.
-  apply n in H2. contradiction H2.
-Qed.
-
-
-Theorem subsequence_eq_def_2 {X: Type} :
-  (forall (x y : X), {x = y} + {x <> y})
-  -> (forall l s : list X, subsequence l s <-> subsequence2 l s).
-Proof.
-  intro I. intro l. induction l.
-  intro s. split; intro H. destruct s. apply subsequence2_nil_r.
-  apply subsequence_nil_cons_r in H. contradiction H.
-  destruct s. apply subsequence_nil_r.
-  apply subsequence2_nil_cons_r in H. contradiction H.
-
-  intro s. destruct s. split; intro H. apply subsequence2_nil_r.
-  apply subsequence_nil_r.
-
-  assert ({a=x} + {a<>x}). apply I. destruct H.
-  rewrite e. rewrite subsequence2_cons_eq. rewrite <- IHl.
-  rewrite subsequence_cons_eq. split; intro; assumption.
-
-  split; intro H. apply subsequence2_cons_l. apply IHl.
-  destruct H. destruct H. destruct H.
-  destruct x0. destruct x1.
-  apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
-  simpl in H0. inversion H0. rewrite H2 in n. contradiction n.
-  reflexivity. inversion H0.
-  exists x2. exists x1. split. assumption.
-  reflexivity.
-
-  apply subsequence_cons_l. apply IHl.
-  destruct H. destruct H.
-  destruct x0. simpl in H0.
-  symmetry in H0. apply nil_cons in H0. contradiction H0.
-  destruct b. simpl in H0. inversion H0. rewrite H2 in n.
-  contradiction n. reflexivity.
-  exists x0. inversion H. inversion H0.
-  split; reflexivity.
+  intro H. intros l s.
+  assert ({ subsequence2 l s } + { ~ subsequence2 l s }).
+  apply subsequence2_dec. assumption. destruct H0.
+  apply subsequence_eq_def_2 in s0. left. assumption.
+  right. unfold not. intro I.
+  apply subsequence_eq_def_3 in I.
+  apply subsequence_eq_def_1 in I.
+  apply n in I. contradiction I.
 Qed.
 
 
@@ -290,45 +323,13 @@ Theorem subsequence_dec {X: Type}:
   -> forall (l s : list X), { subsequence l s } + { ~ subsequence l s }.
 Proof.
   intro H. intros l s.
-  assert ({ subsequence2 l s } + { ~ subsequence2 l s }).
-  apply subsequence2_dec. assumption. destruct H0.
-  rewrite <- subsequence_eq_def_2 in s0. left. assumption.
-  assumption. rewrite <- subsequence_eq_def_2 in n. right. assumption.
-  assumption.
-Qed.
-
-
-Theorem subsequence_eq_def_3 {X: Type} :
-  (forall (x y : X), {x = y} + {x <> y})
-  -> (forall l s : list X, subsequence l s <-> subsequence3 l s).
-Proof.
-  intro I. intro l. induction l.
-  intro s. split; intro H. destruct s. apply subsequence3_nil_r.
-  apply subsequence_nil_cons_r in H. contradiction H.
-  destruct s. apply subsequence_nil_r.
-  apply subsequence3_nil_cons_r in H. contradiction H.
-
-  intro s. destruct s. split; intro H. apply subsequence3_nil_r.
-  apply subsequence_nil_r.
-
-  assert ({a=x} + {a<>x}). apply I. destruct H.
-  rewrite e. rewrite subsequence3_cons_eq. rewrite <- IHl.
-  rewrite subsequence_cons_eq. split; intro; assumption.
-
-  split; intro H. apply subsequence3_cons_l. apply IHl.
-  destruct H. destruct H. destruct H.
-  destruct x0. destruct x1.
-  apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
-  simpl in H0. inversion H0. rewrite H2 in n. contradiction n.
-  reflexivity. inversion H0.
-  exists x2. exists x1. split. assumption.
-  reflexivity.
-
-  apply subsequence_cons_l. apply IHl.
-  destruct H. destruct H. destruct H.
-
-  destruct x0. inversion H. rewrite H2 in n. contradiction n. reflexivity.
-  exists x2. exists x1. split. inversion H. reflexivity. assumption.
+  assert ({ subsequence3 l s } + { ~ subsequence3 l s }).
+  apply subsequence3_dec. assumption. destruct H0.
+  apply subsequence_eq_def_3 in s0. left. assumption.
+  right. unfold not. intro I.
+  apply subsequence_eq_def_1 in I.
+  apply subsequence_eq_def_2 in I.
+  apply n in I. contradiction I.
 Qed.
 
 
@@ -446,173 +447,7 @@ Qed.
 
 Example test3: subsequence [1;2;3;4;5] [1;3;5].
 Proof.
-  rewrite subsequence_eq_def_2.
+  apply subsequence_eq_def_3. apply subsequence_eq_def_2.
   exists [true; false; true; false; true].
   split; reflexivity.
-  apply Nat.eq_dec.
 Qed.
-
-
-
-
-
-Theorem subsequence0_eq_def_2 {X: Type} :
-  forall l s : list X, subsequence l s -> subsequence2 l s.
-Proof.
-  intros l s. intro H. destruct H. destruct H. destruct H.
-
-  exists (
-    (repeat false (length x)) ++
-    (flat_map (fun e => true :: (repeat false (length e))) x0)).
-  split.
-  rewrite H0. rewrite app_length. rewrite app_length. rewrite repeat_length.
-  rewrite Nat.add_cancel_l. rewrite flat_map_length. rewrite flat_map_length.
-
-  assert (forall v (u: list X),
-    length u = length v
-    -> map (fun e => length (fst e :: snd e)) (combine u v)
-       = map (fun e => length (true :: repeat false (length e))) v).
-  intro v. induction v; intro u; intro I.
-  apply length_zero_iff_nil in I. rewrite I. reflexivity.
-  destruct u. apply O_S in I. contradiction I.
-  simpl. rewrite IHv. rewrite repeat_length. reflexivity.
-  inversion I. reflexivity.
-
-  rewrite H1. reflexivity. inversion H. reflexivity. rewrite H0.
-  assert (forall (u: list X) v w,
-    filter fst (combine (repeat false (length u) ++ v) (u ++ w))
-      = filter fst (combine v w)).
-  intro u. induction u; intros v w. reflexivity. simpl. apply IHu.
-
-  assert (forall (v: list (list X)) (u : list X),
-    length u = length v
-    -> u = map snd (filter fst (combine
-         (flat_map (fun e => true:: repeat false (length e)) v)
-         (flat_map (fun e => fst e :: snd e) (combine u v))))).
-  intro v. induction v; intro u; intro I.
-  apply length_zero_iff_nil in I. rewrite I. reflexivity.
-  destruct u. apply O_S in I. contradiction I.
-  simpl. rewrite H1. rewrite <- IHv. reflexivity. inversion I.
-  reflexivity. rewrite H1. rewrite <- H2. reflexivity.
-  inversion H. reflexivity.
-Qed.
-
-
-Theorem subsequence0_eq_def_3 {X: Type} :
-  forall l s : list X, subsequence2 l s -> subsequence3 l s.
-Proof.
-  intros l s. intro H. destruct H. destruct H.
-
-  assert (I: forall u (v w: list X),
-    length u = length w
-    -> v = map snd (filter fst (combine u w))
-    -> subsequence3 w v).
-  intro u. induction u; intros v w; intros I J.
-  rewrite J. apply subsequence3_nil_r.
-  destruct v. apply subsequence3_nil_r.
-  destruct w. apply Nat.neq_succ_0 in I. contradiction I.
-  destruct a. exists nil. exists w.
-  inversion J. apply IHu in H3.
-  split. reflexivity. inversion J. rewrite <- H5. assumption.
-  inversion I. reflexivity. simpl in J.
-
-  assert (subsequence3 w (x0::v)). apply IHu.
-  inversion I. reflexivity. assumption.
-  apply subsequence3_cons_l. assumption.
-
-  apply I with (u := x); assumption.
-Qed.
-
-
-Theorem subsequence0_eq_def_1 {X: Type} :
-  forall l s : list X, subsequence3 l s -> subsequence l s.
-Proof.
-  intros l s. generalize l. induction s; intro l0; intro H.
-  apply subsequence_nil_r. destruct H. destruct H. destruct H.
-  apply IHs in H0. destruct H0. destruct H0. destruct H0.
-  exists x. exists (x1:: x2). split. simpl. rewrite H0.
-  reflexivity. rewrite H. rewrite H1. reflexivity.
-Qed.
-
-
-
-
-
-(*
-  destruct H. destruct H.
-
-  (* z contient la position des booléens dans x *)
-  pose (z := map snd (filter fst (combine x (seq 0 (length x))))).
-  destruct s. exists l. exists nil. rewrite app_nil_r. split; easy.
-
-  assert (0 < length z). unfold z. rewrite map_length.
-  assert (forall v (u: list X) (w: list nat),
-  length u = length v -> length u = length w
-    -> length (filter fst (combine v w))
-        = length (map snd (filter fst (combine v u)))).
-  intro v. induction v; intros u w; intros I J. reflexivity.
-  destruct w. apply length_zero_iff_nil in J. rewrite J in I.
-  apply O_S in I. contradiction I.
-  destruct u. apply O_S in J. contradiction J.
-  destruct a; simpl. apply eq_S. apply IHv.
-  inversion I. reflexivity. inversion J. reflexivity.
-  apply IHv.
-  inversion I. reflexivity. inversion J. reflexivity.
-  assert (length (x0::s) = length (map snd (filter fst (combine x l)))).
-  rewrite H0. reflexivity. rewrite <- H1 with (w := seq 0 (length x)) in H2.
-  rewrite <- H2. apply Nat.lt_0_succ. inversion H. reflexivity.
-  rewrite H. rewrite seq_length. reflexivity.
-  exists (firstn (hd 0 z) l).
-
-  (* z2 contient la position du true suivant *)
-  pose (z2 := (skipn 1 z) ++ [ length l ]).
-
-  (* z3 contient la longueur de chaque bloc  true; false; false; ... *)
-  pose (z3 := map (fun e => (snd e) - (fst e)) (combine z z2)).
-
-  exists (map (fun e => firstn ((snd e) -1) (skipn (S (fst e)) l))
-            (combine z z3)).
-
-  assert (length (x0::s) = length z). unfold z. rewrite H0.
-  rewrite map_length. rewrite map_length. rewrite H.
-  assert (forall u (v: list X) (w: list nat),
-    length v = length w
-    -> length (filter fst (combine u v))
-       = length (filter fst (combine u w))).
-  intro u. induction u; intros v w; intro I. reflexivity.
-  destruct v. symmetry in I. apply length_zero_iff_nil in I.
-  rewrite I. reflexivity. destruct w. apply Nat.neq_succ_0 in I.
-  contradiction I. destruct a; simpl; rewrite IHu with (w := w).
-  inversion I; reflexivity. inversion I; reflexivity. reflexivity.
-  inversion I; reflexivity. rewrite H2 with (w := seq 0 (length l)).
-  reflexivity. rewrite seq_length. reflexivity.
-
-  unfold z3. unfold z2. split. destruct z. apply Nat.nlt_0_r in H1.
-  contradiction H1.
-  rewrite map_length. rewrite combine_length. rewrite map_length.
-  rewrite combine_length. rewrite app_length. rewrite Nat.add_1_r.
-  simpl. apply eq_S. rewrite Nat.min_id. rewrite Nat.min_id.
-  inversion H2. reflexivity. unfold z. rewrite H0.
-
-  assert (forall (u: list bool) (v: list X),
-    length u = length v
-    -> v =
-    firstn (hd 0 (map snd (filter fst (combine u (seq 0 (length u)))))) v ++
-    flat_map (fun e : X * list X => fst e :: snd e)
-      (combine (map snd (filter fst (combine u v)))
-         (map (fun e : nat * nat => firstn (snd e - 1) (skipn (S (fst e)) v))
-            (combine (map snd (filter fst (combine u (seq 0 (length u)))))
-               (map (fun e : nat * nat => snd e - fst e)
-                  (combine (map snd (filter fst (combine u (seq 0 (length u)))))
-                     (skipn 1
-                        (map snd (filter fst (combine u (seq 0 (length u))))) ++
-                      [length v]))))))).
-  intro u. induction u; intro v; intro I.
-  symmetry in I. apply length_zero_iff_nil in I. assumption.
-  destruct v. rewrite app_nil_r. rewrite firstn_nil. reflexivity.
-  destruct a. 
-
-  replace
-     (map snd (filter fst (combine (true :: u) (seq 0 (length (true :: u))))))
-  with 
- *)