diff --git a/src/subsequences.v b/src/subsequences.v
index 985450e..c6a81ea 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -844,9 +844,12 @@ Qed.
 
 
 Theorem subsequence_as_partition {X: Type} :
-  forall (u: list X) f, subsequence u (fst (partition f u)).
+  forall (u v w: list X) f,
+    (v, w) = partition f u -> (subsequence u v) /\ (subsequence u w).
 Proof.
-  intros u f.
-  rewrite partition_as_filter. simpl.
-  apply subsequence_as_filter with (f := f).
+  intros u v w f. intro H. rewrite partition_as_filter in H. split.
+  replace v with (fst (v, w)). rewrite H. simpl.
+  apply subsequence_as_filter. reflexivity.
+  replace w with (snd (v, w)). rewrite H. simpl.
+  apply subsequence_as_filter. reflexivity.
 Qed.