From 00cf74be9c8bf45562d99b23a45657758e64db39 Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Wed, 1 Nov 2023 20:55:55 +0100
Subject: [PATCH] Update

---
 src/subsequences.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/subsequences.v b/src/subsequences.v
index cc01d8a..0f38041 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -217,7 +217,7 @@ Proof.
   simpl. rewrite IHv. rewrite repeat_length. reflexivity.
   inversion I. reflexivity.
 
-  rewrite H1. reflexivity. inversion H. reflexivity. rewrite H0.
+  rewrite H1; inversion H; reflexivity. rewrite H0.
   assert (forall (u: list X) v w,
     filter fst (combine (repeat false (length u) ++ v) (u ++ w))
       = filter fst (combine v w)).
@@ -231,9 +231,9 @@ Proof.
   intro v. induction v; intro u; intro I.
   apply length_zero_iff_nil in I. rewrite I. reflexivity.
   destruct u. apply O_S in I. contradiction I.
-  simpl. rewrite H1. rewrite <- IHv. reflexivity. inversion I.
-  reflexivity. rewrite H1. rewrite <- H2. reflexivity.
-  inversion H. reflexivity.
+  simpl. rewrite H1. rewrite <- IHv; inversion I; reflexivity.
+
+  rewrite H1. rewrite <- H2; inversion H; reflexivity.
 Qed.