diff --git a/src/subsequences.v b/src/subsequences.v
index 0ac0b63..35515ab 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -142,21 +142,19 @@ Qed.
 Theorem subsequence_cons_eq {X: Type} : forall (l1 l2: list X) (a: X),
   subsequence (a::l1) (a::l2) <-> subsequence l1 l2.
 Proof.
-  intros l s a. split; intro H.
-  destruct H. destruct H. destruct H.
+  intros l s a. split; intro H; destruct H; destruct H; destruct H.
   destruct x. destruct x0.
   apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
   simpl in H0. inversion H0. exists l0. exists x0.
   inversion H. rewrite H3. split; reflexivity.
-  destruct x0. simpl in H0.
+  destruct x0. 
   apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
   exists (x1 ++ (a::l0)). exists x0. inversion H. rewrite H2. split. reflexivity.
   inversion H0. rewrite <- app_assoc. apply app_inv_head_iff.
   rewrite app_comm_cons. reflexivity.
 
-  destruct H. destruct H. destruct H.
-  exists nil. exists (x::x0). simpl. split. rewrite H. reflexivity.
-  rewrite H0. reflexivity.
+  exists nil. exists (x::x0). simpl.
+  split; [ rewrite H | rewrite H0 ]; reflexivity.
 Qed.
 
 
@@ -165,19 +163,19 @@ Theorem subsequence2_cons_eq {X: Type}: forall (l1 l2: list X) (a: X),
 Proof.
   intros l s a. split; intro H; destruct H; destruct H.
   destruct x. inversion H0.
-  destruct b. exists (x). split. inversion H. rewrite H2. reflexivity. simpl in H0.
+  destruct b. exists (x). split. inversion H. rewrite H2. reflexivity.
   inversion H0. reflexivity. simpl in H0. inversion H.
   assert (subsequence2 l (a::s)). exists x. split; assumption.
   apply subsequence2_cons_r with (a := a). assumption.
   exists (true :: x).
-  split. simpl. apply eq_S. assumption. rewrite H0. reflexivity.
+  split. apply eq_S. assumption. rewrite H0. reflexivity.
 Qed.
 
 
 Theorem subsequence3_cons_eq {X: Type} : forall (l1 l2: list X) (a: X),
   subsequence3 (a::l1) (a::l2) <-> subsequence3 l1 l2.
 Proof.
-  intros l s a. split. intro H.
+  intros l s a. split; intro H.
   destruct H. destruct H. destruct H.
   destruct x. inversion H. assumption.
   destruct s. apply subsequence3_nil_r.
@@ -185,7 +183,7 @@ Proof.
   exists (x1 ++ (a::x3)). exists x4.
   inversion H. rewrite H0. rewrite <- app_assoc.
   rewrite app_comm_cons. split. reflexivity. assumption.
-  intro H. exists nil. exists l. split. reflexivity. assumption.
+  exists nil. exists l. split. reflexivity. assumption.
 Qed.