From bc25f2d5215152fe943109b090abcdccc5357c0b Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 1 Nov 2023 19:13:41 +0100 Subject: [PATCH] Update --- src/subsequences.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/subsequences.v b/src/subsequences.v index bd9af72..1e2aa95 100644 --- a/src/subsequences.v +++ b/src/subsequences.v @@ -311,7 +311,7 @@ Proof. assert ({ subsequence2 l s } + { ~ subsequence2 l s }). apply subsequence2_dec. assumption. destruct H0. apply subsequence_eq_def_2 in s0. left. assumption. - right. unfold not. intro I. + right. intro I. apply subsequence_eq_def_3 in I. apply subsequence_eq_def_1 in I. apply n in I. contradiction I. @@ -326,7 +326,7 @@ Proof. assert ({ subsequence3 l s } + { ~ subsequence3 l s }). apply subsequence3_dec. assumption. destruct H0. apply subsequence_eq_def_3 in s0. left. assumption. - right. unfold not. intro I. + right. intro I. apply subsequence_eq_def_1 in I. apply subsequence_eq_def_2 in I. apply n in I. contradiction I.