Update

src/subsequences.v

@@ -339,6 +339,17 @@ Proof.
 Qed.
 
 
+Theorem subsequence_dec :
+  (forall x y : Type, {x = y} + {x <> y})
+  -> forall (l s : list Type), { subsequence l s } + { ~ subsequence l s }.
+Proof.
+  intro H. intros l s.
+  assert ({ subsequence2 l s } + { ~ subsequence2 l s }).
+  apply subsequence2_dec. assumption. destruct H0.
+  rewrite <- subsequence_eq_def in s0. left. assumption.
+  assumption. rewrite <- subsequence_eq_def in n. right. assumption.
+  assumption.
+Qed.