diff --git a/src/subsequences.v b/src/subsequences.v
index 02c0970..9cc0a80 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -524,6 +524,15 @@ Proof.
 Qed.
 
 
+Theorem subsequence0_eq_def_1 {X: Type} :
+  forall l s : list X, subsequence3 l s -> subsequence l s.
+Proof.
+  intros l s. generalize l. induction s; intro l0; intro H.
+  apply subsequence_nil_r. destruct H. destruct H. destruct H.
+  apply IHs in H0. destruct H0. destruct H0. destruct H0.
+  exists x. exists (x1:: x2). split. simpl. rewrite H0.
+  reflexivity. rewrite H. rewrite H1. reflexivity.
+Qed.