From 9325baf42b8964d56b3f13c3062c3b6de964c20d Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Mon, 30 Oct 2023 13:00:05 +0100
Subject: [PATCH] Update

---
 src/subsequences.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/subsequences.v b/src/subsequences.v
index 202c34f..f14cdf3 100644
--- a/src/subsequences.v
+++ b/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.