diff --git a/src/subsequences.v b/src/subsequences.v
index e0e2631..bd9af72 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -337,11 +337,14 @@ Qed.
    Various general properties of a subsequence.
 *)
 
-Theorem subsequence2_app {X: Type} :
+Theorem subsequence_app {X: Type} :
   forall l1 s1 l2 s2 : list X,
-  subsequence2 l1 s1 -> subsequence2 l2 s2 -> subsequence2 (l1++l2) (s1++s2).
+  subsequence l1 s1 -> subsequence l2 s2 -> subsequence (l1++l2) (s1++s2).
 Proof.
   intros l1 s1 l2 s2. intros H I.
+  apply subsequence_eq_def_3. apply subsequence_eq_def_2.
+  apply subsequence_eq_def_1 in H.
+  apply subsequence_eq_def_1 in I.
   destruct H. destruct I. exists (x++x0). destruct H. destruct H0.
   split. rewrite app_length. rewrite app_length.
   rewrite H. rewrite H0. reflexivity.
@@ -363,9 +366,11 @@ Qed.
 
 Theorem subsequence_trans {X: Type} :
   forall (l1 l2 l3: list X),
-  subsequence l1 l2 -> subsequence2 l2 l3 -> subsequence2 l1 l3.
+  subsequence l1 l2 -> subsequence l2 l3 -> subsequence l1 l3.
 Proof.
   intros l1 l2 l3. intros H I.
+  apply subsequence_eq_def_3. apply subsequence_eq_def_2.
+  apply subsequence_eq_def_1 in I.
   destruct H. destruct H. destruct H. destruct I. destruct H1.
   exists (
     (repeat false (length x)) ++