diff --git a/src/subsequences.v b/src/subsequences.v
index 99be30e..8263396 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -726,15 +726,6 @@ Theorem subsequence_filter_2 {X: Type} :
   forall (u v: list X) f,
     subsequence u v -> subsequence (filter f u) (filter f v).
 Proof.
-  (*
-  intro u. induction u; intros v f; intro H.
-  assert (v = nil). destruct v. reflexivity.
-  apply subsequence_eq_def_1 in H. apply subsequence_eq_def_2 in H.
-  destruct H. destruct H. destruct H.
-  destruct x0; apply nil_cons in H; contradiction.
-  rewrite H0. apply subsequence_nil_r.
-  simpl. destruct (f a).
-  *)
   intros u v. generalize u. induction v; intros u0 f; intro H.
   apply subsequence_nil_r.