From 444d3a655083adbca1e2a11cef21a4720e4aa4e1 Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Wed, 1 Nov 2023 18:31:41 +0100
Subject: [PATCH] Update

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

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.