diff --git a/src/subsequences.v b/src/subsequences.v
index 9a65c7c..52482d8 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -289,3 +289,7 @@ Qed.
 Example test3: subsequence [1;2;3;4;5] [1;3;5].
 Proof.
   rewrite subsequence_eq_def.
+  exists [true; false; true; false; true].
+  split; reflexivity.
+  apply Nat.eq_dec.
+Qed.