diff --git a/src/subsequences.v b/src/subsequences.v
index 5055489..56714fa 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -833,16 +833,25 @@ Proof.
 Qed.
 
 
-Theorem subsequence_partition {X: Type} :
+Theorem subsequence_as_filter {X: Type} :
   forall (u v: list X),
-    (exists f, v = fst (partition f u)) -> subsequence u v .
+    (exists f, v = filter f u) -> subsequence u v.
 Proof.
-  intros u v. intro H. destruct H.
+  intros u v; intro H. destruct H. rewrite H.
   apply subsequence_eq_def_3. apply subsequence_eq_def_2.
-  exists (map x u). split. apply map_length. rewrite H.
-  rewrite partition_as_filter. simpl.
+  exists (map x u). split. apply map_length.
   assert (L: forall g (w: list X),
       filter g w = map snd (filter fst (combine (map g w) w))).
   intros g w. induction w. reflexivity. simpl. destruct (g a).
   simpl. rewrite IHw. reflexivity. assumption. apply L.
 Qed.
+
+
+Theorem subsequence_partition {X: Type} :
+  forall (u v: list X),
+    (exists f, v = fst (partition f u)) -> subsequence u v .
+Proof.
+  intros u v. intro H. destruct H. rewrite H.
+  rewrite partition_as_filter. simpl. apply subsequence_as_filter.
+  exists x. reflexivity.
+Qed.