From 43d97734b24a59e5e6d6af1a8f0253ed21b113e1 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 1 Nov 2023 21:08:36 +0100 Subject: [PATCH] Update --- src/subsequences.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/subsequences.v b/src/subsequences.v index 3cbcd42..0c4ffe7 100644 --- a/src/subsequences.v +++ b/src/subsequences.v @@ -425,9 +425,8 @@ Proof. apply length_zero_iff_nil in I. rewrite I. reflexivity. destruct u0. reflexivity. destruct v0. apply PeanoNat.Nat.neq_succ_0 in J; contradiction J. - destruct b; simpl; rewrite K; rewrite IHw. - reflexivity. inversion I; reflexivity. inversion J; reflexivity. - reflexivity. inversion I; reflexivity. inversion J; reflexivity. + destruct b; simpl; rewrite K; rewrite IHw; + inversion I; inversion J; reflexivity. rewrite H4; try rewrite H1; try rewrite H; reflexivity. Qed.