From ab46174c218ad6b9bf09013044f577b8c8a2ebbf Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Mon, 30 Oct 2023 08:18:20 +0100
Subject: [PATCH] Update

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

diff --git a/src/subsequences.v b/src/subsequences.v
index 66eb6eb..509d2fb 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -25,15 +25,14 @@ Definition subsequence3 (l s : list Type) :=
 
 Theorem subsequence_nil_r : forall (l : list Type), subsequence l nil.
 Proof.
-  intro l. unfold subsequence. exists l. exists nil. rewrite app_nil_r.
-  split; easy.
+  intro l. exists l. exists nil. rewrite app_nil_r. split; easy.
 Qed.
 
 
 Theorem subsequence_nil_cons_r : forall (l: list Type) (a:Type),
   ~ subsequence nil (a::l).
 Proof.
-  intros l a. unfold subsequence. unfold not. intro H.
+  intros l a. unfold not. intro H.
   destruct H. destruct H. destruct H.
   destruct x. rewrite app_nil_l in H0.
   destruct x0. apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
@@ -44,7 +43,7 @@ Qed.
 
 Theorem subsequence2_nil_r : forall (l : list Type), subsequence2 l nil.
 Proof.
-  intro l. unfold subsequence2.
+  intro l. 
   exists (repeat false (length l)). rewrite repeat_length.
   split. easy.
   induction l. reflexivity. simpl. assumption.
@@ -54,7 +53,7 @@ Qed.
 Theorem subsequence2_nil_cons_r : forall (l: list Type) (a:Type),
   ~ subsequence2 nil (a::l).
 Proof.
-  intros l a. unfold subsequence2. unfold not. intro H. destruct H.
+  intros l a. unfold not. intro H. destruct H.
   destruct H. assert (x = nil). destruct x. reflexivity.
   apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
   rewrite H1 in H0. symmetry in H0. apply nil_cons in H0. contradiction H0.
@@ -64,7 +63,7 @@ Qed.
 Theorem subsequence2_cons_l : forall (l s: list Type) (a: Type),
   subsequence2 l s -> subsequence2 (a::l) s.
 Proof.
-  intros l s a. intro H. unfold subsequence2 in H.
+  intros l s a. intro H.
   destruct H. destruct H. exists (false::x).
   split. simpl. apply eq_S. assumption.
   simpl. assumption.
@@ -75,14 +74,11 @@ Theorem subsequence2_cons_r : forall (l s: list Type) (a: Type),
   subsequence2 l (a::s) -> subsequence2 l s.
 Proof.
   intro l. induction l. intros. apply subsequence2_nil_cons_r in H.
-  contradiction H. intros s a0 . intro H. unfold subsequence2 in H.
-  destruct H. destruct H. destruct x.
+  contradiction H. intros s a0 . intro H. destruct H. destruct H. destruct x.
   symmetry in H0. apply nil_cons in H0. contradiction H0.
   destruct b. simpl in H0. inversion H0.
-  unfold subsequence2. exists (false::x).
-  split; try rewrite <- H; reflexivity.
-  simpl in H0.
-  apply subsequence2_cons_l. apply IHl with (a := a0).
+  exists (false::x). split; try rewrite <- H; reflexivity.
+  simpl in H0. apply subsequence2_cons_l. apply IHl with (a := a0).
   unfold subsequence2. exists (x). split. inversion H.
   reflexivity. assumption.
 Qed.
@@ -93,8 +89,7 @@ Theorem subsequence2_cons_eq : forall (l1 l2: list Type) (a: Type),
 Proof.
   intros l s a. split. intro H. unfold subsequence2 in H.
   destruct H. destruct H. destruct x. inversion H0.
-  destruct b.
-  exists (x). split. inversion H. reflexivity. simpl in H0.
+  destruct b. exists (x). split. inversion H. reflexivity. simpl in H0.
   inversion H0. reflexivity. simpl in H0. inversion H.
   assert (subsequence2 l (a::s)). exists x. split; assumption.
   apply subsequence2_cons_r with (a := a). assumption.