From 2b0a2143525d26ce074fa64a62ab59dc0bfb45b6 Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Wed, 6 Dec 2023 08:16:50 +0100
Subject: [PATCH] Update

---
 src/subsequences2.v | 27 ++++++++++++---------------
 1 file changed, 12 insertions(+), 15 deletions(-)

diff --git a/src/subsequences2.v b/src/subsequences2.v
index 785ed4f..28a41aa 100644
--- a/src/subsequences2.v
+++ b/src/subsequences2.v
@@ -198,23 +198,12 @@ Proof.
 Qed.
 
 
-
-
-
-
-
-
-
-
-
-Theorem subsequence_app {X: Type} :
+Theorem Subsequence_app {X: Type} :
   forall l1 s1 l2 s2 : list X,
-  subsequence l1 s1 -> subsequence l2 s2 -> subsequence (l1++l2) (s1++s2).
+  Subsequence l1 s1 -> Subsequence l2 s2 -> Subsequence (l1++l2) (s1++s2).
 Proof.
-  intros l1 s1 l2 s2. intros H I.
-  apply subsequence_eq_def_3. apply subsequence_eq_def_2.
-  apply subsequence_eq_def_1 in H.
-  apply subsequence_eq_def_1 in I.
+  intros l1 s1 l2 s2. intros H I. apply Subsequence_bools.
+  apply Subsequence_bools in H. apply Subsequence_bools in I.
   destruct H. destruct I. exists (x++x0). destruct H. destruct H0.
   split. rewrite app_length. rewrite app_length.
   rewrite H. rewrite H0. reflexivity.
@@ -234,6 +223,14 @@ Proof.
 Qed.
 
 
+
+
+
+
+
+
+
+
 Theorem subsequence_trans {X: Type} :
   forall (l1 l2 l3: list X),
   subsequence l1 l2 -> subsequence l2 l3 -> subsequence l1 l3.