diff --git a/src/subsequences.v b/src/subsequences.v
index 0f38041..3cbcd42 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -232,7 +232,6 @@ Proof.
   apply length_zero_iff_nil in I. rewrite I. reflexivity.
   destruct u. apply O_S in I. contradiction I.
   simpl. rewrite H1. rewrite <- IHv; inversion I; reflexivity.
-
   rewrite H1. rewrite <- H2; inversion H; reflexivity.
 Qed.
 
@@ -250,15 +249,11 @@ Proof.
   rewrite J. apply subsequence3_nil_r.
   destruct v. apply subsequence3_nil_r.
   destruct w. apply Nat.neq_succ_0 in I. contradiction I.
-  destruct a. exists nil. exists w.
-  inversion J. apply IHu in H3.
-  split. reflexivity. inversion J. rewrite <- H5. assumption.
-  inversion I. reflexivity. simpl in J.
-
-  assert (subsequence3 w (x0::v)). apply IHu.
-  inversion I. reflexivity. assumption.
-  apply subsequence3_cons_l. assumption.
-
+  destruct a. exists nil. exists w. inversion J.
+  apply IHu in H3. split; inversion J; try rewrite <- H5; easy.
+  inversion I. reflexivity.
+  assert (subsequence3 w (x0::v)). apply IHu; inversion I; easy.
+  apply subsequence3_cons_l; assumption.
   apply I with (u := x); assumption.
 Qed.