diff --git a/src/subsequences.v b/src/subsequences.v
index ccc64f0..b47ce34 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -585,15 +585,18 @@ Qed.
 
 
 Theorem subsequence_double_cons {X: Type} :
-  forall (u v: list X) a, subsequence (a::u) (a::v) -> subsequence u v.
+  forall (u v: list X) a, subsequence (a::u) (a::v) <-> subsequence u v.
 Proof.
-  intros u v a. intro H. destruct H. destruct H. destruct H.
+  intros u v a. split; intro H. destruct H. destruct H. destruct H.
   destruct x; destruct x0. symmetry in H0. apply nil_cons in H0.
   contradiction. inversion H0.
   exists l. exists x0. split. inversion H. reflexivity. reflexivity.
   apply PeanoNat.Nat.neq_succ_0 in H. contradiction.
   inversion H0. exists (x1++x::l). exists x0. split. inversion H.
   reflexivity. rewrite <- app_assoc. reflexivity.
+  apply subsequence_eq_def_3. exists nil. exists u.
+  split. reflexivity. apply subsequence_eq_def_2. apply subsequence_eq_def_1.
+  assumption.
 Qed.
 
 
@@ -617,7 +620,7 @@ Proof.
 Qed.
 
 
-Theorem subsequence_filter {X: Type} :
+Theorem subsequence_filter_2 {X: Type} :
   forall (u v: list X) f,
     subsequence u v -> subsequence (filter f u) (filter f v).
 Proof.
@@ -634,13 +637,6 @@ Proof.
   apply subsequence_nil_r. simpl. destruct (f a).
   apply subsequence_cons_r.
 
-Theorem subsequence_trans {X: Type} :
-  forall (l1 l2 l3: list X),
-  subsequence l1 l2 -> subsequence l2 l3 -> subsequence l1 l3.
-
-
-
-
 
 Theorem subsequence_incl {X: Type} :
   forall (u v: list X), subsequence u v -> incl v u.