diff --git a/src/subsequences.v b/src/subsequences.v
index 8fe687b..6a19959 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -329,10 +329,10 @@ Proof.
 
 
   assert ({a=x} + {a<>x}). apply I. destruct H.
-  rewrite e. rewrite subsequence2_cons_eq. rewrite <- IHl.
+  rewrite e. rewrite subsequence3_cons_eq. rewrite <- IHl.
   rewrite subsequence_cons_eq. split; intro; assumption.
 
-  split; intro H. apply subsequence2_cons_l. apply IHl.
+  split; intro H. apply subsequence3_cons_l. apply IHl.
   destruct H. destruct H. destruct H.
   destruct x0. destruct x1.
   apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
@@ -342,14 +342,11 @@ Proof.
   reflexivity.
 
   apply subsequence_cons_l. apply IHl.
-  destruct H. destruct H.
-  destruct x0. simpl in H0.
-  symmetry in H0. apply nil_cons in H0. contradiction H0.
-  destruct b. simpl in H0. inversion H0. rewrite H2 in n.
-  contradiction n. reflexivity.
-  exists x0. inversion H. inversion H0.
-  split; reflexivity.
-Admitted.
+  destruct H. destruct H. destruct H.
+
+  destruct x0. inversion H. rewrite H2 in n. contradiction n. reflexivity.
+  exists x2. exists x1. split. inversion H. reflexivity. assumption.
+Qed.
 
 
 Theorem subsequence_dec {X: Type}: