diff --git a/src/subsequences.v b/src/subsequences.v
index 0c4ffe7..61c2700 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -294,10 +294,8 @@ Proof.
   destruct I. destruct H0. destruct x0.
   symmetry in H1. apply nil_cons in H1. contradiction H1.
   destruct b.
-  inversion H1. rewrite H3 in n0. contradiction n0. reflexivity.
-
-  assert (subsequence2 l (x::s)). exists x0. split; inversion H0; easy.
-  apply n in H2. contradiction H2.
+  inversion H1. rewrite H3 in n0. easy.
+  apply n. exists x0; split; inversion H0; easy.
 Qed.