From d1927fca71a7b6204824b094bb7a9ec0527d129c Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 1 Nov 2023 21:42:31 +0100 Subject: [PATCH] Update --- src/subsequences.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/subsequences.v b/src/subsequences.v index 61c2700..febcdc0 100644 --- a/src/subsequences.v +++ b/src/subsequences.v @@ -283,7 +283,7 @@ Proof. assert({subsequence2 l s} + {~ subsequence2 l s}). apply IHl. destruct H0. rewrite <- subsequence2_cons_eq with (a := a) in s0. - apply subsequence2_cons_r in s0. left. assumption. + apply subsequence2_cons_r in s0. left; assumption. destruct s. left. apply subsequence2_nil_r. assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.